From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 28 May 2012 13:33:45 +0000 (+0000)
Subject: porting of move_char_c
X-Git-Tag: make_still_working~1683
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5fc2b08d86038360e588b8fff333a623964efabe;p=helm.git

porting of move_char_c
---

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 7d6bad37f..f041d8b25 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -39,7 +39,6 @@ definition right ≝
  | rightof _ _ ⇒ []
  | midtape _ _ r ⇒ r ].
  
- 
 definition current ≝ 
  λsig.λt:tape sig.match t with
  [ midtape _ c _ ⇒ Some ? c
diff --git a/matita/matita/lib/turing/universal/copy.ma b/matita/matita/lib/turing/universal/copy.ma
index 019f06540..854b6e158 100644
--- a/matita/matita/lib/turing/universal/copy.ma
+++ b/matita/matita/lib/turing/universal/copy.ma
@@ -10,21 +10,20 @@
       V_____________________________________________________________*)
 
 
-(* COMPARE BIT
-
-*)
-
 include "turing/universal/tuples.ma".
 
 definition write_states ≝ initN 2.
 
+definition wr0 : write_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
+definition wr1 : write_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
+
 definition write ≝ λalpha,c.
   mk_TM alpha write_states
   (λp.let 〈q,a〉 ≝ p in
-    match q with 
-    [ O ⇒ 〈1,Some ? 〈c,N〉〉
-    | S _ ⇒ 〈1,None ?〉 ])
-  O (λx.x == 1).
+    match pi1 … q with 
+    [ O ⇒ 〈wr1,Some ? 〈c,N〉〉
+    | S _ ⇒ 〈wr1,None ?〉 ])
+  wr0 (λx.x == wr1).
   
 definition R_write ≝ λalpha,c,t1,t2.
   ∀ls,x,rs.t1 = midtape alpha ls x rs → t2 = midtape alpha ls c rs.
@@ -147,7 +146,7 @@ definition R_copy_step_false ≝
    bit_or_null (\fst c) = false ∧ t2 = t1.
 
 axiom sem_copy_step : 
-  accRealize ? copy_step (inr … (inl … (inr … 0))) R_copy_step_true R_copy_step_false.
+  accRealize ? copy_step (inr … (inl … (inr … start_nop))) R_copy_step_true R_copy_step_false.
 
 (*
 1) il primo carattere è marcato
@@ -155,7 +154,7 @@ axiom sem_copy_step :
 3) il terminatore non è né bit, né null
 *)
    
-definition copy0 ≝ whileTM ? copy_step (inr … (inl … (inr … 0))).
+definition copy0 ≝ whileTM ? copy_step (inr … (inl … (inr … start_nop))).
 
 let rec merge_config (l1,l2:list STape) ≝ 
   match l1 with
@@ -201,11 +200,6 @@ lemma inj_append_singleton_l2 :
 >reverse_append >reverse_append normalize #H1 destruct %
 qed.
 
-lemma length_reverse : ∀A,l.|reverse A l| = |l|.
-#A #l elim l //
-#a0 #l0 #IH normalize >rev_append_def >length_append >IH normalize //
-qed.
-
 lemma wsem_copy0 : WRealize ? copy0 R_copy0.
 #intape #k #outc #Hloop 
 lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
@@ -272,7 +266,7 @@ lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
         [|normalize in Hl1; destruct (Hl1) %]
         >(?:l4 = 〈grid,bg〉::lb)
         [|@(inj_append_singleton_l1 ?? (〈grid,bg〉::lb) ?? Hl4) ]
-        >length_append >commutative_plus >length_reverse 
+        >length_append >commutative_plus >length_reverse
         normalize #Hlalb destruct (Hlalb) //
       ] #Hlen2
       *
diff --git a/matita/matita/lib/turing/universal/move_char_c.ma b/matita/matita/lib/turing/universal/move_char_c.ma
index f970da13e..4d2490ee0 100644
--- a/matita/matita/lib/turing/universal/move_char_c.ma
+++ b/matita/matita/lib/turing/universal/move_char_c.ma
@@ -35,39 +35,46 @@ include "turing/while_machine.ma".
 
 definition mcc_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 5) alpha.
 
