-definition R_TM ≝ λsig.λM:TM sig.λq.λt1,t2.
-∃i,outc.
- loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (mk_config ?? q t1) = Some ? outc ∧
- t2 = (ctape ?? outc).
-
-(*
-definition universal_R ≝ λM,R,t1,t2.
- Realize ? M R →
- ∀tape1,tape2.
- R tape1 tape 2 ∧
- t1 = low_config M (initc ? M tape1) ∧
- ∃q.halt ? M q = true → t2 = low_config M (mk_config ?? q tape2).*)
-
-axiom uni_step: TM STape.
-axiom us_acc: states ? uni_step.
-
-axiom sem_uni_step: accRealize ? uni_step us_acc low_step_R_true low_step_R_false.
+lemma sem_uni_step1:
+ uni_step ⊨ [us_acc: low_step_R_true, low_step_R_false].
+@(acc_Realize_to_acc_Realize … sem_uni_step)
+ [@unistep_true_to_low_step | @unistep_false_to_low_step ]
+qed.