X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Ftuples.ma;h=f51fdf38461fdf286dc5349ce407572531131846;hb=1695dd8b1861176954666067243c02020e1dcea5;hp=0172f89bfd008e89577db84373b72db6634ab00e;hpb=c20548722d1773bb7ba2b349b2bbb41d94d50b0f;p=helm.git diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma index 0172f89bf..f51fdf384 100644 --- a/matita/matita/lib/turing/universal/tuples.ma +++ b/matita/matita/lib/turing/universal/tuples.ma @@ -18,8 +18,8 @@ include "turing/universal/marks.ma". definition STape ≝ FinProd … FSUnialpha FinBool. -definition only_bits ≝ λl. - ∀c.memb STape c l = true → is_bit (\fst c) = true. +definition only_bits_or_nulls ≝ λl. + ∀c.memb STape c l = true → bit_or_null (\fst c) = true. definition no_grids ≝ λl. ∀c.memb STape c l = true → is_grid (\fst c) = false. @@ -29,18 +29,80 @@ definition no_bars ≝ λl. definition no_marks ≝ λl. ∀c.memb STape c l = true → is_marked ? c = false. - + +lemma bit_not_grid: ∀d. is_bit d = true → is_grid d = false. +* // normalize #H destruct +qed. + +lemma bit_or_null_not_grid: ∀d. bit_or_null d = true → is_grid d = false. +* // normalize #H destruct +qed. + +lemma bit_not_bar: ∀d. is_bit d = true → is_bar d = false. +* // normalize #H destruct +qed. + +lemma bit_or_null_not_bar: ∀d. bit_or_null d = true → is_bar d = false. +* // normalize #H destruct +qed. + +(* by definition, a tuple is not marked *) definition tuple_TM : nat → list STape → Prop ≝ - λn,t.∃qin,qout,mv,b1,b2. - only_bits qin ∧ only_bits qout ∧ only_bits mv ∧ + λn,t.∃qin,qout,mv. + no_marks t ∧ + only_bits_or_nulls qin ∧ only_bits_or_nulls qout ∧ bit_or_null mv = true ∧ |qin| = n ∧ |qout| = n (* ∧ |mv| = ? *) ∧ - t = qin@〈comma,b1〉::qout@〈comma,b2〉::mv. + t = qin@〈comma,false〉::qout@〈comma,false〉::[〈mv,false〉]. inductive table_TM : nat → list STape → Prop ≝ | ttm_nil : ∀n.table_TM n [] -| ttm_cons : ∀n,t1,T,b.tuple_TM n t1 → table_TM n T → table_TM n (t1@〈bar,b〉::T). +| ttm_cons : ∀n,t1,T.tuple_TM n t1 → table_TM n T → table_TM n (t1@〈bar,false〉::T). -axiom no_grids_in_table: ∀n.∀l.table_TM n l → no_grids l. +lemma no_grids_in_table: ∀n.∀l.table_TM n l → no_grids l. +#n #l #t elim t + [normalize #n #x #H destruct + |#m #t1 #t2 * #qin * #qout * #mv * * * * * * + #Hmarks #Hqin #Hqout #Hmv #_ #_ #Heq #Ht2 #Hind + whd >Heq #x #membx + cases (memb_append … membx) -membx #membx + [cases (memb_append … membx) -membx #membx + [@bit_or_null_not_grid @Hqin // + |cases (orb_true_l … membx) -membx #membx + [>(\P membx) // + |cases (memb_append … membx) -membx #membx + [@bit_or_null_not_grid @Hqout // + |cases (orb_true_l … membx) -membx #membx + [>(\P membx) // + |@bit_or_null_not_grid >(memb_single … membx) @Hmv + ] + ] + ] + ] + |cases (orb_true_l … membx) -membx #membx + [>(\P membx) // + |@Hind // + ] + ] + ] +qed. + +lemma no_marks_in_table: ∀n.∀l.table_TM n l → no_marks l. +#n #l #t elim t + [normalize #n #x #H destruct + |#m #t1 #t2 * #qin * #qout * #mv * * * * * * + #Hmarks #_ #_ #_ #_ #_ #_ #Ht2 #Hind + #x #Hx cases (memb_append … Hx) -Hx #Hx + [@Hmarks // + |cases (orb_true_l … Hx) -Hx #Hx + [>(\P Hx) // + |@Hind // + ] + ] + ] +qed. + +axiom last_of_table: ∀n,l,b.¬ table_TM n (l@[〈bar,b〉]). + (* l0 x* a l1 x0* a0 l2 ------> l0 x a* l1 x0 a0* l2 ^ ^ @@ -162,6 +224,109 @@ lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid) ]]]] qed. +definition init_current_on_match ≝ + (seq ? (move_l ?) + (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c))) + (seq ? (move_r ?) (mark ?)))). + +definition R_init_current_on_match ≝ λt1,t2. + ∀l1,l2,c,rs. no_grids l1 → is_grid c = false → + t1 = midtape STape (l1@〈c,false〉::〈grid,false〉::l2) 〈grid,false〉 rs → + t2 = midtape STape (〈grid,false〉::l2) 〈c,true〉 ((reverse ? l1)@〈grid,false〉::rs). + +lemma sem_init_current_on_match : + Realize ? init_current_on_match R_init_current_on_match. +#intape +cases (sem_seq ????? (sem_move_l ?) + (sem_seq ????? (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c))) + (sem_seq ????? (sem_move_r ?) (sem_mark ?))) intape) +#k * #outc * #Hloop #HR +@(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop +#l1 #l2 #c #rs #Hl1 #Hc #Hintape +cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta -Hintape +generalize in match Hl1; cases l1 + [#Hl1 whd in ⊢ ((???(??%%%))→?); #Hta + * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Hta + [* >Hc #Htemp destruct (Htemp) ] + * #_ #Htc lapply (Htc [ ] 〈grid,false〉 ? (refl ??) (refl …) Hl1) + whd in ⊢ ((???(??%%%))→?); -Htc #Htc + * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htc -Htd + whd in ⊢ ((???(??%%%))→?); #Htd + whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc #Houtc + >Houtc % + |#d #tl #Htl whd in ⊢ ((???(??%%%))→?); #Hta + * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Htb + [* >(Htl … (memb_hd …)) #Htemp destruct (Htemp)] + * #Hd >append_cons #Htb lapply (Htb … (refl ??) (refl …) ?) + [#x #membx cases (memb_append … membx) -membx #membx + [@Htl @memb_cons @membx | >(memb_single … membx) @Hc]]-Htb #Htb + * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htb -Htc + >reverse_append >associative_append whd in ⊢ ((???(??%%%))→?); #Htc + whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc) -Houtc #Houtc + >Houtc >reverse_cons >associative_append % + ] +qed. + +(* +definition init_current_gen ≝ + seq ? (adv_to_mark_l ? (is_marked ?)) + (seq ? (clear_mark ?) + (seq ? (move_l ?) + (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c))) + (seq ? (move_r ?) (mark ?))))). + +definition R_init_current_gen ≝ λt1,t2. + ∀l1,c,l2,b,l3,c1,rs,c0,b0. no_marks l1 → no_grids l2 → + Some ? 〈c0,b0〉 = option_hd ? (reverse ? (〈c,true〉::l2)) → + t1 = midtape STape (l1@〈c,true〉::l2@〈grid,b〉::l3) 〈c1,false〉 rs → + t2 = midtape STape (〈grid,b〉::l3) 〈c0,true〉 + ((tail ? (reverse ? (l1@〈c,false〉::l2))@〈c1,false〉::rs)). + +lemma sem_init_current_gen : Realize ? init_current_gen R_init_current_gen. +#intape +cases (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?)) + (sem_seq ????? (sem_clear_mark ?) + (sem_seq ????? (sem_move_l ?) + (sem_seq ????? (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c))) + (sem_seq ????? (sem_move_r ?) (sem_mark ?))))) intape) +#k * #outc * #Hloop #HR +@(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop +#l1 #c #l2 #b #l3 #c1 #rs #c0 #b0 #Hl1 #Hl2 #Hc #Hintape +cases HR -HR #ta * whd in ⊢ (%→?); #Hta cases (Hta … Hintape) -Hta -Hintape + [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ] +* #_ #Hta lapply (Hta l1 〈c,true〉 ? (refl ??) ??) [@Hl1|%] -Hta #Hta +* #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta) -Htb -Hta #Htb +* #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb +generalize in match Hc; generalize in match Hl2; cases l2 + [#_ whd in ⊢ ((???%)→?); #Htemp destruct (Htemp) + whd in ⊢ ((???(??%%%))→?); #Htc + * #td * whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd + [2: * whd in ⊢ (??%?→?); #Htemp destruct (Htemp) ] + * #_ #Htd >Htd in Htc; -Htd #Htd + * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Htd + >reverse_append >reverse_cons + whd in ⊢ ((???(??%%%))→?); #Hte + whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc + >Houtc % + |#d #tl #Htl #Hc0 whd in ⊢ ((???(??%%%))→?); #Htc + * #td * whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd + [* >(Htl … (memb_hd …)) whd in ⊢ (??%?→?); #Htemp destruct (Htemp)] + * #Hd #Htd lapply (Htd … (refl ??) (refl ??) ?) + [#x #membx @Htl @memb_cons @membx] -Htd #Htd + * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Htd + >reverse_append >reverse_cons >reverse_cons + >reverse_cons in Hc0; >reverse_cons cases (reverse ? tl) + [normalize in ⊢ (%→?); #Hc0 destruct (Hc0) #Hte + whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc + >Houtc % + |* #c2 #b2 #tl2 normalize in ⊢ (%→?); #Hc0 destruct (Hc0) + whd in ⊢ ((???(??%%%))→?); #Hte + whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc + >Houtc >associative_append >associative_append >associative_append % + ] + ] +qed. +*) definition init_current ≝ seq ? (adv_to_mark_l ? (is_marked ?)) (seq ? (clear_mark ?) @@ -217,9 +382,9 @@ definition match_tuple_step ≝ definition R_match_tuple_step_true ≝ λt1,t2. ∀ls,c,l1,l2,c1,l3,l4,rs,n. - is_bit c = true → only_bits l1 → no_grids l2 → is_bit c1 = true → - only_bits l3 → n = |l1| → |l1| = |l3| → - table_TM (S n) (〈c1,true〉::l3@〈comma,false〉::l4) → + bit_or_null c = true → only_bits_or_nulls l1 → no_marks l1 (* → no_grids l2 *) → bit_or_null c1 = true → + only_bits_or_nulls l3 → n = |l1| → |l1| = |l3| → + table_TM (S n) (l2@〈bar,false〉::〈c1,false〉::l3@〈comma,false〉::l4) → t1 = midtape STape (〈grid,false〉::ls) 〈c,true〉 (l1@〈grid,false〉::l2@〈bar,false〉::〈c1,true〉::l3@〈comma,false〉::l4@〈grid,false〉::rs) → (* facciamo match *) @@ -229,11 +394,11 @@ definition R_match_tuple_step_true ≝ λt1,t2. ∨ (* non facciamo match e marchiamo la prossima tupla *) ((〈c,false〉::l1 ≠ 〈c1,false〉::l3 ∧ - ∃c2,l5,l6,l7.l4 = l5@〈bar,false〉::〈c2,false〉::l6@〈comma,false〉::l7 ∧ + ∃c2,l5,l6.l4 = l5@〈bar,false〉::〈c2,false〉::l6 ∧ (* condizioni su l5 l6 l7 *) t2 = midtape STape (〈grid,false〉::ls) 〈c,true〉 - (l1@〈grid,false〉::l2@〈bar,false〉::〈c1,true〉::l3@〈comma,false〉:: - l5@〈bar,false〉::〈c2,true〉::l6@〈comma,false〉::l7)) + (l1@〈grid,false〉::l2@〈bar,false〉::〈c1,false〉::l3@〈comma,false〉:: + l5@〈bar,false〉::〈c2,true〉::l6@〈grid,false〉::rs)) ∨ (* non facciamo match e non c'è una prossima tupla: non specifichiamo condizioni sul nastro di output, perché @@ -257,13 +422,11 @@ lemma some_option_hd: ∀A.∀l:list A.∀a.∃b. #A #l #a cases l normalize /2/ qed. -lemma bit_not_grid: ∀d. is_bit d = true → is_grid d = false. -* // normalize #H destruct -qed. - -lemma bit_not_bar: ∀d. is_bit d = true → is_bar d = false. -* // normalize #H destruct -qed. +axiom tech_split2 : ∀A,l1,l2,l3,l4,x. + memb A x l1 = false → memb ? x l3 = false → + l1@x::l2 = l3@x::l4 → l1 = l3 ∧ l2 = l4. + +axiom injective_append : ∀A,l.injective … (λx.append A x l). lemma sem_match_tuple_step: accRealize ? match_tuple_step (inr … (inl … (inr … 0))) @@ -282,11 +445,11 @@ lemma sem_match_tuple_step: [@injective_notb @Hgrid | Htapea1 [2:%] #notgridc -Htapea -Htapea1 -tapea #Htapeb cases (Hcompare … Htapeb) -Hcompare -Htapeb * #_ #_ #Hcompare - cases (Hcompare c c1 l1 l3 (l2@[〈bar,false〉]) (l4@〈grid,false〉::rs) eqlen Hl1 … (refl …) Hc ?) + cases (Hcompare c c1 l1 l3 (l2@[〈bar,false〉]) (l4@〈grid,false〉::rs) eqlen Hl1bars Hl3 Hl1marks … (refl …) Hc ?) -Hcompare [* #Htemp destruct (Htemp) #Htapec %1 % [%] >Htapec in Hor; -Htapec * @@ -303,7 +466,7 @@ lemma sem_match_tuple_step: |#x #tl @not_to_not normalize #H destruct // ] ] #Hnoteq %2 - cut (is_bit d' = true) + cut (bit_or_null d' = true) [cases la in H3; [normalize in ⊢ (%→?); #H destruct // |#x #tl #H @(Hl3 〈d',false〉) @@ -312,37 +475,45 @@ lemma sem_match_tuple_step: ] #Hd' >Htapec in Hor; -Htapec * [* #taped * whd in ⊢ (%→?); #H @False_ind - cases (H … (refl …)) >(bit_not_grid ? Hd') #Htemp destruct (Htemp) + cases (H … (refl …)) >(bit_or_null_not_grid ? Hd') #Htemp destruct (Htemp) |* #taped * whd in ⊢ (%→?); #H cases (H … (refl …)) -H #_ #Htaped * #tapee * whd in ⊢ (%→?); #Htapee <(associative_append ? lc (〈comma,false〉::l4)) in Htaped; #Htaped cases (Htapee … Htaped ???) -Htaped -Htapee [* #rs3 * * (* we proceed by cases on rs4 *) - [(* rs4 is empty *) - * #d * #b * * * #Heq1 #Hnobars - whd in ⊢ ((???%)→?); #Htemp destruct (Htemp) - #Htapee * - [* #tapef * whd in ⊢ (%→?); >Htapee -Htapee #Htapef - cases (Htapef … (refl …)) -Htapef #_ #Htapef >Htapef -Htapef - whd in ⊢ (%→?); #H lapply (H … ???? (refl …)) #Htapeout - %2 % - [% [@Hnoteq |@daemon] - |>Htapeout % - ] - |* #tapef * whd in ⊢ (%→?); >Htapee -Htapee #Htapef - cases (Htapef … (refl …)) whd in ⊢ ((??%?)→?); #Htemp destruct (Htemp) - ] + [(* rs4 is empty : the case is absurd since the tape + cannot end with a bar *) + * #d * #b * * * #Heq1 @False_ind + cut (∀A,l1,l2.∀a:A. a::l1@l2=(a::l1)@l2) [//] #Hcut + >Hcut in Htable; >H3 >associative_append + normalize >Heq1 >Hcut Hcut + Hcut >H3 >associative_append @memb_append_l2 + @memb_cons >Heq1 @memb_append_l2 @memb_cons @memb_hd] #d2intable + cut (is_grid d2 = false) + [@(no_grids_in_table … Htable … 〈d2,b2〉 d2intable)] #Hd2 + cut (b2 = false) + [@(no_marks_in_table … Htable … 〈d2,b2〉 d2intable)] #Hb2 + >Hb2 in Heq1; #Heq1 -Hb2 -b2 whd in ⊢ ((???%)→?); #Htemp destruct (Htemp) #Htapee >Htapee -Htapee * - [* #tapef * whd in ⊢ (%→?); #Htapef + [(* we know current is not grid *) + * #tapef * whd in ⊢ (%→?); #Htapef cases (Htapef … (refl …)) >Hd2 #Htemp destruct (Htemp) |* #tapef * whd in ⊢ (%→?); #Htapef cases (Htapef … (refl …)) #_ -Htapef #Htapef - * #tapeg >Htapef -Htapef * whd in ⊢ (%→?); + * #tapeg >Htapef -Htapef * + (* move_l *) + whd in ⊢ (%→?); #H lapply (H … (refl …)) whd in ⊢ (???%→?); -H #Htapeg - >Htapeg -Htapeg whd in ⊢ (%→?); #Htapeout + >Htapeg -Htapeg + (* init_current *) + whd in ⊢ (%→?); #Htapeout %1 cases (some_option_hd ? (reverse ? (reverse ? la)) 〈c',true〉) * #c00 #b00 #Hoption lapply @@ -357,16 +528,70 @@ lemma sem_match_tuple_step: [normalize in ⊢ (%→?); #Htemp destruct (Htemp) @injective_notb @notgridc |#x #tl normalize in ⊢ (%→?); #Htemp destruct (Htemp) - @bit_not_grid @(Hl1 〈c',false〉) @memb_append_l2 @memb_hd + @bit_or_null_not_grid @(Hl1bars 〈c',false〉) @memb_append_l2 @memb_hd ] - |cut (only_bits (la@(〈c',false〉::lb))) + |cut (only_bits_or_nulls (la@(〈c',false〉::lb))) [

