+definition atml_step ≝
+ λalpha:FinSet.λtest:alpha→bool.
+ mk_TM alpha atm_states
+ (λp.let 〈q,a〉 ≝ p in
+ match a with
+ [ None ⇒ 〈atm1, None ?〉
+ | Some a' ⇒
+ match test a' with
+ [ true ⇒ 〈atm1,None ?〉
+ | false ⇒ 〈atm2,Some ? 〈a',L〉〉 ]])
+ atm0 (λx.notb (x == atm0)).
+
+definition Ratml_step_true ≝
+ λalpha,test,t1,t2.
+ ∃ls,a,rs.
+ t1 = midtape alpha ls a rs ∧ test a = false ∧
+ t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a :: rs).
+
+definition Ratml_step_false ≝
+ λalpha,test,t1,t2.
+ t1 = t2 ∧
+ (current alpha t1 = None ? ∨
+ (∃a.current ? t1 = Some ? a ∧ test a = true)).
+
+lemma atml_q0_q1 :
+ ∀alpha,test,ls,a0,rs. test a0 = true →
+ step alpha (atml_step alpha test)
+ (mk_config ?? atm0 (midtape … ls a0 rs)) =
+ mk_config alpha (states ? (atml_step alpha test)) atm1
+ (midtape … ls a0 rs).
+#alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
+whd in match (trans … 〈?,?〉); >Htest %
+qed.
+
+lemma atml_q0_q2 :
+ ∀alpha,test,ls,a0,rs. test a0 = false →
+ step alpha (atml_step alpha test)
+ (mk_config ?? atm0 (midtape … ls a0 rs)) =
+ mk_config alpha (states ? (atml_step alpha test)) atm2
+ (mk_tape … (tail ? ls) (option_hd ? ls) (a0 :: rs)).
+#alpha #test #ls #a0 #rs #Htest whd in ⊢ (??%?);
+whd in match (trans … 〈?,?〉); >Htest cases ls //
+qed.
+
+lemma sem_atml_step :
+ ∀alpha,test.
+ accRealize alpha (atml_step alpha test)
+ atm2 (Ratml_step_true alpha test) (Ratml_step_false alpha test).
+#alpha #test *
+[ @(ex_intro ?? 2)
+ @(ex_intro ?? (mk_config ?? atm1 (niltape ?))) %
+ [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
+| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (leftof ? a al)))
+ % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
+| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (rightof ? a al)))
+ % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
+| #ls #c #rs @(ex_intro ?? 2)
+ cases (true_or_false (test c)) #Htest
+ [ @(ex_intro ?? (mk_config ?? atm1 ?))
+ [| %
+ [ %
+ [ whd in ⊢ (??%?); >atml_q0_q1 //
+ | whd in ⊢ ((??%%)→?); #Hfalse destruct ]
+ | #_ % // %2 @(ex_intro ?? c) % // ]
+ ]
+ | @(ex_intro ?? (mk_config ?? atm2 (mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs))))
+ %
+ [ %
+ [ whd in ⊢ (??%?); >atml_q0_q2 //
+ | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
+ % // % //
+ ]
+ | #Hfalse @False_ind @(absurd ?? Hfalse) %
+ ]
+ ]
+]
+qed.