From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 8 Aug 2012 12:09:51 +0000 (+0000)
Subject: Adding GRealize to uni_step.
X-Git-Tag: make_still_working~1564
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5535cd4e08fd8d1e7e6e067eac1bb6c1bf8fcbbf;p=helm.git

Adding GRealize to uni_step.
---

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index 8b6a79be5..36b5fc2a3 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -62,6 +62,11 @@ definition inv ≝ λA.λR:relation A.λa,b.R b a.
 definition subR ≝ λA.λR,S:relation A.(∀a,b. R a b → S a b).
 interpretation "relation inclusion" 'subseteq R S = (subR ? R S).
 
+lemma sub_reflexive : 
+  ∀T.∀R:relation T.R ⊆ R.
+#T #R #x //
+qed.
+
 lemma sub_comp_l:  ∀A.∀R,R1,R2:relation A.
   R1 ⊆ R2 → R1 ∘ R ⊆ R2 ∘ R.
 #A #R #R1 #R2 #Hsub #a #b * #c * /4/
diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma
index 1c1ce3020..9790cb43c 100644
--- a/matita/matita/lib/turing/basic_machines.ma
+++ b/matita/matita/lib/turing/basic_machines.ma
@@ -192,6 +192,11 @@ lemma sem_test_char :
 ]
 qed.
 
+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.
+
 (************************************* swap ***********************************)
 definition swap_states : FinSet → FinSet ≝ 
   λalpha:FinSet.FinProd (initN 4) alpha.
diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma
index 6248ab7e7..f778ff308 100644
--- a/matita/matita/lib/turing/if_machine.ma
+++ b/matita/matita/lib/turing/if_machine.ma
@@ -236,6 +236,7 @@ lemma sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,acc.
 qed.
  
 (* we can probably use acc_sem_if to prove sem_if *)
+(* for sure we can use acc_sem_if_guarded to prove acc_sem_if *)
 lemma acc_sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.
   M1 ⊨ [acc: Rtrue, Rfalse]  → M2 ⊨ R2 → M3 ⊨ R3 → 
   ifTM sig M1 (single_finalTM … M2) M3 acc ⊨
@@ -333,3 +334,117 @@ lemma acc_sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,R5,acc.
      |#H cases (Houtc1 H) #t3 * #Hleft #Hright @Hsub1 // ]
   |#H cases (Houtc2 H) #t3 * #Hleft #Hright @Hsub2 // ]
 qed.
