lemma sem_uni_step1:
uni_step ⊨ [us_acc: low_step_R_true, low_step_R_false].
+@daemon (* this no longer works: TODO *) (*
@(acc_Realize_to_acc_Realize … sem_uni_step)
[@unistep_true_to_low_step | @unistep_false_to_low_step ]
+*)
qed.
definition universalTM ≝ whileTM ? uni_step us_acc.
theorem sem_universal: ∀M:normalTM. ∀qstart.
universalTM ⊫ (low_R M qstart (R_TM FinBool M qstart)).
+@daemon (* this no longer works: TODO *) (*
#M #q #intape #i #outc #Hloop
lapply (sem_while … sem_uni_step1 intape i outc Hloop)
[@daemon] -Hloop
|@Houtc
]
]
+*)
qed.
theorem sem_universal2: ∀M:normalTM. ∀R.