Closed all axioms in turing (but not universal).

Revised semantics of basic machines for termination
purposes

diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma
index 56a0bf4b144a4396cc375239f5b1a3aa18404b11..1c1ce3020b824d3c37c1bb48f7581c060deec56f 100644 (file)
--- a/matita/matita/lib/turing/basic_machines.ma
+++ b/matita/matita/lib/turing/basic_machines.ma
@@ -50,22 +50,28 @@ definition move_r ≝
   move0 (λq.q == move1).
   
 definition R_move_r ≝ λalpha,t1,t2.
+  (current ? t1 = None ? → t1 = t2) ∧  
   ∀ls,c,rs.
-  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).*)
     
 lemma sem_move_r :
   ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
 #alpha #intape @(ex_intro ?? 2) cases intape
 [ @ex_intro
-  [| % [ % | #ls #c #rs #Hfalse destruct ] ]
+  [| % [ % | % // #ls #c #rs #H destruct ] ]
 |#a #al @ex_intro
-  [| % [ % | #ls #c #rs #Hfalse destruct ] ]
+  [| % [ % | % // #ls #c #rs #H destruct ] ]
 |#a #al @ex_intro
-  [| % [ % | #ls #c #rs #Hfalse destruct ] ]
+  [| % [ % | % // #ls #c #rs #H destruct ] ]
 | #ls #c #rs
-  @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
-  cases rs0 // ] ] ]
+  @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct]
+  #ls1 #c1 #rs1 #H destruct cases rs1 // ] ] ]
 qed.
 
 (******************** moves the head one step to the left *********************)
@@ -79,24 +85,25 @@ definition move_l ≝
       [ O ⇒ 〈move1,Some ? 〈a',L〉〉
       | S q ⇒ 〈move1,None ?〉 ] ])
   move0 (λq.q == move1).
-  
+
 definition R_move_l ≝ λalpha,t1,t2.
+  (current ? t1 = None ? → t1 = t2) ∧  
   ∀ls,c,rs.
-  t1 = midtape alpha ls c rs → 
-  t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
+    t1 = midtape alpha ls c rs → 
+    t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
     
 lemma sem_move_l :
   ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
 #alpha #intape @(ex_intro ?? 2) cases intape
 [ @ex_intro
-  [| % [ % | #ls #c #rs #Hfalse destruct ] ]
+  [| % [ % | % // #ls #c #rs #H destruct ] ]
 |#a #al @ex_intro
-  [| % [ % | #ls #c #rs #Hfalse destruct ] ]
+  [| % [ % | % // #ls #c #rs #H destruct ] ]
 |#a #al @ex_intro
-  [| % [ % | #ls #c #rs #Hfalse destruct ] ]
+  [| % [ % | % // #ls #c #rs #H destruct ] ]
 | #ls #c #rs
-  @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
-  cases ls0 // ] ] ]
+  @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct]
+  #ls1 #c1 #rs1 #H destruct cases ls1 // ] ] ]
 qed.
 
 (********************************* test char **********************************)
@@ -118,7 +125,7 @@ definition test_char ≝
   mk_TM alpha tc_states
   (λp.let 〈q,a〉 ≝ p in
    match a with
-   [ None ⇒ 〈tc_true, None ?〉
+   [ None ⇒ 〈tc_false, None ?〉
    | Some a' ⇒ 
      match test a' with
      [ true ⇒ 〈tc_true,None ?〉
@@ -127,11 +134,11 @@ definition test_char ≝
 
 definition Rtc_true ≝ 
   λalpha,test,t1,t2.
-   ∀c. current alpha t1 = Some ? c → test c = true ∧ t2 = t1.
+   (∃c. current alpha t1 = Some ? c ∧ test c = true) ∧ t2 = t1.
    
 definition Rtc_false ≝ 
   λalpha,test,t1,t2.
-    ∀c. current alpha t1 = Some ? c → test c = false ∧ t2 = t1.
+    (∀c. current alpha t1 = Some ? c → test c = false) ∧ t2 = t1.
      
 lemma tc_q0_q1 :
   ∀alpha,test,ls,a0,rs. test a0 = true → 
@@ -159,19 +166,19 @@ lemma sem_test_char :
     tc_true (Rtc_true alpha test) (Rtc_false alpha test).
 #alpha #test *
 [ @(ex_intro ?? 2)
-  @(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 //
-        | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ]
+        | #_ % // @(ex_intro … c) /2/]
       | * #Hfalse @False_ind @Hfalse % ]
     ]
   | @(ex_intro ?? (mk_config ?? tc_false (midtape ? ls c rs)))
@@ -179,7 +186,7 @@ lemma sem_test_char :
     [ %
       [ whd in ⊢ (??%?); >tc_q0_q2 //
       | whd in ⊢ ((??%%)→?); #Hfalse destruct (Hfalse) ]
-    | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) //
+    | #_ % // #c0 whd in ⊢ ((??%?)→?); #Hc0 destruct (Hc0) //
     ]
   ]
 ]
@@ -215,25 +222,30 @@ definition swap_r ≝
   ]])
   〈swap0,foo〉
   (λq.\fst q == swap3).
-
-definition Rswap ≝ 
+  
+definition Rswap_r ≝ 
   λalpha,t1,t2.
-   ∀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_r : ∀alpha,foo.
-  swap_r alpha foo ⊨ Rswap alpha. 
+  swap_r alpha foo ⊨ Rswap_r alpha. 
 #alpha #foo *
   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
-   % [% |#a #b #ls #rs #H destruct]
+   % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
   |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
-   % [% |#a #b #ls #rs #H destruct] 
+   % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
   |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
-   % [% |#a #b #ls #rs #H destruct] 
+   % [% |% [#b #ls | #a #b #ls #rs] #H destruct] 
   | #lt #c #rt @(ex_intro ?? 4) cases rt
-    [@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 //
     ]
   ]
 qed.
@@ -262,22 +274,27 @@ definition swap_l ≝
 
 definition Rswap_l ≝ 
   λalpha,t1,t2.
-   ∀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_l : ∀alpha,foo.
   swap_l alpha foo ⊨ Rswap_l alpha. 
 #alpha #foo *
   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
-   % [% |#a #b #ls #rs #H destruct]
+   % [% |% [#b #rs | #a #b #ls #rs] #H destruct]
   |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
-   % [% |#a #b #ls #rs #H destruct] 
+   % [% | % [#b #rs | #a #b #ls #rs] #H destruct]
   |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
-   % [% |#a #b #ls #rs #H destruct] 
+   % [% |% [#b #rs | #a #b #ls #rs] #H destruct] 
   | #lt #c #rt @(ex_intro ?? 4) cases lt
-    [@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 //
     ]
   ]
-qed.
\ No newline at end of file
+qed.

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index e117fc7be167bf4bb034fc0d4c84d06ca31ee2dc..0fcbfbe480d5d6cc8db8389c8141daa0dca8cde0 100644 (file)
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -47,6 +47,19 @@ definition mk_tape :
       | cons r0 rs0 ⇒ leftof ? r0 rs0 ]
     | cons l0 ls0 ⇒ rightof ? l0 ls0 ] ].
 
+lemma current_to_midtape: ∀sig,t,c. current sig t = Some ? c →
+  ∃ls,rs. t = midtape ? ls c rs.
+#sig *
+  [#c whd in ⊢ ((??%?)→?); #Hfalse destruct
+  |#a #l #c whd in ⊢ ((??%?)→?); #Hfalse destruct
+  |#a #l #c whd in ⊢ ((??%?)→?); #Hfalse destruct
+  |#ls #a #rs #c whd in ⊢ ((??%?)→?); #H destruct 
+   @(ex_intro … ls) @(ex_intro … rs) //
+  ]
+qed.
+
+(*********************************** moves ************************************)
+
 inductive move : Type[0] ≝
   | L : move | R : move | N : move.
 

diff --git a/matita/matita/lib/turing/move_char.ma b/matita/matita/lib/turing/move_char.ma
index a0bf18996055e573c3f4e08c46b4f101eefe6fe7..e20591c5f607b725b2b6d4cd0a6038c3834c8fd2 100644 (file)
--- a/matita/matita/lib/turing/move_char.ma
+++ b/matita/matita/lib/turing/move_char.ma
@@ -35,17 +35,20 @@ definition mcr_step ≝ λalpha:FinSet.λsep:alpha.
      (single_finalTM … (swap_l alpha sep · move_r ?)) (nop ?) tc_true.
 
 definition Rmcr_step_true ≝ 
-  λalpha,sep,t1,t2.
-   ∀a,b,ls,rs.  
-    t1 = midtape alpha (a::ls) b rs → 
-    b ≠ sep ∧
-    t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs).
+  λalpha,sep,t1,t2. 
+   ∃b. b ≠ sep ∧
+    ((∃a,ls,rs.
+       t1 = midtape alpha (a::ls) b rs ∧
+       t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs)) ∨
+     (∃rs.
+       t1 = midtape alpha [ ] b rs ∧
+       t2 = leftof alpha b rs)).
 
 definition Rmcr_step_false ≝ 
   λalpha,sep,t1,t2.
     left ? t1 ≠ [] →  current alpha t1 ≠ None alpha → 
       current alpha t1 = Some alpha sep ∧ t2 = t1.
-    
+      
 lemma sem_mcr_step :
   ∀alpha,sep.
   mcr_step alpha sep ⊨ 
@@ -53,18 +56,25 @@ lemma sem_mcr_step :
 #alpha #sep 
   @(acc_sem_if_app … 
      (sem_test_char …) (sem_seq …(sem_swap_l …) (sem_move_r …)) (sem_nop …))
-  [#intape #outtape #tapea whd in ⊢ (%→%→%);
-   #Htapea * #tapeb * whd in ⊢ (%→%→?);
-   #Htapeb #Houttape #a #b #ls #rs #Hintape
-   >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea
-   #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))]
-   @Houttape @Htapeb //
+  [#intape #outtape #tapea whd in ⊢ (%→%→%); * * #c *
+   #Hcur cases (current_to_midtape … Hcur) #ls * #rs #Hintape
+   #csep #Htapea * #tapeb * #Hswap #Hmove @(ex_intro … c) %
+    [@(\Pf (injective_notb ? false csep))]
+   generalize in match Hintape; -Hintape cases ls
+    [#Hintape %2 @(ex_intro …rs) % //
+     >Htapea in Hswap; >Hintape
+     whd in ⊢ (%→?); * #Hswap #_ >(Hswap … (refl …)) in Hmove;
+     whd in ⊢ (%→?); * #Hmove #_ >Hmove //
+    |#a #ls1 #Hintape %1
+     @(ex_intro … a) @(ex_intro … ls1) @(ex_intro … rs) % //
+     @(proj2 … Hmove) @(proj2 … Hswap) >Htapea //
+    ]
   |#intape #outtape #tapea whd in ⊢ (%→%→%);
    cases (current alpha intape) 
     [#_ #_ #_ * #Hfalse @False_ind @Hfalse %
-    |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % //
+    |#c * #H1 #H2 #Htapea #_ #_ % // lapply (H1 c (refl …)) #csep 
      lapply (injective_notb ? true csep) -csep #csep >(\P csep) //
-    ]
+    ]   
   ]
 qed.
 
@@ -79,7 +89,7 @@ definition R_move_char_r ≝
     (∀rs1,rs2.rs = rs1@sep::rs2 → 
      b ≠ sep → memb ? sep rs1 = false → 
      t2 = midtape alpha (a::reverse ? rs1@b::ls) sep rs2).
-    
+
 lemma sem_move_char_r :
   ∀alpha,sep.
   WRealize alpha (move_char_r alpha sep) (R_move_char_r alpha sep).
@@ -96,62 +106,67 @@ lapply (sem_while … (sem_mcr_step alpha sep) inc i outc Hloop) [%]
     |*:% #H2 normalize in H2; destruct (H2) ]
   ]
 | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
-  lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
-  #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
-  #Ha0 #Htapeb %
-  [ #Hfalse @False_ind @(absurd ?? Ha0) //
-  | *
-    [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ (* normalize *)
-      >Hrs in Htapeb; #Htapeb normalize in Htapeb;
-      cases (IH … Htapeb) #Houtc #_ >Houtc normalize // 
-    | #r0 #rs0 #rs2 #Hrs #_ #Hrs0
+  lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%); #IH
+  #b0 #a0 #ls #rs #Htapea cases Hstar1 #b * #bsep *
+  [* #a * #ls1 * #rs1 * >Htapea #H destruct (H) #Htapeb %
+    [#Hb @False_ind /2/
+    |* (* by cases on rs1 *)
+      [#rs2 whd in ⊢ (???%→?); #Hrs #_ #_ (* normalize *)
+       >Hrs in Htapeb; #Htapeb normalize in Htapeb;
+       cases (IH … Htapeb) #Houtc #_ >Houtc normalize // 
+     |#r0 #rs0 #rs2 #Hrs #_ #Hrs0
       cut (r0 ≠ sep ∧ memb … sep rs0 = false)
-      [ %
-         [ % #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct
-         | whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse
-           [ destruct
-           | @Hfalse ]
-         ]
-      ] *
+       [%
+         [% #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct
+         |whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse
+           [ destruct | @Hfalse ]]
+         ] *
       #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb;
       normalize in ⊢ (%→?); #Htapeb
       cases (IH … Htapeb) -IH #_ #IH 
       >reverse_cons >associative_append @IH //
-    ]
-  ]
+     ]
+   ]
+ |* #rs1 * >Htapea #H destruct (H)
+ ]
 qed.
 
-lemma terminate_move_char_r :
-  ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha (a::ls) b rs →  
-  (b = sep ∨ memb ? sep rs = true) → Terminate alpha (move_char_r alpha sep) t.
-#alpha #sep #t #b #a #ls #rs #Ht #Hsep
-@(terminate_while … (sem_mcr_step alpha sep))
-  [%
-  |generalize in match Hsep; -Hsep
-   generalize in match Ht; -Ht
-   generalize in match ls; -ls
-   generalize in match a; -a
-   generalize in match b; -b
-   generalize in match t; -t
-   elim rs 
-    [#t #b #a #ls #Ht #Hsep % #tinit 
-     whd in ⊢ (%→?); #H @False_ind
-     cases (H … Ht) #Hb #_ cases Hb #eqb @eqb 
-     cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
-    |#r0 #rs0 #Hind #t #b #a #ls #Ht #Hsep % #tinit
-     whd in ⊢ (%→?); #H 
-     cases (H … Ht) #Hbsep #Htinit
-     @(Hind … Htinit) cases Hsep 
-      [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
-        [#eqsep %1 >(\P eqsep) // | #H %2 //]
-  ]
+lemma WF_mcr_niltape:
+  ∀alpha,sep. WF ? (inv ? (Rmcr_step_true alpha sep)) (niltape alpha).
+#alpha #sep @wf #t1 whd in ⊢ (%→?); * #b * #_ * 
+  [* #a * #ls * #rs * #H destruct | * #rs * #H destruct ]
+qed.
+
+lemma WF_mcr_rightof:
+  ∀alpha,sep,a,ls. WF ? (inv ? (Rmcr_step_true alpha sep)) (rightof alpha a ls).
+#alpha #sep #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ * 
+  [* #a * #ls * #rs * #H destruct | * #rs * #H destruct ]
 qed.
 
-(* NO GOOD: we must stop if current = None too!!! *)
+lemma WF_mcr_leftof:
+  ∀alpha,sep,a,rs. WF ? (inv ? (Rmcr_step_true alpha sep)) (leftof alpha a rs).
+#alpha #sep #a #rs @wf #t1 whd in ⊢ (%→?); * #b * #_ * 
+  [* #a * #ls * #rs * #H destruct | * #rs * #H destruct ]
+qed.
 
-axiom ssem_move_char_r :
+lemma terminate_move_char_r :
+  ∀alpha,sep.∀t. Terminate alpha (move_char_r alpha sep) t.
+#alpha #sep #t @(terminate_while … (sem_mcr_step alpha sep)) [%]
+cases t // #ls #c #rs generalize in match ls; generalize in match c; elim rs 
+  [#c1 #l1 @wf #t1 whd in ⊢ (%→?); * #b * #bsep *
+    [* #a * #ls1 * #rs1 * #H destruct #Ht1 >Ht1 //
+    |* #rs1 * #_ #Ht1 >Ht1 //
+    ]
+  |#a #ls1 #Hind #c1 #l1 @wf #t1 whd in ⊢ (%→?); * #b * #bsep *
+    [* #a * #ls1 * #rs1 * #H destruct whd in ⊢ ((???%)→?); #Ht1 >Ht1 @Hind
+    |* #rs1 * #_ #Ht1 >Ht1 //
+    ]
+qed.
+
+lemma ssem_move_char_r :
   ∀alpha,sep.
   Realize alpha (move_char_r alpha sep) (R_move_char_r alpha sep).
+/2/ qed.
 
 
 (******************************* move_char_l **********************************)
@@ -173,51 +188,57 @@ Final state = 〈4,#〉
 
 *)
 
-include "turing/basic_machines.ma".
-include "turing/if_machine.ma".
-
 definition mcl_step ≝ λalpha:FinSet.λsep:alpha.
   ifTM alpha (test_char ? (λc.¬c==sep))
      (single_finalTM … (swap_r alpha sep · move_l ?)) (nop ?) tc_true.
-     
-definition Rmcl_step_true ≝ 
-  λalpha,sep,t1,t2.
-   ∀a,b,ls,rs.  
-    t1 = midtape alpha ls b (a::rs) → 
-    b ≠ sep ∧
-    t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a::b::rs).
 
+definition Rmcl_step_true ≝ 
+  λalpha,sep,t1,t2. 
+   ∃b. b ≠ sep ∧
+    ((∃a,ls,rs.
+       t1 = midtape alpha ls b (a::rs) ∧
+       t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a::b::rs)) ∨
+     (∃ls.
+       t1 = midtape alpha ls b [ ] ∧
+       t2 = rightof alpha b ls)).
+       
 definition Rmcl_step_false ≝ 
   λalpha,sep,t1,t2.
     right ? t1 ≠ [] →  current alpha t1 ≠ None alpha → 
       current alpha t1 = Some alpha sep ∧ t2 = t1.
-
+      
 definition mcls_acc: ∀alpha:FinSet.∀sep:alpha.states ? (mcl_step alpha sep)
  ≝ λalpha,sep.inr … (inl … (inr … start_nop)).
 
 lemma sem_mcl_step :
   ∀alpha,sep.
   mcl_step alpha sep ⊨ 
-    [mcls_acc alpha sep: Rmcl_step_true alpha sep, Rmcl_step_false alpha sep].
+    [mcls_acc ??: Rmcl_step_true alpha sep, Rmcl_step_false alpha sep].  
 #alpha #sep 
-@(acc_sem_if_app … 
-  (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_l …)) (sem_nop …))
-  [#intape #outtape #tapea whd in ⊢ (%→%→%);
-   #Htapea * #tapeb * whd in ⊢ (%→%→?);
-   #Htapeb #Houttape #a #b #ls #rs #Hintape
-   >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea
-   #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))]
-   @Houttape @Htapeb //
+  @(acc_sem_if_app … 
+     (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_l …)) (sem_nop …))
+  [#intape #outtape #tapea whd in ⊢ (%→%→%); * * #c *
+   #Hcur cases (current_to_midtape … Hcur) #ls * #rs #Hintape
+   #csep #Htapea * #tapeb * #Hswap #Hmove @(ex_intro … c) %
+    [@(\Pf (injective_notb ? false csep))]
+   generalize in match Hintape; -Hintape cases rs
+    [#Hintape %2 @(ex_intro …ls) % //
+     >Htapea in Hswap; >Hintape
+     whd in ⊢ (%→?); * #Hswap #_ >(Hswap … (refl …)) in Hmove;
+     whd in ⊢ (%→?); * #Hmove #_ >Hmove //
+    |#a #rs1 #Hintape %1
+     @(ex_intro … a) @(ex_intro … ls) @(ex_intro … rs1) % //
+     @(proj2 … Hmove) @(proj2 … Hswap) >Htapea //
+    ]
   |#intape #outtape #tapea whd in ⊢ (%→%→%);
    cases (current alpha intape) 
     [#_ #_ #_ * #Hfalse @False_ind @Hfalse %
-    |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % //
+    |#c * #H1 #H2 #Htapea #_ #_ % // lapply (H1 c (refl …)) #csep 
      lapply (injective_notb ? true csep) -csep #csep >(\P csep) //
-    ]
+    ]   
   ]
 qed.
-    
-(* the move_char (variant left) machine *)
+
 definition move_char_l ≝ 
   λalpha,sep.whileTM alpha (mcl_step alpha sep) (inr … (inl … (inr … start_nop))).
 
@@ -228,7 +249,7 @@ definition R_move_char_l ≝
     (∀ls1,ls2.ls = ls1@sep::ls2 → 
      b ≠ sep → memb ? sep ls1 = false → 
      t2 = midtape alpha ls2 sep (a::reverse ? ls1@b::rs)).
-    
+     
 lemma sem_move_char_l :
   ∀alpha,sep.
   WRealize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
@@ -238,73 +259,72 @@ lapply (sem_while … (sem_mcl_step alpha sep) inc i outc Hloop) [%]
 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
   %
   [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
-   [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2) ]
+    [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)]
   | #rs1 #rs2 #Hrs #Hb #Hrs1 
-    >Htapea in H1; (* normalize in ⊢ (% → ?); *) #H1 cases (H1 ??)
-    [ #Hfalse normalize in Hfalse; @False_ind @(absurd ?? Hb) destruct %
-    |*:% normalize #H2 destruct (H2) ]
+    >Htapea in H1; #H1 cases (H1 ??)
+    [#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
+    |*:% #H2 normalize in H2; destruct (H2) ]
   ]
 | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
-  lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
-  #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
-  #Ha0 #Htapeb %
-  [ #Hfalse @False_ind @(absurd ?? Ha0) //
-  | *
-    [ #ls2 whd in ⊢ (???%→?); #Hls #_ #_
-      >Hls in Htapeb; #Htapeb normalize in Htapeb;
-      cases (IH … Htapeb) #Houtc #_ >Houtc normalize // 
-    | #l0 #ls0 #ls2 #Hls #_ #Hls0
-      cut (l0 ≠ sep ∧ memb … sep ls0 = false)
-      [ %
-         [ % #Hl0 >Hl0 in Hls0; >memb_hd #Hfalse destruct
-         | whd in Hls0:(??%?); cases (sep==l0) in Hls0; normalize #Hfalse
-           [ destruct
-           | @Hfalse ]
-         ]
-      ] *
-      #Hl0 -Hls0 #Hls0 >Hls in Htapeb;
+  lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%); #IH
+  #b0 #a0 #ls #rs #Htapea cases Hstar1 #b * #bsep *
+  [* #a * #ls1 * #rs1 * >Htapea #H destruct (H) #Htapeb %
+    [#Hb @False_ind /2/
+    |* (* by cases on ls1 *)
+      [#rs2 whd in ⊢ (???%→?); #Hrs #_ #_ (* normalize *)
+       >Hrs in Htapeb; #Htapeb normalize in Htapeb;
+       cases (IH … Htapeb) #Houtc #_ >Houtc normalize // 
+     |#r0 #rs0 #rs2 #Hrs #_ #Hrs0
+      cut (r0 ≠ sep ∧ memb … sep rs0 = false)
+       [%
+         [% #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct
+         |whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse
+           [ destruct | @Hfalse ]]
+         ] *
+      #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb;
       normalize in ⊢ (%→?); #Htapeb
       cases (IH … Htapeb) -IH #_ #IH 
       >reverse_cons >associative_append @IH //
-    ]
-  ]
+     ]
+   ]
+ |* #rs1 * >Htapea #H destruct (H)
+ ]
 qed.
 
-lemma terminate_move_char_l :
-  ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha ls b (a::rs) → 
-  (b = sep ∨ memb ? sep ls = true) → Terminate alpha (move_char_l alpha sep) t.
-#alpha #sep #t #b #a #ls #rs #Ht #Hsep
-@(terminate_while … (sem_mcl_step alpha sep))
-  [%
-  |generalize in match Hsep; -Hsep
-   generalize in match Ht; -Ht
-   generalize in match rs; -rs
-   generalize in match a; -a
-   generalize in match b; -b
-   generalize in match t; -t
-   elim ls 
-    [#t #b #a #rs #Ht #Hsep % #tinit 
-     whd in ⊢ (%→?); #H @False_ind
-     cases (H … Ht) #Hb #_ cases Hb #eqb @eqb 
-     cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
-    |#l0 #ls0 #Hind #t #b #a #rs #Ht #Hsep % #tinit
-     whd in ⊢ (%→?); #H 
-     cases (H … Ht) #Hbsep #Htinit
-     @(Hind … Htinit) cases Hsep 
-      [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
-        [#eqsep %1 >(\P eqsep) // | #H %2 //]
-  ]
+lemma WF_mcl_niltape:
+  ∀alpha,sep. WF ? (inv ? (Rmcl_step_true alpha sep)) (niltape alpha).
+#alpha #sep @wf #t1 whd in ⊢ (%→?); * #b * #_ * 
+  [* #a * #ls * #rs * #H destruct | * #rs * #H destruct ]
 qed.
 
-(* NO GOOD: we must stop if current = None too!!! 
-lemma ssem_move_char_l :
-  ∀alpha,sep.
-  Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
-#alpha #sep *
-[ %{5} % [| % [whd in ⊢ (??%?);
- @WRealize_to_Realize // @terminate_move_char_l
-*)
+lemma WF_mcl_rightof:
+  ∀alpha,sep,a,ls. WF ? (inv ? (Rmcl_step_true alpha sep)) (rightof alpha a ls).
+#alpha #sep #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ * 
+  [* #a * #ls * #rs * #H destruct | * #rs * #H destruct ]
+qed.
+
+lemma WF_mcl_leftof:
+  ∀alpha,sep,a,rs. WF ? (inv ? (Rmcl_step_true alpha sep)) (leftof alpha a rs).
+#alpha #sep #a #rs @wf #t1 whd in ⊢ (%→?); * #b * #_ * 
+  [* #a * #ls * #rs * #H destruct | * #rs * #H destruct ]
+qed.
+
+lemma terminate_move_char_l :
+  ∀alpha,sep.∀t. Terminate alpha (move_char_l alpha sep) t.
+#alpha #sep #t @(terminate_while … (sem_mcl_step alpha sep)) [%]
+cases t // #ls elim ls 
+  [#c1 #l1 @wf #t1 whd in ⊢ (%→?); * #b * #bsep *
+    [* #a * #ls1 * #rs1 * #H destruct #Ht1 >Ht1 //
+    |* #rs1 * #_ #Ht1 >Ht1 //
+    ]
+  |#a #ls1 #Hind #c1 #l1 @wf #t1 whd in ⊢ (%→?); * #b * #bsep *
+    [* #a * #ls1 * #rs1 * #H destruct whd in ⊢ ((???%)→?); #Ht1 >Ht1 @Hind
+    |* #rs1 * #_ #Ht1 >Ht1 //
+    ]
+qed.
 
-axiom ssem_move_char_l :
+lemma ssem_move_char_l:
   ∀alpha,sep.
   Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
+/2/ qed.
+