qed.
definition universalTM ≝ whileTM ? uni_step us_acc.
theorem sem_universal: ∀M:normalTM. ∀qstart.
universalTM ⊫ (low_R M qstart (R_TM FinBool M qstart)).
qed.
definition universalTM ≝ whileTM ? uni_step us_acc.
theorem sem_universal: ∀M:normalTM. ∀qstart.
universalTM ⊫ (low_R M qstart (R_TM FinBool M qstart)).