+lemma test_char_inv :
+ ∀sig.∀P:tape sig → Prop.∀f,t,t0.P t → Rtc_true sig f t t0 → P t0.
+#sig #P #f #t #t0 #HPt * #_ //
+qed.
+
+definition test_null ≝ λalpha.test_char alpha (λ_.true).
+
+definition R_test_null_true ≝ λalpha,t1,t2.
+ current alpha t1 ≠ None ? ∧ t1 = t2.
+
+definition R_test_null_false ≝ λalpha,t1,t2.
+ current alpha t1 = None ? ∧ t1 = t2.
+
+lemma sem_test_null : ∀alpha.
+ test_null alpha ⊨ [ tc_true : R_test_null_true alpha, R_test_null_false alpha].
+#alpha #t1 cases (sem_test_char alpha (λ_.true) t1) #k * #outc * * #Hloop #Htrue
+#Hfalse %{k} %{outc} % [ %
+[ @Hloop
+| #Houtc cases (Htrue ?) [| @Houtc] * #c * #Hcurt1 #_ #Houtc1 %
+ [ >Hcurt1 % #H destruct (H) | <Houtc1 % ] ]
+| #Houtc cases (Hfalse ?) [| @Houtc] #Habsurd #Houtc %
+ [ cases (current alpha t1) in Habsurd; // #c1 #Habsurd
+ lapply (Habsurd ? (refl ??)) #H destruct (H)
+ | <Houtc % ] ]
+qed.
+
+(************************************* swap ***********************************)
+definition swap_states : FinSet → FinSet ≝
+ λalpha:FinSet.FinProd (initN 4) alpha.
+
+definition swap0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)).
+definition swap1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
+definition swap2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
+definition swap3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
+
+definition swap_r ≝
+ λalpha:FinSet.λfoo:alpha.
+ mk_TM alpha (swap_states alpha)
+ (λp.let 〈q,a〉 ≝ p in
+ let 〈q',b〉 ≝ q in
+ let q' ≝ pi1 nat (λi.i<4) q' in
+ match a with
+ [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
+ | Some a' ⇒
+ match q' with
+ [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',R〉 (* save in register and move R *)
+ | S q' ⇒ match q' with
+ [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,L〉 (* swap with register and move L *)
+ | S q' ⇒ match q' with
+ [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
+ | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
+ ]
+ ]
+ ]])
+ 〈swap0,foo〉
+ (λq.\fst q == swap3).
+
+definition Rswap_r ≝
+ λalpha,t1,t2.
+ (∀b,ls.
+ t1 = midtape alpha ls b [ ] →
+ t2 = rightof ? b ls) ∧
+ (∀a,b,ls,rs.
+ t1 = midtape alpha ls b (a::rs) →
+ t2 = midtape alpha ls a (b::rs)).
+
+lemma sem_swap_r : ∀alpha,foo.
+ swap_r alpha foo ⊨ Rswap_r alpha.
+#alpha #foo *
+ [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
+ % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
+ |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
+ % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
+ |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
+ % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
+ | #lt #c #rt @(ex_intro ?? 4) cases rt
+ [@ex_intro [|% [ % | %
+ [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
+ |#r0 #rt0 @ex_intro [| % [ % | %
+ [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
+ ]
+ ]
+qed.
+
+definition swap_l ≝
+ λalpha:FinSet.λfoo:alpha.
+ mk_TM alpha (swap_states alpha)
+ (λp.let 〈q,a〉 ≝ p in
+ let 〈q',b〉 ≝ q in
+ let q' ≝ pi1 nat (λi.i<4) q' in
+ match a with
+ [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
+ | Some a' ⇒
+ match q' with
+ [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',L〉 (* save in register and move L *)
+ | S q' ⇒ match q' with
+ [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,R〉 (* swap with register and move R *)
+ | S q' ⇒ match q' with
+ [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
+ | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
+ ]
+ ]
+ ]])
+ 〈swap0,foo〉
+ (λq.\fst q == swap3).
+
+definition Rswap_l ≝
+ λalpha,t1,t2.
+ (∀b,rs.
+ t1 = midtape alpha [ ] b rs →
+ t2 = leftof ? b rs) ∧
+ (∀a,b,ls,rs.
+ t1 = midtape alpha (a::ls) b rs →
+ t2 = midtape alpha (b::ls) a rs).
+
+lemma sem_swap_l : ∀alpha,foo.
+ swap_l alpha foo ⊨ Rswap_l alpha.
+#alpha #foo *
+ [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
+ % [% |% [#b #rs | #a #b #ls #rs] #H destruct]
+ |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
+ % [% | % [#b #rs | #a #b #ls #rs] #H destruct]
+ |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
+ % [% |% [#b #rs | #a #b #ls #rs] #H destruct]
+ | #lt #c #rt @(ex_intro ?? 4) cases lt
+ [@ex_intro [|% [ % | %
+ [#b #rs #H destruct normalize // |#a #b #ls #rs #H destruct]]]
+ |#r0 #rt0 @ex_intro [| % [ % | %
+ [#b #rs #H destruct | #a #b #ls #rs #H destruct normalize //
+ ]
+ ]
+qed.
\ No newline at end of file