FiniteWordOutput.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Every-path output properties of the finite-word machine

theorem OAI.ContingencyTables.FiniteWordExecution.machine_all line 15

Source documentation

A property verified for every finite source word holds on every actual machine tape once the fixed execution bound has elapsed.

theorem machine_all (N : TreeTyped.Realizer n) (F : TreeTyped.Realizer f)
    (as : List Symbol) (ha : ∀ a∈as,a≠0)
    (hout : ∀ bs,∀ a∈f (as,bs),a≠6 ∧ a≠7)
    (P : Tape Symbol → Prop)
    (hf : ∀ bits : Bits (n as),P (Tape.mk₁ (f (as,List.ofFn bits))))
    (t : ℕ) (ht : machineTime N F as≤t) :
    ∀ bits : Bits t,P (run (machine N F) as bits).tape := by
…

Mentions: OAI.ContingencyTables.FiniteWordExecution.machineTime, OAI.ContingencyTables.FiniteWordExecution.machine