- t1 = midtape alpha ls c rs →
- t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
+ t1 = midtape alpha ls c rs →
+ t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
+(*
+ (current ? t1 = None ? ∧ t1 = t2) ∨
+ ∃ls,c,rs.
+ t1 = midtape alpha ls c rs ∧
+ t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).*)
[ O ⇒ 〈move1,Some ? 〈a',L〉〉
| S q ⇒ 〈move1,None ?〉 ] ])
move0 (λq.q == move1).
[ O ⇒ 〈move1,Some ? 〈a',L〉〉
| S q ⇒ 〈move1,None ?〉 ] ])
move0 (λq.q == move1).
lemma tc_q0_q1 :
∀alpha,test,ls,a0,rs. test a0 = true →
lemma tc_q0_q1 :
∀alpha,test,ls,a0,rs. test a0 = true →
- @(ex_intro ?? (mk_config ?? tc_true (niltape ?))) %
- [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
-| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_true (leftof ? a al)))
- % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
-| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_true (rightof ? a al)))
- % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
+ @(ex_intro ?? (mk_config ?? tc_false (niltape ?))) %
+ [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
+| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (leftof ? a al)))
+ % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
+| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (rightof ? a al)))
+ % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
| #ls #c #rs @(ex_intro ?? 2)
cases (true_or_false (test c)) #Htest
[ @(ex_intro ?? (mk_config ?? tc_true ?))
[| %
[ %
[ whd in ⊢ (??%?); >tc_q0_q1 //
| #ls #c #rs @(ex_intro ?? 2)
cases (true_or_false (test c)) #Htest
[ @(ex_intro ?? (mk_config ?? tc_true ?))
[| %
[ %
[ whd in ⊢ (??%?); >tc_q0_q1 //
(************************************* swap ***********************************)
definition swap_states : FinSet → FinSet ≝
λalpha:FinSet.FinProd (initN 4) alpha.
(************************************* swap ***********************************)
definition swap_states : FinSet → FinSet ≝
λalpha:FinSet.FinProd (initN 4) alpha.
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 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 …)).
- ∀a,b,ls,rs.
- t1 = midtape alpha ls b (a::rs) →
- t2 = midtape alpha ls a (b::rs).
+ (∀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 : ∀alpha,foo.
- swap alpha foo ⊨ Rswap alpha.
+lemma sem_swap_r : ∀alpha,foo.
+ swap_r alpha foo ⊨ Rswap_r alpha.
- [@ex_intro [|% [ % | #a #b #ls #rs #H destruct]]
- |#r0 #rt0 @ex_intro [| % [ % | #a #b #ls #rs #H destruct //
+ [@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 //
- ∀a,b,ls,rs.
- t1 = midtape alpha (a::ls) b rs →
- t2 = midtape alpha (b::ls) a rs.
+ (∀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_r : ∀alpha,foo.
- swap_r alpha foo ⊨ Rswap_r alpha.
+lemma sem_swap_l : ∀alpha,foo.
+ swap_l alpha foo ⊨ Rswap_l alpha.
- [@ex_intro [|% [ % | #a #b #ls #rs #H destruct]]
- |#l0 #lt0 @ex_intro [| % [ % | #a #b #ls #rs #H destruct //
+ [@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 //