OAI/Combinatorics/ContingencyTables/Machines/CachedDecisionSemantics.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.SmallGraphProfiles.encodedShortStep line 22
2. theorem OAI.ContingencyTables.SmallGraphProfiles.cachedDecision_encoded line 27

   Source documentation

   This identity holds for every feasible cached completion, including those not selected by a particular finite random word.

   theorem cachedDecision_encoded (htotal : ∑ i,r i=∑ j,c j) (h : ℕ)
       (x : PaperStates r c) (word : Fin s → Bool) (A : Table (R x) (P x)) :
       cachedDecision (encodedShortStep r c e h x word,tableOutput A)=
         stateCode r c e (completionDecision R P x (decodedCodeProposal r c e x word) A) := by
   …

   Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.Table, OAI.ContingencyTables.SmallGraphProfiles.encodedShortStep, OAI.ContingencyTables.SmallGraphProfiles.stateCode, OAI.ContingencyTables.SmallGraphProfiles.decodedCodeProposal