(\P eqc0) @Hc |@Hl1] - |#Hl1' #x #Hx @bit_not_grid @Hl1' + [#eqc0 >(\P eqc0) @Hc |@Hl1bars] + |#Hl1' #x #Hx @bit_or_null_not_grid @Hl1' @memb_append_l1 @daemon ] |@daemon - |@daemon + |>reverse_append >reverse_cons >reverse_reverse + >reverse_append >reverse_reverse + >reverse_cons >reverse_append >reverse_reverse + >reverse_append >reverse_cons >reverse_reverse + >reverse_reverse + #Htapeout % [@Hnoteq] + @(ex_intro … d2) + cut (∃rs32.rs3 = lc@〈comma,false〉::rs32) + [ (*cases (tech_split STape (λc.c == 〈bar,false〉) l4) + [ + | * #l41 * * #cbar #bfalse * #l42 * * #Hbar #Hl4 #Hl41 + @(ex_intro ?? l41) >Hl4 in Heq1; #Heq1 + + cut (sublist … lc l3) + [ #x #Hx cases la in H3; + [ normalize #H3 destruct (H3) @Hx + | #p #la' normalize #Hla' destruct (Hla') + @memb_append_l2 @memb_cons @Hx ] ] #Hsublist*) + @daemon] + * #rs32 #Hrs3 + (* cut + (〈c1,false〉::l3@〈comma,false〉::l4= la@〈d',false〉::rs3@〈bar,false〉::〈d2,b2〉::rs3') + [@daemon] #Hcut *) + cut (l4=rs32@〈bar,false〉::〈d2,false〉::rs3') + [ >Hrs3 in Heq1; @daemon ] #Hl4 + @(ex_intro … rs32) @(ex_intro … rs3') % + [@Hl4 + |>Htapeout @eq_f2 + [@daemon + |(*>Hrs3 *)>append_cons + > (?:l1@〈grid,false〉::l2@〈bar,false〉::〈c1,false〉::l3@〈comma,false〉::rs32@〈bar,false〉::〈d2,true〉::rs3'@〈grid,false〉::rs + = (l1@〈grid,false〉::l2@〈bar,false〉::〈c1,false〉::l3@〈comma,false〉::rs32@[〈bar,false〉])@〈d2,true〉::rs3'@〈grid,false〉::rs) + [|>associative_append normalize + >associative_append normalize + >associative_append normalize + >associative_append normalize + % ] + @eq_f2 [|%] + @(injective_append … (〈d2,false〉::rs3')) + >(?:(la@[〈c',false〉])@((((lb@[〈grid,false〉])@l2@[〈bar,false〉])@la)@[〈d',false〉])@rs3 + =((la@〈c',false〉::lb)@([〈grid,false〉]@l2@[〈bar,false〉]@la@[〈d',false〉]@rs3))) + [|>associative_append >associative_append + >associative_append >associative_append >associative_append + >associative_append >associative_append % ] +