+
+lemma sem_single_final_guarded: ∀sig.∀M: TM sig.∀Pre,R.
+  GRealize sig M Pre R → GRealize sig (single_finalTM sig M) Pre R.
+#sig #M #Pre #R #HR #intape #HPre 
+cases (sem_seq_guarded ??????? HR (Realize_to_GRealize ?? (λt.True) ? (sem_nop …)) ?? HPre) //
+#k * #outc * #Hloop * #ta * #Hta whd in ⊢ (%→?); #Houtc
+@(ex_intro ?? k) @(ex_intro ?? outc) %  [ @Hloop | >Houtc // ]
+qed.
+    
+lemma acc_sem_if_guarded: ∀sig,M1,M2,M3,P,P2,Rtrue,Rfalse,R2,R3,acc.
+  M1 ⊨ [acc: Rtrue, Rfalse]  → 
+  (GRealize ? M2 P2 R2) → (∀t,t0.P t → Rtrue t t0 → P2 t0) → 
+  M3 ⊨ R3 → 
+  accGRealize ? (ifTM sig M1 (single_finalTM … M2) M3 acc) 
+    (inr … (inl … (inr … start_nop))) P (Rtrue ∘ R2) (Rfalse ∘ R3).
+#sig #M1 #M2 #M3 #P #P2 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HP2 #HR3 #t #HPt 
+cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse 
+cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
+  [lapply (sem_single_final_guarded … HR2) -HR2 #HR2
+   cases (HR2 (ctape sig ? outc1) ?)
+   [|@HP2 [||@HMtrue @(\P Hacc)] // ]
+   #k2 * #outc2 * #Hloop2 #HM2
+   @(ex_intro … (k1+k2)) 
+   @(ex_intro … (lift_confR … (lift_confL … outc2))) %
+    [%
+      [@(loop_merge ?????????
+         (mk_config ? (states sig (ifTM sig M1 (single_finalTM … M2) M3 acc))
+          (inr (states sig M1) ? (inl ? (states sig M3) (start sig (single_finalTM sig M2)))) (ctape ?? outc1) )
+         ? 
+         (loop_lift ??? 
+          (lift_confL sig (states ? M1) (FinSum (states ? (single_finalTM … M2)) (states ? M3)))
+          (step sig M1) (step sig (ifTM sig M1 (single_finalTM ? M2) M3 acc)) 
+          (λc.halt sig M1 (cstate … c)) 
+          (λc.halt_liftL ?? (halt sig M1) (cstate … c)) 
+          … Hloop1))
+        [* *
+          [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
+          | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
+        |#c0 #Hhalt >(step_if_liftM1 … Hhalt) // 
+        |#x <p_halt_liftL %
+        |whd in ⊢ (??%?); >(config_expand ?? outc1);
+         whd in match (lift_confL ????);
+         >(trans_if_M1true_acc … Hacc) 
+          [% | @(loop_Some ?????? Hloop1)]
+        |cases outc1 #s1 #t1 %
+        |@(loop_lift ??? 
+           (λc.(lift_confR … (lift_confL sig (states ? (single_finalTM ? M2)) (states ? M3) c)))
+           … Hloop2) 
+          [ * #s2 #t2 %
+          | #c0 #Hhalt >(step_if_liftM2 … Hhalt) // ]
+        ]
+      |#_ @(ex_intro … (ctape ?? outc1)) % 
+        [@HMtrue @(\P Hacc) | >(config_expand ?? outc2) @HM2 ]
+      ]
+    |>(config_expand ?? outc2) whd in match (lift_confR ????);
+     * #H @False_ind @H @eq_f @eq_f >(config_expand ?? outc2)
+     @single_final // @(loop_Some ?????? Hloop2)
+    ]
+  |cases (HR3 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM3
+   @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confR … outc2))) %
+    [%
+      [@(loop_merge ?????????
+         (mk_config ? (states sig (ifTM sig M1 (single_finalTM … M2) M3 acc))
+          (inr (states sig M1) ? (inr (states sig (single_finalTM ? M2)) ? (start sig M3))) (ctape ?? outc1) )
+         ? 
+         (loop_lift ??? 
+          (lift_confL sig (states ? M1) (FinSum (states ? (single_finalTM … M2)) (states ? M3)))
+          (step sig M1) (step sig (ifTM sig M1 (single_finalTM ? M2) M3 acc)) 
+          (λc.halt sig M1 (cstate … c)) 
+          (λc.halt_liftL ?? (halt sig M1) (cstate … c)) 
+          … Hloop1))
+        [* *
+          [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
+          | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
+        |#c0 #Hhalt >(step_if_liftM1 … Hhalt) // 
+        |#x <p_halt_liftL %
+        |whd in ⊢ (??%?); >(config_expand ?? outc1);
+         whd in match (lift_confL ????);
+         >(trans_if_M1true_notacc … Hacc) 
+          [% | @(loop_Some ?????? Hloop1)]
+        |cases outc1 #s1 #t1 %
+        |@(loop_lift ??? 
+           (λc.(lift_confR … (lift_confR sig (states ? (single_finalTM ? M2)) (states ? M3) c)))
+           … Hloop2) 
+          [ * #s2 #t2 %
+          | #c0 #Hhalt >(step_if_liftM3 … Hhalt) // ]
+        ]
+      |>(config_expand ?? outc2) whd in match (lift_confR ????);
+       #H destruct (H) 
+      ]
+    |#_ @(ex_intro … (ctape ?? outc1)) % 
+      [@HMfalse @(\Pf Hacc) | >(config_expand ?? outc2) @HM3 ]
+    ]
+  ]
+qed.
+    
+lemma acc_sem_if_app_guarded: ∀sig,M1,M2,M3,P,P2,Rtrue,Rfalse,R2,R3,R4,R5,acc.
+  M1 ⊨ [acc: Rtrue, Rfalse] → 
+  (GRealize ? M2 P2 R2) → (∀t,t0.P t → Rtrue t t0 → P2 t0) → 
+  M3 ⊨ R3 → 
+  (∀t1,t2,t3. Rtrue t1 t3 → R2 t3 t2 → R4 t1 t2) → 
+  (∀t1,t2,t3. Rfalse t1 t3 → R3 t3 t2 → R5 t1 t2) → 
+  accGRealize ? (ifTM sig M1 (single_finalTM … M2) M3 acc) 
+    (inr … (inl … (inr … start_nop))) P R4 R5 .
+#sig #M1 #M2 #M3 #P #P2 #Rtrue #Rfalse #R2 #R3 #R4 #R5 #acc
+#HRacc #HRtrue #Hinv #HRfalse #Hsub1 #Hsub2 
+#t #HPt cases (acc_sem_if_guarded … HRacc HRtrue Hinv HRfalse t HPt)
+#k * #outc * * #Hloop #Houtc1 #Houtc2 @(ex_intro … k) @(ex_intro … outc)
+% [% [@Hloop
+     |#H cases (Houtc1 H) #t3 * #Hleft #Hright @Hsub1 // ]
+  |#H cases (Houtc2 H) #t3 * #Hleft #Hright @Hsub2 // ]
+qed.
+
+
diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 32bd28c87..37ce2f2de 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -292,6 +292,21 @@ lemma WRealize_to_GRealize : ∀sig.∀M: TM sig.∀Pre,R.
 @(ex_intro … i) @(ex_intro … outc) % // @(HW … i) //
 qed.
 
+lemma Realize_to_GRealize : ∀sig,M.∀P,R. 
+  M ⊨ R → GRealize sig M P R.
+#alpha #M #Pre #R #HR #t #HPre
+cases (HR t) -HR #k * #outc * #Hloop #HR 
+@(ex_intro ?? k) @(ex_intro ?? outc) % 
+  [ @Hloop | @HR ]
+qed.
+
+lemma acc_Realize_to_acc_GRealize: ∀sig,M.∀q:states sig M.∀P,R1,R2. 
+  M ⊨ [q:R1,R2] → accGRealize sig M q P R1 R2.
+#alpha #M #q #Pre #R1 #R2 #HR #t #HPre
+cases (HR t) -HR #k * #outc * * #Hloop #HRtrue #HRfalse 
+@(ex_intro ?? k) @(ex_intro ?? outc) % 
+  [ % [@Hloop] @HRtrue | @HRfalse]
+qed.
 
 (******************************** monotonicity ********************************)
 lemma Realize_to_Realize : ∀alpha,M,R1,R2.
diff --git a/matita/matita/lib/turing/universal/copy.ma b/matita/matita/lib/turing/universal/copy.ma
index 2367910ba..95216acdb 100644
--- a/matita/matita/lib/turing/universal/copy.ma
+++ b/matita/matita/lib/turing/universal/copy.ma
@@ -278,6 +278,16 @@ qed.
 
 axiom daemon : ∀P:Prop.P.
 
+lemma list_cases2_full : 
+  ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:Prop.
+  length ? l1 = length ? l2 →
+  (l1 = [] → l2 = [] → P) → 
+  (∀hd1,hd2,tl1,tl2.l1 = hd1::tl1 → l2 = hd2::tl2 → P) → P.
+#T1 #T2 #l1 #l2 #P #Hl @(list_ind2 … Hl)
+[ #Pnil #Pcons @Pnil //
+| #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
+qed.
+
 lemma wsem_copy0 : WRealize ? copy0 R_copy0.
 #intape #k #outc #Hloop 
 lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
@@ -299,7 +309,7 @@ lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
   cases (Htc … Htb) -Htc #Hcbitnull #Htc
   % [ % #Hc' >Hc' in Hcbitnull; normalize #Hfalse destruct (Hfalse) ]
   cut (|l1| = |reverse ? l4|) [>length_reverse @Hlen] #Hlen1
-  @(list_cases2 … Hlen1)
+  @(list_cases2_full … Hlen1)
   [ (* case l1 = [] is discriminated because l1 contains at least comma *)
     #Hl1nil @False_ind >Hl1nil in Hl1; cases l1' normalize
     [ #Hl1 destruct normalize in Hcbitnull; destruct (Hcbitnull)
@@ -501,7 +511,9 @@ definition option_cons ≝ λA.λa:option A.λl.
   [ None ⇒ l
   | Some a' ⇒ a'::l ].
 
-lemma sem_copy : Realize ? copy R_copy.
+
+axiom sem_copy : Realize ? copy R_copy.
+(*
 #intape 
 cases (sem_seq … (sem_copy0 …)
         (sem_seq … (sem_move_l …)
@@ -577,4 +589,5 @@ lapply (Hte (reverse ? (reverse ? l1@〈s1,false〉::l2)@[〈c1,false〉])
 >reverse_append >reverse_append >reverse_single >reverse_cons
 >reverse_append >reverse_append >reverse_reverse >reverse_reverse
 >reverse_single >associative_append >associative_append %
-qed.
\ No newline at end of file
+qed.
+*)
\ No newline at end of file
diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
index fc663ff2c..4761ce135 100644
--- a/matita/matita/lib/turing/universal/uni_step.ma
+++ b/matita/matita/lib/turing/universal/uni_step.ma
@@ -78,19 +78,19 @@ cases (sem_seq ????? (sem_mark ?)
 @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
 #ls #l #rs #c #d #Hnogrids #Hnomarks #Hintape
 cases HR -HR
-#ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta -Hintape #Hta
-* #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Htb -Hta 
+#ta * whd in ⊢ (%→?); * #Hta #_ lapply (Hta … Hintape) -Hta -Hintape #Hta
+* #tb * whd in ⊢ (%→?); * #_ #Htb cases (Htb … Hta) -Htb -Hta 
   [* #Hgridc @False_ind @(absurd … Hgridc) @eqnot_to_noteq 
    @(Hnogrids 〈c,false〉) @memb_hd ]
-* #Hgrdic #Htb lapply (Htb l 〈grid,false〉 (〈bar,false〉::〈d,false〉::rs) (refl …) (refl …) ?) 
+* * #Hgrdic #Htb #_ lapply (Htb l 〈grid,false〉 (〈bar,false〉::〈d,false〉::rs) (refl …) (refl …) ?) 
   [#x #membl @Hnogrids @memb_cons @membl] -Htb #Htb
-* #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb #Htc
-* #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd -Htc #Htd
-* #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Hte -Htd #Hte
-* #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf -Hte #Htf
-whd in ⊢ (%→?); #Htg cases (Htg … Htf) -Htg -Htf
-  [* whd in ⊢ ((??%?)→?); #Habs destruct (Habs)]
-* #_ #Htg lapply (Htg (〈grid,false〉::reverse ? l) 〈c,true〉 ls (refl …) (refl …) ?) 
+* #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc … Htb) -Htc -Htb #Htc
+* #td * whd in ⊢ (%→?); * #_ #Htd lapply (Htd … Htc) -Htd -Htc #Htd
+* #te * whd in ⊢ (%→?); * #Hte #_ lapply (Hte … Htd) -Hte -Htd #Hte
+* #tf * whd in ⊢ (%→?); * #_ #Htf lapply (Htf … Hte) -Htf -Hte #Htf
+whd in ⊢ (%→?); * #_ #Htg cases (Htg … Htf) -Htg -Htf
+#_ #Htg cases (Htg (refl …)) -Htg #Htg #_
+lapply (Htg (〈grid,false〉::reverse ? l) 〈c,true〉 ls (refl …) (refl …) ?) 
   [#x #membl @Hnomarks @daemon] -Htg #Htg >Htg >reverse_cons >reverse_reverse
    >associative_append %
 qed.
@@ -134,21 +134,22 @@ cases (sem_seq ????? sem_init_current_on_match
 #l1 #l2 #c #ls #d #rs #Hl1marks #Hl1grids #Hl2marks #Hc #Hintape
 cases HR -HR
 #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hl1grids Hc Hintape) -Hta -Hintape #Hta
-* #tb * whd in ⊢ (%→?); #Htb lapply (Htb  … Hta) -Htb -Hta
+* #tb * whd in ⊢ (%→?); * #_ #Htb lapply (Htb  … Hta) -Htb -Hta
 generalize in match Hl1marks; -Hl1marks cases (list_last ? l1) 
   [#eql1 >eql1 #Hl1marks whd in ⊢ ((???%)→?); whd in ⊢ ((???(????%))→?); #Htb
-   * #tc * whd in ⊢ (%→?); #Htc lapply (Htc  … Htb) -Htc -Htb *
+   * #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc  … Htb) -Htc -Htb *
     [* whd in ⊢ ((??%?)→?); #Htemp destruct (Htemp)]
-   * #_ #Htc lapply (Htc … (refl …) (refl …) ?)
+   * * #_ #Htc #_ lapply (Htc … (refl …) (refl …) ?)
     [#x #membx @Hl2marks @membx]
-   #Htc whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc) -Houtc -Htc #Houtc
+   #Htc whd in ⊢ (%→?); * #Houtc #_ cases (Houtc (reverse ? l2@〈grid,false〉::〈c,true〉::〈grid,false〉::ls) comma)
+   -Houtc #Houtc lapply (Houtc … Htc) -Houtc -Htc #Houtc #_
    >Houtc %
   |* #c1 * #tl #eql1 >eql1 #Hl1marks >reverse_append >reverse_single 
    whd in ⊢ ((???%)→?); whd in ⊢ ((???(????%))→?);
    >associative_append whd in ⊢ ((???(????%))→?); #Htb
-   * #tc * whd in ⊢ (%→?); #Htc lapply (Htc  … Htb) -Htc -Htb *
+   * #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc  … Htb) -Htc -Htb *
     [* >Hl1marks [#Htemp destruct (Htemp)] @memb_append_l2 @memb_hd]
-   * #_ >append_cons <associative_append #Htc lapply (Htc … (refl …) (refl …) ?)
+   * * #_ >append_cons <associative_append #Htc lapply (Htc … (refl …) (refl …) ?)
     [#x #membx cases (memb_append … membx) -membx #membx
       [cases (memb_append … membx) -membx #membx
         [@Hl1marks @memb_append_l1 @daemon
@@ -156,7 +157,9 @@ generalize in match Hl1marks; -Hl1marks cases (list_last ? l1)
         ]
       |@Hl2marks @membx
       ]]
-  #Htc whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc) -Houtc -Htc #Houtc
+  -Htc #Htc #_ whd in ⊢ (%→?); * #Houtc #_ cases (Houtc (reverse (FinProd FSUnialpha FinBool) ((reverse STape tl@[〈grid,false〉])@l2)
+     @c1::〈c,true〉::〈grid,false〉::ls) comma)
+  -Houtc #Houtc lapply (Houtc … Htc) -Houtc -Htc #Houtc #_
   >Houtc >reverse_append >reverse_append >reverse_single 
   >reverse_reverse >associative_append >associative_append 
   >associative_append %
@@ -338,7 +341,7 @@ lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1
 | #Hta * #tb * whd in ⊢ (%→?); #Htb
   lapply (Htb (〈grid,false〉::ls) s0 s1 c0 c1 (〈mv,false〉::table2@〈grid,false〉::rs) newconfig (〈comma,false〉::reverse ? table1) curconfig Hta ????????) -Htb
   [9:|*:(* bit_or_null c0,c1; |curconfig| = |newconfig|*) @daemon ]
-  #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc whd in ⊢(???(??%%%)→?);#Htc
+  #Htb * #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc … Htb) -Htc whd in ⊢(???(??%%%)→?);#Htc
   whd in ⊢ (%→?); #Houtc whd in Htc:(???%); whd in Htc:(???(??%%%));
   lapply (Houtc rs n 
     (〈comma,false〉::〈c1,false〉::reverse ? newconfig@〈s1,false〉::〈comma,false〉::reverse ? table1)
@@ -475,13 +478,164 @@ definition R_uni_step_true ≝ λt1,t2.
 definition R_uni_step_false ≝ λt1,t2.
   ∀b. current STape t1 = Some ? 〈bit b,false〉 → b = true ∧ t2 = t1.
   
-axiom sem_match_tuple : Realize ? match_tuple R_match_tuple.
+(*axiom sem_match_tuple : Realize ? match_tuple R_match_tuple.*)
 
 definition us_acc : states ? uni_step ≝ (inr … (inl … (inr … start_nop))).
 
+definition Pre_uni_step ≝ λt1.
+  ∃n,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
+  0 < |table| ∧ table_TM (S n) table ∧
+  match_in_table (S n) (〈s0,false〉::curconfig) 〈c0,false〉
+    (〈s1,false〉::newconfig) 〈c1,false〉 〈mv,false〉 table ∧
+  legal_tape ls 〈c0,false〉 rs ∧
+  t1 = midtape STape (〈grid,false〉::ls) 〈s0,false〉 
+    (curconfig@〈c0,false〉::〈grid,false〉::table@〈grid,false〉::rs).
+    
 lemma sem_uni_step :
-  accRealize ? uni_step us_acc
+  accGRealize ? uni_step us_acc Pre_uni_step
      R_uni_step_true R_uni_step_false. 
+@(acc_sem_if_app_guarded STape … (sem_test_char ? (λc:STape.\fst c == bit false)) 
+  ? (test_char_inv …) (sem_nop …) …)
+[| @(sem_seq_app_guarded … (Realize_to_GRealize … sem_init_match) ???)
+  [ 5: @sub_reflexive
+  | 3: @(sem_seq_app_guarded … sem_match_tuple 
+         (Realize_to_GRealize … (sem_if ????????? (sem_test_char …  (λc.¬is_marked FSUnialpha c))
+          (sem_seq … sem_exec_action (sem_move_r …))
+          (sem_nop …))))
+     [@(λx.True)
+     |//
+     |@sub_reflexive]
+  ||| #t1 #t2 * #n * #table * #s0 * #s1 * #c0 * #c1 * #ls * #rs * #curconfig 
+      * #newconfig * #mv * * * *
+      #Hlen1 #Htable #Hmatch #Hlegal #Ht1
+      whd in ⊢ (%→?);
+      cut (∃tup,table0.table = tup@table0 ∧ tuple_TM (S n) tup)
+      [@daemon]
+      * #tup * #table0 * #Htableeq * #qin * #cin * #qout * #cout * #mv0
+      * * * * * * * * * *
+      #Hqinnomarks #_ #Hqinbits #_ #_ #_ #_ #_ #Hqinlen #_ #Htupeq
+      cut (∃d,qin0.qin = 〈d,false〉::qin0)
+      [ lapply Hqinlen lapply Hqinnomarks -Hqinlen -Hqinnomarks cases qin
+        [ #_ normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) 
+        | * #d #bd #qin0 #Hqinnomarks #_ %{d} %{qin0}
+          >(?:bd=false) [%]
+          @(Hqinnomarks 〈d,bd〉) @memb_hd ] ]
+      * #d * #qin0 #Hqineq
+      #Ht2 
+      lapply (Ht2 (〈grid,false〉::ls) (curconfig@[〈c0,false〉])
+               (qin0@〈cin,false〉::〈comma,false〉::qout@〈cout,false〉::〈comma,false〉::〈mv0,false〉::table0@〈grid,false〉::rs) s0 d ???)
+      [ >Ht1 @eq_f >associative_append @eq_f @eq_f @eq_f
+        >Htableeq >Htupeq >associative_append whd in ⊢ (??%?);
+        @eq_f >Hqineq >associative_append @eq_f whd in ⊢ (??%?);
+        @eq_f whd in ⊢ (??%?); @eq_f
+        >associative_append %
+      | @daemon
+      | @daemon
+      ]
+      #Ht2 % [| % [| % [| % [ @Ht2 ]
+        %2
+        (* ls0 = ls
+           c = s0
+           l1 = curconfig@[〈c0,false〉]
+           l2 = [〈bar,false〉]
+           c10 = d
+           l3 = qin0@[〈cin,false〉]
+           l4 = qout@〈cout,false〉::〈comma,false〉::〈mv0,false〉::table0
+           rs00 = rs
+           n0 = S n ?
+         *)
+        %{ls} %{s0} %{(curconfig@[〈c0,false〉])}
+        %{([〈bar,false〉])} %{d} %{(qin0@[〈cin,false〉])}
+        %{(qout@〈cout,false〉::〈comma,false〉::〈mv0,false〉::table0)}
+        %{rs} %{n} @daemon (* TODO *)
+      ]
+     ]
+    ]
+   ]
+ | #intape #outtape 
+  #ta whd in ⊢ (%→?); #Hta #HR
+  #n #fulltable #s0 #s1 #c0 #c1 #ls #rs #curconfig #newconfig #mv
+  #Htable_len cut (∃t0,table. fulltable =〈bar,false〉::〈t0,false〉::table) [(* 0 < |table| *) @daemon]
+  * #t0 * #table #Hfulltable >Hfulltable -fulltable 
+  #Htable #Hmatch #Htape #Hintape #t1' #Ht1'
+  >Hintape in Hta; * * * #c #bc *
+  whd in ⊢ (??%?→?); #HSome destruct (HSome) #Hc #Hta % [@(\P Hc)]
+  cases HR -HR 
+  #tb * whd in ⊢ (%→?); #Htb
+  lapply (Htb (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) (table@〈grid,false〉::rs) c t0 ???)
+  [ >Hta >associative_append %
+  | @daemon
+  | @daemon
+  | -Hta -Htb #Htb * 
+    #tc * whd in ⊢ (%→?); #Htc cases (Htc … Htable … Htb) -Htb -Htc
+    [| * #Hcurrent #Hfalse @False_ind
+      (* absurd by Hmatch *) @daemon
+    | >(\P Hc) %
+    | (* Htable (con lemma) *) @daemon
+    | (* Hmatch *) @daemon
+    | (* Htable *) @daemon
+    | (* Htable, Hmatch → |config| = n 
+       necessaria modifica in R_match_tuple, le dimensioni non corrispondono
+      *) @daemon
+    ]
+    * #table1 * #newc * #mv1 * #table2 * #Htableeq #Htc *
+    [ * #td * whd in ⊢ (%→?); >Htc -Htc * * #c2 * whd in ⊢ (??%?→?); #Hc2 destruct (Hc2) 
+      #_ #Htd
+      cut (newc = 〈s1,false〉::newconfig@[〈c1,false〉]) [@daemon] #Hnewc
+      >Hnewc cut (mv1 = 〈mv,false〉)
+      [@daemon] #Hmv1
+      * #te * whd in ⊢ (%→?); #Hte
+      cut (td = midtape STape (〈c0,false〉::reverse STape curconfig@〈c,false〉::〈grid,false〉::ls) 
+              〈grid,false〉
+              ((table1@〈bar,false〉::〈c,false〉::curconfig@[〈c0,false〉])@〈comma,true〉::〈s1,false〉::
+               newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs))
+      [ >Htd @eq_f3 //
+        [ >reverse_append >reverse_single %
+        | >associative_append >associative_append normalize
+          >associative_append >Hmv1 >Hnewc @eq_f @eq_f @eq_f @eq_f @eq_f @eq_f
+          whd in ⊢ (??%?); >associative_append % 
+        ]
+      ]
+      -Htd #Htd lapply (Hte … (S n) … Htd … Ht1') -Htd -Hte
+      [ //
+      | (*|curconfig| = |newconfig|*) @daemon
+      | (* Htable → bit_or_null c1 = true *) @daemon
+      | (* only_bits (〈s1,false〉::newconfig) *) @daemon
+      | (* only_bits (curconfig@[〈s0,false〉]) *) @daemon
+      | (* no_marks (reverse ? curconfig) *) @daemon
+      | >Hmv1 in Htableeq; >Hnewc 
+        >associative_append >associative_append normalize
+        >associative_append >associative_append
+        #Htableeq <Htableeq // ]
+      * #ls1 * #rs1 * #c2 * * #Hte #Hliftte #Hlegalte
+      whd in ⊢ (%→?); * #_ #Houttape lapply (Houttape … Hte) -Houttape #Houttape
+      whd in Houttape:(???%); whd in Houttape:(???(??%%%));
+      @ex_intro [| @(ex_intro ?? rs1) @ex_intro [| % [ % 
+      [ >Houttape @eq_f @eq_f @eq_f @eq_f
+        change with ((〈bar,false〉::〈t0,false〉::table)@?) in ⊢ (???%);
+        >Htableeq >associative_append >associative_append 
+        >associative_append normalize >associative_append
+        >associative_append normalize >Hnewc <Hmv1
+        >associative_append normalize >associative_append
+        >Hmv1 % 
+      | @Hliftte
+      ]
+     | //
+     ]
+    ]
+   ] 
+  | * #td * whd in ⊢ (%→%→?); >Htc * #Htd
+    lapply (Htd ? (refl ??)) normalize in ⊢ (%→?);
+    #Hfalse destruct (Hfalse)
+  ]
+ ]
+| #t1 #t2 #t3 whd in ⊢ (%→%→?); #Ht1 #Ht2
+  #b #Hb >Hb in Ht1; * #Hc #Ht1 lapply (Hc ? (refl ??)) -Hc #Hb' %
+  // cases b in Hb'; normalize #H1 //
+]
+qed.
+
+(*
 @(acc_sem_if_app STape … (sem_test_char ? (λc:STape.\fst c == bit false))
    (sem_seq … sem_init_match      
      (sem_seq … sem_match_tuple        
@@ -497,11 +651,11 @@ lemma sem_uni_step :
   #Htable_len cut (∃t0,table. fulltable =〈bar,false〉::〈t0,false〉::table) [(* 0 < |table| *) @daemon]
   * #t0 * #table #Hfulltable >Hfulltable -fulltable 
   #Htable #Hmatch #Htape #Hintape #t1' #Ht1'
-  >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta 
-  #Hs0 lapply (\P Hs0) -Hs0 #Hs0 #Hta % //
+  >Hintape in Hta; * * * #c #bc *
+  whd in ⊢ (??%?→?); #HSome destruct (HSome) #Hc #Hta % [@(\P Hc)]
   cases HR -HR 
   #tb * whd in ⊢ (%→?); #Htb
-  lapply (Htb (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) (table@〈grid,false〉::rs) s0 t0 ???)
+  lapply (Htb (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) (table@〈grid,false〉::rs) c t0 ???)
   [ >Hta >associative_append %
   | @daemon
   | @daemon
@@ -509,7 +663,7 @@ lemma sem_uni_step :
     #tc * whd in ⊢ (%→?); #Htc cases (Htc … Htable … Htb) -Htb -Htc
     [| * #Hcurrent #Hfalse @False_ind
       (* absurd by Hmatch *) @daemon
-    | >Hs0 %
+    | >(\P Hc) %
     | (* Htable (con lemma) *) @daemon
     | (* Hmatch *) @daemon
     | (* Htable *) @daemon
@@ -518,20 +672,21 @@ lemma sem_uni_step :
       *) @daemon
     ]
     * #table1 * #newc * #mv1 * #table2 * #Htableeq #Htc *
-    [ * #td * whd in ⊢ (%→?); >Htc -Htc #Htd
-      cases (Htd ? (refl ??)) #_ -Htd
+    [ * #td * whd in ⊢ (%→?); >Htc -Htc * * #c2 * whd in ⊢ (??%?→?); #Hc2 destruct (Hc2) 
+      #_ #Htd
       cut (newc = 〈s1,false〉::newconfig@[〈c1,false〉]) [@daemon] #Hnewc
-      >Hnewc #Htd cut (mv1 = 〈mv,false〉)
+      >Hnewc cut (mv1 = 〈mv,false〉)
       [@daemon] #Hmv1
       * #te * whd in ⊢ (%→?); #Hte
-      cut (td = midtape STape (〈c0,false〉::reverse STape curconfig@〈s0,false〉::〈grid,false〉::ls) 
+      cut (td = midtape STape (〈c0,false〉::reverse STape curconfig@〈c,false〉::〈grid,false〉::ls) 
               〈grid,false〉
-              ((table1@〈bar,false〉::〈s0,false〉::curconfig@[〈c0,false〉])@〈comma,true〉::〈s1,false〉::
+              ((table1@〈bar,false〉::〈c,false〉::curconfig@[〈c0,false〉])@〈comma,true〉::〈s1,false〉::
                newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs))
       [ >Htd @eq_f3 //
         [ >reverse_append >reverse_single %
         | >associative_append >associative_append normalize
-          >associative_append >associative_append >Hmv1 % 
+          >associative_append >Hmv1 >Hnewc @eq_f @eq_f @eq_f @eq_f @eq_f @eq_f
+          whd in ⊢ (??%?); >associative_append % 
         ]
       ]
       -Htd #Htd lapply (Hte … (S n) … Htd … Ht1') -Htd -Hte
@@ -546,7 +701,7 @@ lemma sem_uni_step :
         >associative_append >associative_append
         #Htableeq <Htableeq // ]
       * #ls1 * #rs1 * #c2 * * #Hte #Hliftte #Hlegalte
-      whd in ⊢ (%→?); #Houttape lapply (Houttape … Hte) -Houttape #Houttape
+      whd in ⊢ (%→?); * #_ #Houttape lapply (Houttape … Hte) -Houttape #Houttape
       whd in Houttape:(???%); whd in Houttape:(???(??%%%));
       @ex_intro [| @(ex_intro ?? rs1) @ex_intro [| % [ % 
       [ >Houttape @eq_f @eq_f @eq_f @eq_f
@@ -562,13 +717,14 @@ lemma sem_uni_step :
      ]
     ]
    ] 
-  | * #td * whd in ⊢ (%→%→?); >Htc #Htd
-    cases (Htd ? (refl ??)) normalize in ⊢ (%→?);
+  | * #td * whd in ⊢ (%→%→?); >Htc * #Htd
+    lapply (Htd ? (refl ??)) normalize in ⊢ (%→?);
     #Hfalse destruct (Hfalse)
   ]
  ]
 | #t1 #t2 #t3 whd in ⊢ (%→%→?); #Ht1 #Ht2
-  #b #Hb cases (Ht1 ? Hb) #Hb' #Ht3 >Ht2 % //
-  cases b in Hb'; normalize #H1 //
+  #b #Hb >Hb in Ht1; * #Hc #Ht1 lapply (Hc ? (refl ??)) -Hc #Hb' %
+  // cases b in Hb'; normalize #H1 //
 ]
-qed.
\ No newline at end of file
+qed.
+*)
\ No newline at end of file