+definition mcc0 : initN 5 ≝ mk_Sig ?? 0 (leb_true_to_le 1 5 (refl …)).
+definition mcc1 : initN 5 ≝ mk_Sig ?? 1 (leb_true_to_le 2 5 (refl …)).
+definition mcc2 : initN 5 ≝ mk_Sig ?? 2 (leb_true_to_le 3 5 (refl …)).
+definition mcc3 : initN 5 ≝ mk_Sig ?? 3 (leb_true_to_le 4 5 (refl …)).
+definition mcc4 : initN 5 ≝ mk_Sig ?? 4 (leb_true_to_le 5 5 (refl …)).
+
 definition mcc_step ≝ 
  λalpha:FinSet.λsep:alpha.
  mk_TM alpha (mcc_states alpha)
  (λp.let 〈q,a〉 ≝ p in
   let 〈q',b〉 ≝ q in
+  let q' ≝ pi1 nat (λi.i<5) q' in (* perche' devo passare il predicato ??? *)
   match a with 
-  [ None ⇒ 〈〈4,sep〉,None ?〉 
-  | Some a' ⇒ 
+  [ None ⇒ 〈〈mcc4,sep〉,None ?〉 
+  | Some a' ⇒  
   match q' with
   [ O ⇒ (* qinit *)
     match a' == sep with
-    [ true ⇒ 〈〈4,sep〉,None ?〉
-    | false ⇒ 〈〈1,a'〉,Some ? 〈a',L〉〉 ]
-  | S q' ⇒ match q' with
+    [ true ⇒ 〈〈mcc4,sep〉,None ?〉
+    | false ⇒ 〈〈mcc1,a'〉,Some ? 〈a',L〉〉 ]
+  | S q' ⇒  match q' with
     [ O ⇒ (* q1 *)
-      〈〈2,a'〉,Some ? 〈b,R〉〉
+      〈〈mcc2,a'〉,Some ? 〈b,R〉〉
     | S q' ⇒ match q' with
       [ O ⇒ (* q2 *)
-        〈〈3,sep〉,Some ? 〈b,R〉〉
+        〈〈mcc3,sep〉,Some ? 〈b,R〉〉
       | S q' ⇒ match q' with
         [ O ⇒ (* qacc *)
-          〈〈3,sep〉,None ?〉
+          〈〈mcc3,sep〉,None ?〉
         | S q' ⇒ (* qfail *)
-          〈〈4,sep〉,None ?〉 ] ] ] ] ])
-  〈0,sep〉
-  (λq.let 〈q',a〉 ≝ q in q' == 3 ∨ q' == 4).
+          〈〈mcc4,sep〉,None ?〉 ] ] ] ] ])
+  〈mcc0,sep〉
+  (λq.let 〈q',a〉 ≝ q in q' == mcc3 ∨ q' == mcc4).
 
 lemma mcc_q0_q1 : 
   ∀alpha:FinSet.∀sep,a,ls,a0,rs.
   a0 == sep = false → 
   step alpha (mcc_step alpha sep)
-    (mk_config ?? 〈0,a〉 (mk_tape … ls (Some ? a0) rs)) =
-  mk_config alpha (states ? (mcc_step alpha sep)) 〈1,a0〉
+    (mk_config ?? 〈mcc0,a〉 (mk_tape … ls (Some ? a0) rs)) =
+  mk_config alpha (states ? (mcc_step alpha sep)) 〈mcc1,a0〉
     (tape_move_left alpha ls a0 rs).
 #alpha #sep #a *
 [ #a0 #rs #Ha0 whd in ⊢ (??%?); 
@@ -80,8 +87,8 @@ qed.
 lemma mcc_q1_q2 :
   ∀alpha:FinSet.∀sep,a,ls,a0,rs.
   step alpha (mcc_step alpha sep) 
-    (mk_config ?? 〈1,a〉 (mk_tape … ls (Some ? a0) rs)) = 
-  mk_config alpha (states ? (mcc_step alpha sep)) 〈2,a0〉 
+    (mk_config ?? 〈mcc1,a〉 (mk_tape … ls (Some ? a0) rs)) = 
+  mk_config alpha (states ? (mcc_step alpha sep)) 〈mcc2,a0〉 
     (tape_move_right alpha ls a rs).
 #alpha #sep #a #ls #a0 * //
 qed.
@@ -89,8 +96,8 @@ qed.
 lemma mcc_q2_q3 :
   ∀alpha:FinSet.∀sep,a,ls,a0,rs.
   step alpha (mcc_step alpha sep) 
-    (mk_config ?? 〈2,a〉 (mk_tape … ls (Some ? a0) rs)) = 
-  mk_config alpha (states ? (mcc_step alpha sep)) 〈3,sep〉 
+    (mk_config ?? 〈mcc2,a〉 (mk_tape … ls (Some ? a0) rs)) = 
+  mk_config alpha (states ? (mcc_step alpha sep)) 〈mcc3,sep〉 
     (tape_move_right alpha ls a rs).
 #alpha #sep #a #ls #a0 * //
 qed.
@@ -109,38 +116,44 @@ definition Rmcc_step_false ≝
     
 lemma mcc_trans_init_sep: 
   ∀alpha,sep,x.
-  trans ? (mcc_step alpha sep) 〈〈0,x〉,Some ? sep〉 = 〈〈4,sep〉,None ?〉.
+  trans ? (mcc_step alpha sep) 〈〈mcc0,x〉,Some ? sep〉 = 〈〈mcc4,sep〉,None ?〉.
 #alpha #sep #x normalize >(\b ?) //
 qed.
  
 lemma mcc_trans_init_not_sep: 
   ∀alpha,sep,x,y.y == sep = false → 
-  trans ? (mcc_step alpha sep) 〈〈0,x〉,Some ? y〉 = 〈〈1,y〉,Some ? 〈y,L〉〉.
+  trans ? (mcc_step alpha sep) 〈〈mcc0,x〉,Some ? y〉 = 〈〈mcc1,y〉,Some ? 〈y,L〉〉.
 #alpha #sep #x #y #H1 normalize >H1 //
 qed.
 
 lemma sem_mcc_step :
   ∀alpha,sep.
   accRealize alpha (mcc_step alpha sep) 
-    〈3,sep〉 (Rmcc_step_true alpha sep) (Rmcc_step_false alpha sep).
-#alpha #sep *
+    〈mcc3,sep〉 (Rmcc_step_true alpha sep) (Rmcc_step_false alpha sep).
+#alpha #sep 
+cut (∀P:Prop.〈mcc4,sep〉=〈mcc3,sep〉→P)
+  [#P whd in ⊢ ((??(???%?)(???%?))→?); #Hfalse destruct] #Hfalse
+*
 [@(ex_intro ?? 2)  
-  @(ex_intro … (mk_config ?? 〈4,sep〉 (niltape ?)))
-  % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %]
+  @(ex_intro … (mk_config ?? 〈mcc4,sep〉 (niltape ?))) % 
+  [% [whd in ⊢ (??%?); % | @Hfalse]
+  |#H1 #H2 @False_ind @(absurd ?? H2) %]
 |#l0 #lt0 @(ex_intro ?? 2)  
-  @(ex_intro … (mk_config ?? 〈4,sep〉 (leftof ? l0 lt0)))
-  % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %]
+  @(ex_intro … (mk_config ?? 〈mcc4,sep〉 (leftof ? l0 lt0)))% 
+  [% [whd in ⊢ (??%?);% |@Hfalse]
+  |#H1 #H2 @False_ind @(absurd ?? H2) %]
 |#r0 #rt0 @(ex_intro ?? 2)  
-  @(ex_intro … (mk_config ?? 〈4,sep〉 (rightof ? r0 rt0)))
-  % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %]
+  @(ex_intro … (mk_config ?? 〈mcc4,sep〉 (rightof ? r0 rt0))) % 
+  [% [whd in ⊢ (??%?);% |@Hfalse] 
+  |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %]
 | #lt #c #rt cases (true_or_false (c == sep)) #Hc
   [ @(ex_intro ?? 2) 
-    @(ex_intro ?? (mk_config ?? 〈4,sep〉 (midtape ? lt c rt)))
+    @(ex_intro ?? (mk_config ?? 〈mcc4,sep〉 (midtape ? lt c rt)))
     % [ % 
         [ >(\P Hc) >loop_S_false // >loop_S_true 
          [ @eq_f whd in ⊢ (??%?); >mcc_trans_init_sep %
          |>(\P Hc) whd in ⊢(??(???(???%))?); >mcc_trans_init_sep % ]
-        |   #Hfalse destruct ]
+        |@Hfalse]
       |#_ #H1 #H2 % // normalize >(\P Hc) % ]
   | @(ex_intro ?? 4) cases lt
     [ @ex_intro
@@ -164,7 +177,7 @@ qed.
 
 (* the move_char (variant c) machine *)
 definition move_char_c ≝ 
-  λalpha,sep.whileTM alpha (mcc_step alpha sep) 〈3,sep〉.
+  λalpha,sep.whileTM alpha (mcc_step alpha sep) 〈mcc3,sep〉.
 
 definition R_move_char_c ≝ 
   λalpha,sep,t1,t2.
@@ -182,15 +195,12 @@ lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
   %
-  [ #Hb >Htapea in H1; >Hb normalize in ⊢ (%→?); #H1
-   cases (H1 ??)
-   [#_ #H2 >H2 %
-   |*: % #H2 destruct (H2) ]
+  [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
+    [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)]
   | #rs1 #rs2 #Hrs #Hb #Hrs1 
-    >Htapea in H1; normalize in ⊢ (% → ?); #H1
-    cases (H1 ??)
-    [ #Hfalse @False_ind @(absurd ?? Hb) destruct %
-    |*:% #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
@@ -198,10 +208,9 @@ lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
   #Ha0 #Htapeb %
   [ #Hfalse @False_ind @(absurd ?? Ha0) //
   | *
-    [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ normalize
-      >Hrs in Htapeb; normalize #Htapeb
-      cases (IH … Htapeb)
-      #Houtc #_ >Houtc //
+    [ #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)
       [ %
diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma
index 4ec94cbc3..fed33bfa8 100644
--- a/matita/matita/lib/turing/universal/move_tape.ma
+++ b/matita/matita/lib/turing/universal/move_tape.ma
@@ -15,15 +15,19 @@ include "turing/universal/tuples.ma".
 
 definition init_cell_states ≝ initN 2.
 
+definition ics0 : init_cell_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
+definition ics1 : init_cell_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
+
+d
 definition init_cell ≝ 
  mk_TM STape init_cell_states
  (λp.let 〈q,a〉 ≝ p in
-  match q with
+  match pi1 … q with
   [ O ⇒ match a with
-    [ None ⇒ 〈1, Some ? 〈〈null,false〉,N〉〉
+    [ None ⇒ 〈ics1, Some ? 〈〈null,false〉,N〉〉
     | Some _ ⇒ 〈1, None ?〉 ]
-  | S _ ⇒ 〈1,None ?〉 ])
- O (λq.q == 1).
+  | S _ ⇒ 〈ics1,None ?〉 ])
+ ics0 (λq.q == ics1).
  
 definition R_init_cell ≝ λt1,t2.
  (∃c.current STape t1 = Some ? c ∧ t2 = t1) ∨
diff --git a/matita/matita/lib/turing/universal/trans_to_tuples.ma b/matita/matita/lib/turing/universal/trans_to_tuples.ma
new file mode 100644
index 000000000..e40a0bbc8
--- /dev/null
+++ b/matita/matita/lib/turing/universal/trans_to_tuples.ma
@@ -0,0 +1,307 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic   
+    ||A||  Library of Mathematics, developed at the Computer Science 
+    ||T||  Department of the University of Bologna, Italy.           
+    ||I||                                                            
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_____________________________________________________________*)
+
+
+
+include "turing/universal/tuples.ma".
+include "basics/fun_graph.ma".
+
+(* p < n is represented with a list of bits of lenght n with the
+ p-th bit from left set to 1 *)
+ 
+let rec to_bitlist n p: list bool ≝
+  match n with
+  [ O ⇒ [ ]
+  | S q ⇒ (eqb p q)::to_bitlist q p].
+  
+let rec from_bitlist l ≝
+  match l with
+  [ nil ⇒ 0 (* assert false *)
+  | cons b tl ⇒ if b then |tl| else from_bitlist tl].
+
+lemma bitlist_length: ∀n,p.|to_bitlist n p| = n.
+#n elim n normalize // 
+qed.
+  
+lemma bitlist_inv1: ∀n,p.p<n → from_bitlist (to_bitlist n p) = p.
+#n elim n normalize -n
+  [#p #abs @False_ind /2/
+  |#n #Hind #p #lepn 
+   cases (le_to_or_lt_eq … (le_S_S_to_le … lepn))
+    [#ltpn lapply (lt_to_not_eq … ltpn) #Hpn
+     >(not_eq_to_eqb_false … Hpn) normalize @Hind @ltpn
+    |#Heq >(eq_to_eqb_true … Heq) normalize <Heq //
+    ]
+  ]
+qed.
+
+lemma bitlist_lt: ∀l. 0 < |l| → from_bitlist l < |l|.
+#l elim l normalize // #b #tl #Hind cases b normalize //
+#Htl cases (le_to_or_lt_eq … (le_S_S_to_le … Htl)) -Htl #Htl
+  [@le_S_S @lt_to_le @Hind //  
+  |cut (tl=[ ]) [/2 by append_l2_injective/] #eqtl >eqtl @le_n
+  ]
+qed.
+
+definition nat_of: ∀n. Nat_to n → nat.
+#n normalize * #p #_ @p
+qed. 
+
+definition bits_of_state ≝ λn.λh:Nat_to n → bool.λs:Nat_to n.
+  h s::(to_bitlist n (nat_of n s)).
+
+definition m_bits_of_state ≝ λn.λh.λp.
+  map ? (unialpha×bool) (λx.〈bit x,false〉) (bits_of_state n h p).
+  
+lemma no_marks_bits_of_state : ∀n,h,p. no_marks (m_bits_of_state n h p).
+#n #h #p #x whd in match (m_bits_of_state n h p);
+#H cases (orb_true_l … H) -H 
+  [#H >(\P H) %
+  |elim (to_bitlist n (nat_of n p))
+    [whd in ⊢ ((??%?)→?); #H destruct 
+    |#b #l #Hind #H cases (orb_true_l … H) -H #H
+      [>(\P H) %
+      |@Hind @H
+      ]
+    ]
+  ]
+qed.
+
+lemma only_bits_bits_of_state : ∀n,h,p. only_bits (m_bits_of_state n h p).
+#n #h #p #x whd in match (m_bits_of_state n h p);
+#H cases (orb_true_l … H) -H 
+  [#H >(\P H) %
+  |elim (to_bitlist n (nat_of n p))
+    [whd in ⊢ ((??%?)→?); #H destruct 
+    |#b #l #Hind #H cases (orb_true_l … H) -H #H
+      [>(\P H) %
+      |@Hind @H
+      ]
+    ]
+  ]
+qed.
+
+definition tuple_type ≝ λn.
+ (Nat_to n × (option FinBool)) × (Nat_to n × (option (FinBool × move))).  
+
+definition tuple_of_pair ≝ λn.λh:Nat_to n→bool. 
+  λp:tuple_type n.
+  let 〈inp,outp〉 ≝ p in
+  let 〈q,a〉 ≝ inp in
+  let cin ≝ match a with [ None ⇒ null | Some b ⇒ bit b ] in
+  let 〈qn,action〉 ≝ outp in
+  let 〈cout,mv〉 ≝ 
+    match action with 
+    [ None ⇒ 〈null,null〉
+    | Some act ⇒ let 〈na,m〉 ≝ act in 
+      match m with 
+      [ R ⇒ 〈bit na,bit true〉
+      | L ⇒ 〈bit na,bit false〉
+      | N ⇒ 〈bit na,null〉]
+    ] in
+  let qin ≝ m_bits_of_state n h q in
+  let qout ≝ m_bits_of_state n h qn in
+  mk_tuple qin 〈cin,false〉 qout 〈cout,false〉 〈mv,false〉.
+
+definition WFTuple_conditions ≝ 
+ λn,qin,cin,qout,cout,mv.
+ no_marks qin ∧ no_marks qout ∧ (* queste fuori ? *)
+ only_bits qin ∧ only_bits qout ∧ 
+ bit_or_null cin = true ∧ bit_or_null cout = true ∧ bit_or_null mv = true ∧
+ (cout = null → mv = null) ∧
+ |qin| = n ∧ |qout| = n.
+
+lemma is_tuple: ∀n,h,p. tuple_TM (S n) (tuple_of_pair n h p).
+#n #h * * #q #a * #qn #action
+@(ex_intro … (m_bits_of_state n h q))
+letin cin ≝ match a with [ None ⇒ null | Some b ⇒ bit b ]
+@(ex_intro … cin)
+@(ex_intro … (m_bits_of_state n h qn))
+letin cout ≝ 
+  match action with 
+  [ None ⇒ null | Some act ⇒ bit (\fst act)]
+@(ex_intro … cout)
+letin mv ≝ match action with 
+  [ None ⇒ null
+  | Some act ⇒ 
+      match \snd act with 
+      [ R ⇒ bit true | L ⇒ bit false | N ⇒ null]
+  ]
+@(ex_intro … mv)
+%[%[%[%[%[%[%[% /3/ 
+             |whd in match cin ; cases a //
+             ]
+           |whd in match cout; cases action //
+           ]
+         |whd in match mv; cases action //
+          * #b #m cases m //
+         ]
+       |whd in match cout; whd in match mv; cases action
+         [// | #act whd in ⊢ ((??%?)→?); #Hfalse destruct ]
+       ]
+     |>length_map normalize @eq_f //
+     ]
+   |>length_map normalize @eq_f //
+   ]
+ |normalize cases a cases action normalize //
+   [* #c #m cases m %
+   |* #c #m #c1 cases m %
+   ]
+ ]
+qed. 
+
+definition tuple_length ≝ λn.2*n+3.
+
+axiom length_of_tuple: ∀n,t. tuple_TM n t → 
+  |t| = tuple_length n.
+
+definition move_eq ≝ λm1,m2:move.
+  match m1 with
+  [R ⇒ match m2 with [R ⇒ true | _ ⇒ false]
+  |L ⇒ match m2 with [L ⇒ true | _ ⇒ false]
+  |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]].
+  
+definition tuples_of_pairs ≝ λn.λh.map … (λp.(tuple_of_pair n h p)@[〈bar,false〉]).
+
+definition flatten ≝ λA.foldr (list A) (list A) (append A) [].
+
+lemma wftable: ∀n,h,l.table_TM (S n) (flatten ? (tuples_of_pairs n h l)).
+#n #h #l elim l // -l #a #tl #Hind 
+whd in match (flatten … (tuples_of_pairs …));
+>associative_append @ttm_cons //
+qed.
+
+lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:list A. 0 < n →
+  (∀x. mem ? x l → |x| = n) → |a| = n → flatten ? l = l1@a@l2  →
+    (∃q.|l1| = n*q)  → mem ? a l.
+#A #n #l elim l
+  [normalize #l1 #l2 #a #posn #Hlen #Ha #Hnil @False_ind
+   cut (|a|=0) [@daemon] /2/
+  |#hd #tl #Hind #l1 #l2 #a #posn #Hlen #Ha 
+   whd in match (flatten ??); #Hflat * #q cases q
+    [<times_n_O #Hl1 
+     cut (a = hd) [@daemon] /2/
+    |#q1 #Hl1 lapply (split_exists … n l1 ?) //
+     * #l11 * #l12 * #Heql1 #Hlenl11 %2
+     @(Hind l12 l2 … posn ? Ha) 
+      [#x #memx @Hlen %2 //
+      |@(append_l2_injective ? hd l11) 
+        [>Hlenl11 @Hlen %1 %
+        |>Hflat >Heql1 >associative_append %
+        ]
+      |@(ex_intro …q1) @(injective_plus_r n) 
+       <Hlenl11 in ⊢ (??%?); <length_append <Heql1 >Hl1 //
+      ]
+    ]
+  ]
+qed.
+
+axiom match_decomp: ∀n,l,qin,cin,qout,cout,mv.
+  match_in_table (S n) qin cin qout cout mv l →
+  ∃l1,l2. l = l1@((mk_tuple qin cin qout cout mv)@[〈bar,false〉])@l2 ∧
+    (∃q.|l1| = (S (tuple_length (S n)))*q) ∧ tuple_TM (S n) (mk_tuple qin cin qout cout mv).
+(*
+lemma match_tech: ∀n,l,qin,cin,qout,cout,mv.
+  (∀t. mem ? t l → |t| = |mk_tuple qin cin qout cout mv|) →
+  match_in_table (S n) qin cin qout cout mv (flatten ? l) → 
+    ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? p l.
+#n #l #qin #cin #qout #cout #mv #Hlen #Hmatch 
+@(ex_intro … (mk_tuple qin cin qout cout mv)) % //
+@flatten_to_mem *)
+
+lemma match_to_tuple: ∀n,h,l,qin,cin,qout,cout,mv.
+  match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h l)) → 
+    ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? (p@[〈bar,false〉]) (tuples_of_pairs n h l).
+#n #h #l #qin #cin #qout #cout #mv #Hmatch 
+@(ex_intro … (mk_tuple qin cin qout cout mv)) % //
+cases (match_decomp … Hmatch) #l1 * #l2 * * #Hflat #Hlen #Htuple
+@(flatten_to_mem … Hflat … Hlen)  
+  [// 
+  |@daemon
+  |>length_append >(length_of_tuple … Htuple) normalize //
+  ]
+qed.
+
+lemma mem_map: ∀A,B.∀f:A→B.∀l,b. 
+  mem ? b (map … f l) → ∃a. mem ? a l ∧ f a = b.
+#A #B #f #l elim l 
+  [#b normalize @False_ind
+  |#a #tl #Hind #b normalize *
+    [#eqb @(ex_intro … a) /3/
+    |#memb cases (Hind … memb) #a * #mema #eqb
+     @(ex_intro … a) /3/
+    ]
+  ]
+qed.
+
+lemma match_to_pair: ∀n,h,l,qin,cin,qout,cout,mv.
+  match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h l)) → 
+    ∃p. tuple_of_pair n h p = mk_tuple qin cin qout cout mv ∧ mem ? p l.
+#n #h #l #qin #cin #qout #cout #mv #Hmatch 
+cases (match_to_tuple … Hmatch)
+#p * #eqp #memb 
+cases(mem_map … (λp.(tuple_of_pair n h p)@[〈bar,false〉]) … memb)
+#p1 * #Hmem #H @(ex_intro … p1) % /2/
+qed.
+
+(* turning DeqMove into a DeqSet *)
+lemma move_eq_true:∀m1,m2.
+  move_eq m1 m2 = true ↔ m1 = m2.
+*
+  [* normalize [% #_ % |2,3: % #H destruct ]
+  |* normalize [1,3: % #H destruct |% #_ % ]
+  |* normalize [1,2: % #H destruct |% #_ % ]
+qed.
+
+definition DeqMove ≝ mk_DeqSet move move_eq move_eq_true.
+
+unification hint 0 ≔ ;
+    X ≟ DeqMove
+(* ---------------------------------------- *) ⊢ 
+    move ≡ carr X.
+
+unification hint  0 ≔ m1,m2; 
+    X ≟ DeqMove
+(* ---------------------------------------- *) ⊢ 
+    move_eq m1 m2 ≡ eqb X m1 m2.
+
+(* turning DeqMove into a FinSet *)
+definition move_enum ≝ [L;R;N].
+
+lemma move_enum_unique: uniqueb ? [L;R;N] = true.
+// qed.
+
+lemma move_enum_complete: ∀x:move. memb ? x [L;R;N] = true.
+* // qed.
+
+definition FinMove ≝ 
+  mk_FinSet DeqMove [L;R;N] move_enum_unique move_enum_complete.
+
+unification hint  0 ≔ ; 
+    X ≟ FinMove
+(* ---------------------------------------- *) ⊢ 
+    move ≡ FinSetcarr X.
+
+definition trans_source ≝ λn.FinProd (initN n) (FinOption FinBool).
+definition trans_target ≝ λn.FinProd (initN n) (FinOption (FinProd FinBool FinMove)).
+
+lemma match_to_trans: 
+  ∀n.∀trans: trans_source n → trans_target n.
+  ∀h,qin,cin,qout,cout,mv.
+  match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h (graph_enum ?? trans))) → 
+  ∃s,t. tuple_of_pair n h 〈s,t〉 = mk_tuple qin cin qout cout mv 
+    ∧ trans s = t.
+#n #trans #h #qin #cin #qout #cout #mv #Hmatch
+cases (match_to_pair … Hmatch) -Hmatch * #s #t * #Heq #Hmem
+@(ex_intro … s) @(ex_intro … t) % // @graph_enum_correct 
+@mem_to_memb @Hmem 
+qed.
+