From: Wilmer Ricciotti Date: Wed, 23 May 2012 14:32:15 +0000 (+0000) Subject: Progress X-Git-Tag: make_still_working~1699 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=690675dde36407d039e9d05047bc7909202170c1;p=helm.git Progress --- diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma index fc3e3f633..2f5a342d6 100644 --- a/matita/matita/lib/turing/universal/move_tape.ma +++ b/matita/matita/lib/turing/universal/move_tape.ma @@ -321,17 +321,6 @@ definition sim_current_of_tape ≝ λt. [ None ⇒ 〈null,false〉 | Some c0 ⇒ c0 ]. -definition mk_tuple ≝ λc,newc,mv. - c @ 〈comma,false〉:: newc @ 〈comma,false〉 :: [〈mv,false〉]. - -inductive match_in_table (c,newc:list STape) (mv:unialpha) : list STape → Prop ≝ -| mit_hd : - ∀tb. - match_in_table c newc mv (mk_tuple c newc mv@〈bar,false〉::tb) -| mit_tl : - ∀c0,newc0,mv0,tb. - match_in_table c newc mv tb → - match_in_table c newc mv (mk_tuple c0 newc0 mv0@〈bar,false〉::tb). definition move_of_unialpha ≝ λc.match c with @@ -499,10 +488,9 @@ qed. definition R_move_tape_l_abstract ≝ λt1,t2. ∀rs,n,table,curc,curconfig,ls. - bit_or_null curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) → + is_bit curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) → t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls) 〈grid,false〉 rs → - no_nulls ls → no_marks ls → legal_tape ls 〈curc,false〉 rs → ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs → ∃ls1,rs1,newc. @@ -515,7 +503,7 @@ lemma mtl_concrete_to_abstract : ∀t1,t2.R_move_tape_l t1 t2 → R_move_tape_l_abstract t1 t2. #t1 #t2 whd in ⊢(%→?); #Hconcrete #rs #n #table #curc #curconfig #ls #Hcurc #Hcurconfig #Htable #Ht1 -#Hlsnonulls #Hlsnomarks #Htape #t1' #Ht1' +* * * #Hnomarks #Hbits #Hcurc #Hlegal #t1' #Ht1' cases (Hconcrete … Htable Ht1) // [ * #Hls #Ht2 @(ex_intro ?? []) @@ -524,24 +512,51 @@ cases (Hconcrete … Htable Ht1) // [ % [ >Ht2 % | >Hls % ] - | % % % ] -| * * #l0 #bl0 * #ls0 * #Hls - cut (bl0 = false) [@(Hlsnomarks 〈l0,bl0〉) >Hls @memb_hd] + | % [ % [ % + [ #x #Hx cases (orb_true_l … Hx) #Hx' + [ >(\P Hx') % + | @Hnomarks >Hls @Hx' ] + | #x #Hx cases (orb_true_l … Hx) #Hx' + [ >(\P Hx') // + | @Hbits >Hls @Hx' ]] + | % ] + | % %2 % ] + ] +| * * #l0 #bl0 * #ls0 * #Hls + cut (bl0 = false) + [ @(Hnomarks 〈l0,bl0〉) @memb_cons @memb_append_l1 >Hls @memb_hd] #Hbl0 >Hbl0 in Hls; #Hls #Ht2 - @(ex_intro ?? ls0) - @(ex_intro ?? (〈curc,false〉::rs)) + @(ex_intro ?? ls0) @(ex_intro ?? (〈curc,false〉::rs)) @(ex_intro ?? l0) % [ % [ >Ht2 % | >Hls >lift_tape_not_null [ % - | @(Hlsnonulls 〈l0,false〉) >Hls @memb_hd ] ] - | @legal_tape_conditions % % % #Hl0 >Hl0 in Hls; #Hls - lapply (Hlsnonulls 〈null,false〉 ?) - [ >Hls @memb_hd | normalize #H destruct (H) ] - ] -qed. - + | @bit_not_null @(Hbits 〈l0,false〉) >Hls @memb_append_l1 @memb_hd ] ] + | % [ % [ % + [ #x #Hx cases (orb_true_l … Hx) #Hx' + [ >(\P Hx') % + | cases (memb_append … Hx') #Hx'' @Hnomarks + [ >Hls @memb_cons @memb_cons @(memb_append_l1 … Hx'') + | cases (orb_true_l … Hx'') #Hx''' + [ >(\P Hx''') @memb_hd + | @memb_cons @(memb_append_l2 … Hx''')] + ] + ] + | whd in ⊢ (?%); #x #Hx cases (memb_append … Hx) #Hx' + [ @Hbits >Hls @memb_cons @(memb_append_l1 … Hx') + | cases (orb_true_l … Hx') #Hx'' + [ >(\P Hx'') // + | @Hbits @(memb_append_l2 … Hx'') + ]]] + | whd in ⊢ (??%?); >(Hbits 〈l0,false〉) // + @memb_append_l1 >Hls @memb_hd ] + | % % % #Hl0 lapply (Hbits 〈l0,false〉?) + [ @memb_append_l1 >Hls @memb_hd + | >Hl0 normalize #Hfalse destruct (Hfalse) + ] ] ] ] +qed. + lemma Realize_to_Realize : ∀alpha,M,R1,R2.(∀t1,t2.R1 t1 t2 → R2 t1 t2) → Realize alpha M R1 → Realize alpha M R2. #alpha #M #R1 #R2 #Himpl #HR1 #intape @@ -606,21 +621,21 @@ definition move_tape ≝ tc_true) tc_true. definition R_move_tape ≝ λt1,t2. - ∀rs,n,table1,c,table2,curc,curconfig,ls. - bit_or_null curc = true → bit_or_null c = true → only_bits_or_nulls curconfig → - table_TM n (reverse ? table1@〈c,false〉::table2) → + ∀rs,n,table1,mv,table2,curc,curconfig,ls. + bit_or_null mv = true → only_bits_or_nulls curconfig → + (is_bit mv = true → is_bit curc = true) → + table_TM n (reverse ? table1@〈mv,false〉::table2) → t1 = midtape STape (table1@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls) - 〈c,false〉 (table2@〈grid,false〉::rs) → - no_nulls ls → no_nulls rs → no_marks ls → no_marks rs → + 〈mv,false〉 (table2@〈grid,false〉::rs) → legal_tape ls 〈curc,false〉 rs → ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs → ∃ls1,rs1,newc. legal_tape ls1 〈newc,false〉 rs1 ∧ (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉:: - 〈grid,false〉::reverse ? table1@〈c,false〉::table2@〈grid,false〉::rs1) ∧ - ((c = bit false ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_left STape ls 〈curc,false〉 rs) ∨ - (c = bit true ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_right STape ls 〈curc,false〉 rs) ∨ - (c = null ∧ ls1 = ls ∧ rs1 = rs ∧ curc = newc))). + 〈grid,false〉::reverse ? table1@〈mv,false〉::table2@〈grid,false〉::rs1) ∧ + ((mv = bit false ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_left STape ls 〈curc,false〉 rs) ∨ + (mv = bit true ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_right STape ls 〈curc,false〉 rs) ∨ + (mv = null ∧ ls1 = ls ∧ rs1 = rs ∧ curc = newc))). lemma sem_move_tape : Realize ? move_tape R_move_tape. #intape @@ -632,17 +647,19 @@ cases (sem_if ? (test_char ??) … tc_true (sem_test_char ? (λc:STape.c == 〈b (sem_seq … (sem_move_l …) (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))))) intape) #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop -#rs #n #table1 #c #table2 #curc #curconfig #ls -#Hcurc #Hc #Hcurconfig #Htable #Hintape #Hls #Hrs #Hls1 #Hrs1 #Htape #t1' #Ht1' +#rs #n #table1 #mv #table2 #curc #curconfig #ls +#Hmv #Hcurconfig #Hmvcurc #Htable #Hintape #Htape #t1' #Ht1' generalize in match HR; -HR * -[ * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈c,false〉 ?) +[ * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈mv,false〉 ?) [| >Hintape % ] -Hta #Hceq #Hta lapply (\P Hceq) -Hceq #Hceq destruct (Hta Hceq) * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hintape) -Htb -Hintape [ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] * #_ #Htb lapply (Htb … (refl ??) (refl ??) ?) [ @daemon ] -Htb >append_cons reverse_append >reverse_append >reverse_reverse @Htable |] + [ >reverse_append >reverse_append >reverse_reverse @Htable + | /2/ + ||] -Houtc -Htb * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) % [ // @@ -651,18 +668,19 @@ generalize in match HR; -HR * >associative_append >associative_append % | % % % // ] ] -| * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈c,false〉 ?) - [| >Hintape % ] -Hta #Hcneq cut (c ≠ bit false) +| * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈mv,false〉 ?) + [| >Hintape % ] -Hta #Hcneq cut (mv ≠ bit false) [ lapply (\Pf Hcneq) @not_to_not #Heq >Heq % ] -Hcneq #Hcneq #Hta destruct (Hta) * - [ * #tb * whd in ⊢ (%→?);#Htb cases (Htb 〈c,false〉 ?) + [ * #tb * whd in ⊢ (%→?);#Htb cases (Htb 〈mv,false〉 ?) [| >Hintape % ] -Htb #Hceq #Htb lapply (\P Hceq) -Hceq #Hceq destruct (Htb Hceq) * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Hintape) -Htc -Hintape [ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?) [ @daemon ] -Htc >append_cons reverse_append >reverse_append >reverse_reverse @Htable |] + [ >reverse_append >reverse_append >reverse_reverse @Htable + | /2/ |] -Houtc -Htc * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) % [ // @@ -671,15 +689,16 @@ generalize in match HR; -HR * >associative_append >associative_append % | % %2 % // ] ] - | * #tb * whd in ⊢ (%→?); #Htb cases (Htb 〈c,false〉 ?) - [| >Hintape % ] -Htb #Hcneq' cut (c ≠ bit true) + | * #tb * whd in ⊢ (%→?); #Htb cases (Htb 〈mv,false〉 ?) + [| >Hintape % ] -Htb #Hcneq' cut (mv ≠ bit true) [ lapply (\Pf Hcneq') @not_to_not #Heq >Heq % ] -Hcneq' #Hcneq' #Htb destruct (Htb) * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Hintape) - [ * >(bit_or_null_not_grid … Hc) #Hfalse destruct (Hfalse) ] -Htc + [ * >(bit_or_null_not_grid … Hmv) #Hfalse destruct (Hfalse) ] -Htc * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?) [@daemon] -Htc #Htc * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd -Htc whd in ⊢ (???%→?); #Htd whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc * - [ * >(bit_or_null_not_grid … Hcurc) #Hfalse destruct (Hfalse) ] + [ * cases Htape * * #_ #_ #Hcurc #_ + >(bit_or_null_not_grid … Hcurc) #Hfalse destruct (Hfalse) ] * #_ #Houtc lapply (Houtc … (refl ??) (refl ??) ?) [@daemon] -Houtc #Houtc @(ex_intro ?? ls) @(ex_intro ?? rs) @(ex_intro ?? curc) % [ // @@ -687,7 +706,7 @@ generalize in match HR; -HR * [ @Houtc | %2 % // % // % // generalize in match Hcneq; generalize in match Hcneq'; - cases c in Hc; normalize // + cases mv in Hmv; normalize // [ * #_ normalize [ #Hfalse @False_ind cases Hfalse /2/ | #_ #Hfalse @False_ind cases Hfalse /2/ ] |*: #Hfalse destruct (Hfalse) ] ] diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma index b8c0a7ed4..7967331b5 100644 --- a/matita/matita/lib/turing/universal/tuples.ma +++ b/matita/matita/lib/turing/universal/tuples.ma @@ -49,17 +49,66 @@ lemma bit_or_null_not_bar: ∀d. bit_or_null d = true → is_bar d = false. * // normalize #H destruct qed. +definition mk_tuple ≝ λqin,cin,qout,cout,mv. + qin @ cin :: 〈comma,false〉:: qout @ cout :: 〈comma,false〉 :: [mv]. + (* by definition, a tuple is not marked *) definition tuple_TM : nat → list STape → Prop ≝ - λ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,false〉::qout@〈comma,false〉::[〈mv,false〉]. + λn,t.∃qin,cin,qout,cout,mv. + no_marks qin ∧ no_marks qout ∧ + 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 ∧ + t = mk_tuple qin 〈cin,false〉 qout 〈cout,false〉 〈mv,false〉. -inductive table_TM : nat → list STape → Prop ≝ -| ttm_nil : ∀n.table_TM n [] -| ttm_cons : ∀n,t1,T.tuple_TM n t1 → table_TM n T → table_TM n (t1@〈bar,false〉::T). +inductive table_TM (n:nat) : list STape → Prop ≝ +| ttm_nil : table_TM n [] +| ttm_cons : ∀t1,T.tuple_TM n t1 → table_TM n T → table_TM n (t1@〈bar,false〉::T). + +inductive match_in_table (qin:list STape) (cin: STape) + (qout:list STape) (cout:STape) (mv:STape) +: list STape → Prop ≝ +| mit_hd : + ∀tb. + match_in_table qin cin qout cout mv + (mk_tuple qin cin qout cout mv @〈bar,false〉::tb) +| mit_tl : + ∀qin0,cin0,qout0,cout0,mv0,tb. + match_in_table qin cin qout cout mv tb → + match_in_table qin cin qout cout mv + (mk_tuple qin0 cin0 qout0 cout0 mv0@〈bar,false〉::tb). + +axiom append_l1_injective : + ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l1 = l2. +axiom append_l2_injective : + ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l3 = l4. + + +lemma generic_match_to_match_in_table : + ∀n,T.table_TM n T → + ∀qin,cin,qout,cout,mv.|qin| = n → |qout| = n → + ∀t1,t2. + T = t1@qin@cin::〈comma,false〉::qout@cout::〈comma,false〉::mv::t2 → + match_in_table qin cin qout cout mv T. +#n #T #Htable #qin #cin #qout #cout #mv #Hlenqin #Hlenqout +elim Htable +[ #t1 #t2 Htuple normalize in ⊢ (??%%→?); + >associative_append #HT + cut (qin0 = qin ∧ (〈cin0,false〉 = cin ∧ (qout0 = qout ∧ + (〈cout0,false〉 = cout ∧ (〈mv0,false〉 = mv ∧ 〈bar,false〉::T0 = t2))))) + [ lapply (append_l1_injective … HT) [ >Hlenqin @Hlenqin0 ] + #Hqin % [ @Hqin ] -Hqin + lapply (append_l2_injective … HT) [ >Hlenqin @Hlenqin0 ] -HT #HT + destruct (HT) + lemma no_grids_in_table: ∀n.∀l.table_TM n l → no_grids l. #n #l #t elim t diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma index 1811d5a19..128c81aa5 100644 --- a/matita/matita/lib/turing/universal/uni_step.ma +++ b/matita/matita/lib/turing/universal/uni_step.ma @@ -254,9 +254,9 @@ definition map_move ≝ definition R_exec_move ≝ λt1,t2. ∀n,curconfig,ls,rs,c0,c1,s0,s1,table1,newconfig,mv,table2. table_TM n (table1@〈comma,false〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2) → - no_marks curconfig → only_bits (curconfig@[〈s0,false〉]) → only_bits (〈s1,false〉::newconfig) → + no_marks curconfig → only_bits (curconfig@[〈s0,false〉]) → + only_bits (〈s1,false〉::newconfig) → bit_or_null c1 = true → |curconfig| = |newconfig| → - no_nulls ls → no_nulls rs → no_marks ls → no_marks rs → legal_tape ls 〈c0,false〉 rs → t1 = midtape STape (〈c0,false〉::curconfig@〈s0,false〉::〈grid,false〉::ls) 〈grid,false〉 (table1@〈comma,true〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) → @@ -298,6 +298,33 @@ lemma merge_char_not_null : ] qed. +lemma merge_char_null : ∀c.merge_char null c = c. +* // +qed. + +lemma merge_char_cases : ∀c1,c2.merge_char c1 c2 = c1 ∨ merge_char c1 c2 = c2. +#c1 * +[ #c1' %2 % +| % % +| *: %2 % ] +qed. + +(* lemma merge_char_c_bit : + ∀c1,c2.is_bit c2 = true → merge_char c1 c2 = c2. +#c1 * +[ #c2' #_ % +|*: normalize #Hfalse destruct (Hfalse) ] +qed. + +lemma merge_char_c_bit : + ∀c1,c2.is_null c2 = true → merge_char c1 c2 = c1. +#c1 * +[ #c2' #_ % +|*: normalize #Hfalse destruct (Hfalse) ] +qed. + +*) + lemma sem_exec_move : Realize ? exec_move R_exec_move. #intape cases (sem_seq … sem_init_copy @@ -306,7 +333,7 @@ cases (sem_seq … sem_init_copy #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [ @Hloop ] -Hloop #n #curconfig #ls #rs #c0 #c1 #s0 #s1 #table1 #newconfig #mv #table2 -#Htable #Hcurconfig1 #Hcurconfig2 #Hnewconfig #Hlen #Hls #Hrs #Hls1 #Hrs1 #Htape #Hintape #t1' #Ht1' +#Htable #Hcurconfig1 #Hcurconfig2 #Hnewconfig #Hc1 #Hlen #Htape #Hintape #t1' #Ht1' cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1 (newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) … Hintape) -Hta @@ -321,17 +348,20 @@ lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1 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) - mv table2 (merge_char c0 c1) (reverse ? newconfig@[〈s1,false〉]) ls ????? - Hls Hrs Hls1 Hrs1 ???) - [3: cases (true_or_false (c0 == null)) #Hc0 - [ >(\P Hc0) in Htape; #Htape cases (legal_tape_cases … Htape) - [ * #Hfalse @False_ind /2/ - | * #_ * - [ #Hlsnil @legal_tape_conditions % %2 // - | #Hrsnil @legal_tape_conditions %2 // - ] - ] - | @legal_tape_conditions % % @merge_char_not_null @(\Pf Hc0) ] + mv table2 (merge_char c0 c1) (reverse ? newconfig@[〈s1,false〉]) ls ????????) + [3: cases Htape -Htape * * #Hnomarks #Hbits #Hc0 #Hlsrs % [ % [ % + [ #x #Hx cases (orb_true_l … Hx) #Hx' + [ >(\P Hx') % + | @Hnomarks @memb_cons // ] + | @Hbits ] + | cases (merge_char_cases c0 c1) #Hmerge >Hmerge // ] + | cases (true_or_false (c0 == null)) #Hc0' + [ cases Hlsrs -Hlsrs + [ * + [ >(\P Hc0') * #Hfalse @False_ind /2/ + | #Hlsnil % %2 // ] + | #Hrsnil %2 // ] + | % % @merge_char_not_null @(\Pf Hc0') ] ] |4:>Htc @(eq_f3 … (midtape ?)) [ @eq_f @eq_f >associative_append >associative_append % | % @@ -342,9 +372,9 @@ lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1 >associative_append >associative_append >associative_append >associative_append >associative_append @Htable + | (* well formedness of table *) @daemon | (* Hnewconfig *) @daemon - | (* bit_or_null mv = true *) @daemon - | (* bit_or_null c1,c2 → bit_or_null (merge_char c1 c2) *) @daemon + | (* bit_or_null mv = true (well formedness of table) *) @daemon | -Houtc * #ls1 * #rs1 * #newc * #Hnewtapelegal * #Houtc * [ * [ * #Hmv #Htapemove @@ -361,14 +391,8 @@ lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1 | >Hmv >Ht1' >Htapemove (* mv = bit false -→ c1 = bit ? *) cut (∃c1'.c1 = bit c1') [ @daemon ] * #c1' #Hc1 - >Hc1 >tape_move_left_eq cases (legal_tape_cases … Htape) - [ #Hc0 >lift_tape_not_null /2/ - | * #Hc0 * - [ #Hls >Hc0 >Hls whd in ⊢ (??%%); cases rs; - [%| #r0 #rs0 %] - | #Hrs >Hc0 >Hrs cases ls; [%| #l0 #ls0 %] - ] - ] + >Hc1 >tape_move_left_eq >(legal_tape_left … Htape) + >(legal_tape_right … Htape) % ] | // ] @@ -384,38 +408,34 @@ lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1 >associative_append >associative_append % |>Hmv >Ht1' >Htapemove cut (∃c1'.c1 = bit c1') [ @daemon ] * #c1' #Hc1 - >Hc1 >tape_move_right_eq cases (legal_tape_cases … Htape) - [ #Hc0 >lift_tape_not_null /2/ - | * #Hc0 * - [ #Hls >Hc0 >Hls whd in ⊢ (??%%); cases rs; - [%| #r0 #rs0 %] - | #Hrs >Hc0 >Hrs cases ls; [%| #l0 #ls0 %] - ] + >Hc1 >tape_move_right_eq >(legal_tape_left … Htape) + >(legal_tape_right … Htape) % ] + | // ] - | // ] - ] - | * * * #Hmv #Hlseq #Hrseq #Hnewc - @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) % - [ % - [ >Houtc -Houtc >reverse_append - >reverse_reverse >reverse_single @eq_f - >reverse_cons >reverse_cons >reverse_append >reverse_cons - >reverse_cons >reverse_reverse >reverse_reverse - >associative_append >associative_append - >associative_append >associative_append - >associative_append >associative_append % - |>Hmv >Ht1' cases c1 in Hnewc; - [ #c1' whd in ⊢ (??%?→?);#Hnewc Hlseq >Hrseq cases Htape * #Hleft #Hright #_ - whd in ⊢ (??%%); >Hleft >Hright % - | whd in ⊢ (??%?→?); #Hnewc >Hnewc >Hlseq >Hrseq % - |*: whd in ⊢ (??%?→?);#Hnewc Hlseq >Hrseq cases Htape * #Hleft #Hright #_ - whd in ⊢ (??%%); >Hleft >Hright % ] + | * * * #Hmv #Hlseq #Hrseq #Hnewc + @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) % + [ % + [ >Houtc -Houtc >reverse_append + >reverse_reverse >reverse_single @eq_f + >reverse_cons >reverse_cons >reverse_append >reverse_cons + >reverse_cons >reverse_reverse >reverse_reverse + >associative_append >associative_append + >associative_append >associative_append + >associative_append >associative_append % + |>Hmv >Ht1' cases c1 in Hnewc; + [ #c1' whd in ⊢ (??%?→?);#Hnewc Hlseq >Hrseq whd in ⊢ (??%%); + >(legal_tape_left … Htape) >(legal_tape_right … Htape) % + | whd in ⊢ (??%?→?); #Hnewc >Hnewc >Hlseq >Hrseq % + |*: whd in ⊢ (??%?→?);#Hnewc Hlseq >Hrseq whd in ⊢ (??%%); + >(legal_tape_left … Htape) >(legal_tape_right … Htape) % + ] + ] + | // ] - | // ] ] ] @@ -504,7 +524,6 @@ lemma sem_uni_step : cut (mv1 = 〈\fst mv1,false〉) [ >(eq_pair_fst_snd … mv1) @eq_f (*Htable, Htableeq*) @daemon ] #Hmv1 * #te * whd in ⊢ (%→?); #Hte - (* mv1 ha tipo lista ma dovrebbe avere tipo unialpha *) cut (td = midtape STape (〈c0,false〉::reverse STape curconfig@〈s0,false〉::〈grid,false〉::ls) 〈grid,false〉 ((table1@〈s0,false〉::curconfig@[〈c0,false〉])@〈comma,true〉::〈s1,false〉:: @@ -517,8 +536,8 @@ lemma sem_uni_step : ] -Htd #Htd lapply (Hte … (S n) … Htd … Ht1') -Htd -Hte [ // - |2,3,4,5: (* dovrebbe scomparire (lo metteremo nel legal_tape) *) @daemon | (*|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