associative_append >associative_append >associative_append + @eq_f normalize @eq_f >associative_append + >associative_append @eq_f normalize @eq_f + >(append_cons ? 〈d',false〉) >associative_append + Hl4 associative_append normalize + >associative_append normalize % + ] + ] ] ] ] @@ -385,25 +610,54 @@ lemma sem_match_tuple_step: cases (Htapef … (refl …)) -Htapef whd in ⊢ ((??%?)→?); #Htemp destruct (Htemp) ] - |@daemon (* no marks in table *) + |(* no marks in table *) + #x #membx @(no_marks_in_table … Htable) + @memb_append_l2 @memb_cons + cut (∀A,l1,l2.∀a:A. a::l1@l2=(a::l1)@l2) [//] #Hcut >Hcut + >H3 >associative_append @memb_append_l2 @memb_cons @membx |(* no grids in table *) - #x #Hx cases (memb_append … Hx) - [-Hx #Hx @bit_not_grid @Hl3 cases la in H3; normalize - [#H3 destruct (H3) @Hx | #y #tl #H3 destruct (H3) - @memb_append_l2 @memb_cons @Hx ] - |-Hx #Hx @(no_grids_in_table … Htable) - @memb_cons @memb_append_l2 @Hx - ] - |whd in ⊢ (??%?); >(bit_not_grid … Hd') >(bit_not_bar … Hd') % + #x #membx @(no_grids_in_table … Htable) + @memb_append_l2 @memb_cons + cut (∀A,l1,l2.∀a:A. a::l1@l2=(a::l1)@l2) [//] #Hcut >Hcut + >H3 >associative_append @memb_append_l2 @memb_cons @membx + |whd in ⊢ (??%?); >(bit_or_null_not_grid … Hd') >(bit_or_null_not_bar … Hd') % ] ] - |@Hl3 - |@daemon - |@daemon - |@daemon + |#x #membx @(no_marks_in_table … Htable) + @memb_append_l2 @memb_cons @memb_cons @memb_append_l1 @membx + |#x #membx @(no_marks_in_table … Htable) + cases (memb_append … membx) -membx #membx + [@memb_append_l1 @membx | @memb_append_l2 >(memb_single … membx) @memb_hd] |>associative_append % ] ] qed. - \ No newline at end of file + +(* + MATCH TUPLE + + scrolls through the tuples in the transition table until one matching the + current configuration is found +*) + +definition match_tuple ≝ whileTM ? match_tuple_step (inr … (inl … (inr … 0))). + +definition R_match_tuple ≝ λt1,t2. + ∀ls,c,l1,c1,l2,rs,n. + is_bit c = true → only_bits_or_nulls l1 → is_bit c1 = true → n = |l1| → + table_TM (S n) (〈c1,false〉::l2) → + t1 = midtape STape (〈grid,false〉::ls) 〈c,true〉 + (l1@〈grid,false〉::〈c1,true〉::l2@〈grid,false〉::rs) → + (* facciamo match *) + (∃l3,newc,mv,l4. + 〈c1,false〉::l2 = l3@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv@l4 ∧ + t2 = midtape ? (reverse ? l1@〈c,false〉::〈grid,false〉::ls) 〈grid,false〉 + (l3@〈c,false〉::l1@〈comma,true〉::newc@〈comma,false〉::mv@l4@〈grid,false〉::rs)) + ∨ + (* non facciamo match su nessuna tupla; + non specifichiamo condizioni sul nastro di output, perché + non eseguiremo altre operazioni, quindi il suo formato non ci interessa *) + (current ? t2 = Some ? 〈grid,true〉 ∧ + ∀l3,newc,mv,l4. + 〈c1,false〉::l2 ≠ l3@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv@l4).