\ / GNU General Public License Version 2
V_____________________________________________________________*)
-include "turing/universal/move_char_c.ma".
-include "turing/universal/move_char_l.ma".
+include "turing/move_char.ma".
+include "turing/universal/marks.ma".
include "turing/universal/tuples.ma".
definition init_cell_states ≝ initN 2.
(* l1 # l2 r ---> l1 r # l2
^ ^
*)
-definition mtr_aux ≝
- seq ? (move_l …) (seq ? (move_char_l STape 〈grid,false〉)
- (swap STape 〈grid,false〉)).
-definition R_mtr_aux ≝ λt1,t2.
+definition move_after_left_bar ≝
+ move_l … · move_char_l STape 〈grid,false〉 · swap_r STape 〈grid,false〉.
+
+definition R_move_after_left_bar ≝ λt1,t2.
∀l1,l2,l3,r. t1 = midtape STape (l2@〈grid,false〉::l1) r l3 → no_grids l2 →
t2 = midtape STape l1 r (〈grid,false〉::reverse ? l2@l3).
-lemma sem_mtr_aux : Realize ? mtr_aux R_mtr_aux.
+lemma sem_move_after_left_bar : Realize ? move_after_left_bar R_move_after_left_bar.
#intape
cases (sem_seq … (sem_move_l …) (sem_seq … (ssem_move_char_l STape 〈grid,false〉)
- (sem_swap STape 〈grid,false〉)) intape)
+ (sem_swap_r STape 〈grid,false〉)) intape)
#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
#l1 #l2 #l3 #r #Hintape #Hl2
-cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
+cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (proj2 ?? Hta … Hintape) -Hta #Hta
* #tb * whd in ⊢(%→?); generalize in match Hta; -Hta cases l2 in Hl2;
[ #_ #Hta #Htb lapply (Htb … Hta) -Htb * #Htb lapply (Htb (refl ??)) -Htb #Htb #_
- whd in ⊢(%→?); >Htb #Houtc lapply (Houtc … Hta) -Houtc #Houtc @Houtc
+ whd in ⊢(%→?); >Htb #Houtc lapply (proj2 ?? Houtc … Hta) -Houtc #Houtc @Houtc
| #c0 #l0 #Hnogrids #Hta #Htb lapply (Htb … Hta) -Htb * #_ #Htb
lapply (Htb … (refl ??) ??)
[ cases (true_or_false (memb STape 〈grid,false〉 l0)) #Hmemb
| @Hmemb ]
| % #Hc0 lapply (Hnogrids c0 ?)
[ @memb_hd | >Hc0 normalize #Hfalse destruct (Hfalse) ]
- | #Htb whd in ⊢(%→?); >Htb #Houtc lapply (Houtc … (refl ??)) -Houtc #Houtc
+ | #Htb whd in ⊢(%→?); >Htb #Houtc lapply (proj2 ?? Houtc … (refl ??)) -Houtc #Houtc
>reverse_cons >associative_append @Houtc
]]
qed.
definition move_tape_r ≝
- seq ? (move_r …) (seq ? init_cell (seq ? (move_l …)
- (seq ? (swap STape 〈grid,false〉)
- (seq ? mtr_aux (seq ? (move_l …) (seq ? mtr_aux (move_r …))))))).
+ move_r … · init_cell · move_l … · swap_r STape 〈grid,false〉 ·
+ move_after_left_bar · move_l … · move_after_left_bar · move_r ….
definition R_move_tape_r ≝ λt1,t2.
∀rs,n,table,c0,bc0,curconfig,ls0.
lemma sem_move_tape_r : Realize ? move_tape_r R_move_tape_r.
#tapein
cases (sem_seq …(sem_move_r …) (sem_seq … sem_init_cell (sem_seq … (sem_move_l …)
- (sem_seq … (sem_swap STape 〈grid,false〉) (sem_seq … sem_mtr_aux
- (sem_seq … (sem_move_l …) (sem_seq … sem_mtr_aux (sem_move_r …))))))) tapein)
+ (sem_seq … (sem_swap_r STape 〈grid,false〉) (sem_seq … sem_move_after_left_bar
+ (sem_seq … (sem_move_l …) (sem_seq … sem_move_after_left_bar (sem_move_r …))))))) tapein)
#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
#rs #n #table #c0 #bc0 #curconfig #ls0 #Hbitnullc0 #Hbitnullcc #Htable #Htapein
-cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Htapein) -Hta #Hta
+cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (proj2 ?? Hta … Htapein) -Hta #Hta
* #tb * whd in ⊢ (%→?); *
[ * #r0 *
generalize in match Hta; generalize in match Htapein; -Htapein -Hta cases rs
[ #_ #Hta >Hta normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
#r1 #rs1 #Htapein #Hta change with (midtape ?? r1 rs1) in Hta:(???%); >Hta
- #Hr0 whd in Hr0:(??%?); #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc #Htc
- * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd #Htd
- * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?) [ (*memb_reverse @(no_grids_in_table … Htable)*) @daemon ] -Hte #Hte
- * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf #Htf
+ #Hr0 whd in Hr0:(??%?); #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (proj2 ?? Htc … Htb) -Htc #Htc
+ * #td * whd in ⊢ (%→?); #Htd lapply (proj2 ?? Htd … Htc) -Htd #Htd
+ * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?) [ #x #memx @(no_grids_in_table … Htable) @memb_reverse @memx]
+ -Hte #Hte
+ * #tf * whd in ⊢ (%→?); #Htf lapply (proj2 ?? Htf … Hte) -Htf #Htf
* #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?) [ #x #Hx @bit_or_null_not_grid @Hbitnullcc // ] -Htg #Htg
- whd in ⊢ (%→?); #Houtc lapply (Houtc … Htg) -Houtc #Houtc
+ whd in ⊢ (%→?); #Houtc lapply (proj2 ?? Houtc … Htg) -Houtc #Houtc
%2 @(ex_intro ?? r1) @(ex_intro ?? rs1) % [%] @Houtc
| * generalize in match Hta; generalize in match Htapein; -Htapein -Hta cases rs
[|#r1 #rs1 #_ #Hta >Hta normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
#Htapein #Hta change with (rightof ???) in Hta:(???%); >Hta
- #Hr0 whd in Hr0:(??%?); #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc #Htc
- * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd #Htd
- * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?) [(*same as above @(no_grids_in_table … Htable) *) @daemon ] -Hte #Hte
- * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf #Htf
+ #Hr0 whd in Hr0:(??%?); #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (proj2 ?? Htc … Htb) -Htc #Htc
+ * #td * whd in ⊢ (%→?); #Htd lapply (proj2 ?? Htd … Htc) -Htd #Htd
+ * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?) [ #x #memx @(no_grids_in_table … Htable) @memb_reverse @memx] -Hte #Hte
+ * #tf * whd in ⊢ (%→?); #Htf lapply (proj2 ?? Htf … Hte) -Htf #Htf
* #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?) [ #x #Hx @bit_or_null_not_grid @Hbitnullcc // ] -Htg #Htg
- whd in ⊢ (%→?); #Houtc lapply (Houtc … Htg) -Houtc #Houtc
+ whd in ⊢ (%→?); #Houtc lapply (proj2 ?? Houtc … Htg) -Houtc #Houtc
% % [% | @Houtc ]
qed.
^
*)
definition mtl_aux ≝
- seq ? (swap STape 〈grid,false〉)
- (seq ? (move_r …) (seq ? (move_r …) (seq ? (move_char_c STape 〈grid,false〉) (move_l …)))).
+ swap_r STape 〈grid,false〉 · move_r … · move_r … ·
+ move_char_r STape 〈grid,false〉 · move_l ….
definition R_mtl_aux ≝ λt1,t2.
∀l1,l2,l3,r. t1 = midtape STape l1 r (〈grid,false〉::l2@〈grid,false〉::l3) → no_grids l2 →
t2 = midtape STape (reverse ? l2@〈grid,false〉::l1) r (〈grid,false〉::l3).
lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux.
#intape
-cases (sem_seq … (sem_swap STape 〈grid,false〉) (sem_seq … (sem_move_r …)
- (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_c STape 〈grid,false〉)
+cases (sem_seq … (sem_swap_r STape 〈grid,false〉) (sem_seq … (sem_move_r …)
+ (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_r STape 〈grid,false〉)
(sem_move_l …)))) intape)
#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
#l1 #l2 #l3 #r #Hintape #Hl2
-cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
-* #tb * whd in ⊢(%→?); #Htb lapply (Htb … Hta) -Htb -Hta whd in ⊢ (???%→?); #Htb
-* #tc * whd in ⊢(%→?); #Htc lapply (Htc … Htb) -Htc -Htb cases l2 in Hl2;
+cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (proj2 ?? Hta … Hintape) -Hta #Hta
+* #tb * whd in ⊢(%→?); #Htb lapply (proj2 ?? Htb … Hta) -Htb -Hta whd in ⊢ (???%→?); #Htb
+* #tc * whd in ⊢(%→?); #Htc lapply (proj2 ?? Htc … Htb) -Htc -Htb cases l2 in Hl2;
[ #_ #Htc * #td * whd in ⊢(%→?); #Htd lapply (Htd … Htc) -Htd >Htc -Htc * #Htd #_
- whd in ⊢ (%→?); #Houtc lapply (Htd (refl ??)) -Htd @Houtc
+ whd in ⊢ (%→?); #Houtc lapply (Htd (refl ??)) -Htd @(proj2 ?? Houtc)
| #c0 #l0 #Hnogrids #Htc *
#td * whd in ⊢(%→?); #Htd lapply (Htd … Htc) -Htd -Htc * #_ #Htd
lapply (Htd … (refl ??) ??)
| @Hmemb ]
| % #Hc0 lapply (Hnogrids c0 ?)
[ @memb_hd | >Hc0 normalize #Hfalse destruct (Hfalse) ]
- | #Htd whd in ⊢(%→?); >Htd #Houtc lapply (Houtc … (refl ??)) -Houtc #Houtc
+ | #Htd whd in ⊢(%→?); >Htd #Houtc lapply (proj2 ?? Houtc … (refl ??)) -Houtc #Houtc
>reverse_cons >associative_append @Houtc
]]
qed.
cases (sem_seq … (sem_move_l …) (sem_adv_to_mark_l … (λc:STape.is_grid (\fst c))) intape)
#k * #outc * #Hloop #HR %{k} %{outc} % [@Hloop] -Hloop
#ls1 #ls2 #rs #Hnogrids #Hintape cases HR -HR
-#ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta
+#ta * whd in ⊢ (%→?); #Hta lapply (proj2 ?? Hta … Hintape) -Hta
cases ls1 in Hnogrids;
-[ #_ #Hta whd in ⊢ (%→?); #Houtc cases (Houtc … Hta) -Houtc
- [ * #_ >Hta #Houtc @Houtc
- | * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
-| #c0 #l0 #Hnogrids #Hta whd in ⊢ (%→?); #Houtc cases (Houtc … Hta) -Houtc
- [ * #Hc0 lapply (Hnogrids c0 (memb_hd …)) >Hc0 #Hfalse destruct (Hfalse)
- | * #_ #Htb >reverse_cons >associative_append @Htb //
- #x #Hx @Hnogrids @memb_cons //
+[ #_ #Hta whd in ⊢ (%→?); #Houtc cases (proj2 ?? Houtc … Hta) -Houtc
+ #Houtc #_ >Houtc [@Hta | %]
+| #c0 #l0 #Hnogrids #Hta whd in ⊢ (%→?); #Houtc cases (proj2 ?? Houtc … Hta) -Houtc
+ #_ #Houtc cases (Houtc ?)
+ [#Houtc #_ >(Houtc … (refl …)(refl …))
+ [>reverse_cons >associative_append %
+ | #x #Hx @Hnogrids @memb_cons //
+ ]
+ |@Hnogrids @memb_hd
]
]
qed.
definition move_tape_l : TM STape ≝
- seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
- (seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
- (seq ? (move_l …)
- (seq ? init_cell
- (seq ? mtl_aux
- (seq ? (swap_r STape 〈grid,false〉)
- (seq ? mtl_aux
- (seq ? (swap STape 〈grid,false〉)
- (seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
- (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c)))))))))))).
+ (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))) ·
+ (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))) ·
+ move_l … · init_cell · mtl_aux · swap_l STape 〈grid,false〉 ·
+ mtl_aux ·swap_r STape 〈grid,false〉 ·
+ (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))) ·
+ (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))).
(* seq ? (move_r …) (seq ? init_cell (seq ? (move_l …)
(seq ? (swap STape 〈grid,false〉)
- (seq ? mtr_aux (seq ? (move_l …) mtr_aux))))). *)
+ (seq ? move_after_left_bar (seq ? (move_l …) move_after_left_bar))))). *)
+
+axiom daemon: ∀P:Prop.P.
definition R_move_tape_l ≝ λt1,t2.
∀rs,n,table,c0,bc0,curconfig,ls0.
(sem_seq … (sem_move_l …)
(sem_seq … sem_init_cell
(sem_seq … sem_mtl_aux
- (sem_seq … (sem_swap_r STape 〈grid,false〉)
+ (sem_seq … (sem_swap_l STape 〈grid,false〉)
(sem_seq … sem_mtl_aux
- (sem_seq … (sem_swap STape 〈grid,false〉)
+ (sem_seq … (sem_swap_r STape 〈grid,false〉)
(sem_seq … sem_ml_atml sem_ml_atml)))))))) tapein)
#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
#rs #n #table #c0 #bc0 #curconfig #ls0 #Hbitnullc0 #Hbitnullcc #Htable #Hls0 #Htapein
cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Htapein)
-[ @daemon (* by no_grids_in_table, manca un lemma sulla reverse *) ]
+[#x #memx @(no_grids_in_table … Htable) @memb_reverse @memx]
-Hta #Hta * #tb * whd in ⊢ (%→?); #Htb lapply (Htb (〈c0,bc0〉::curconfig) … Hta)
[ @daemon ] -Hta -Htb #Htb
-* #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htb -Htc #Htc
+* #tc * whd in ⊢ (%→?); #Htc lapply (proj2 ?? Htc … Htb) -Htb -Htc #Htc
* #td * whd in ⊢ (%→?); *
[ * #c1 * generalize in match Htc; generalize in match Htapein; -Htapein -Htc
cases ls0 in Hls0;
#Hl1 whd in Hl1:(??%?); #Htd
* #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?)
[ (* memb_reverse *) @daemon ] -Hte -Htd >reverse_reverse #Hte
- * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf -Hte #Htf
+ * #tf * whd in ⊢ (%→?); #Htf lapply (proj2 ?? Htf … Hte) -Htf -Hte #Htf
* #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?)
[ @(no_grids_in_table … Htable) ] -Htg -Htf >reverse_reverse #Htg
- * #th * whd in ⊢ (%→?); #Hth lapply (Hth … Htg) -Hth -Htg #Hth
+ * #th * whd in ⊢ (%→?); #Hth lapply (proj2 ?? Hth … Htg) -Hth -Htg #Hth
* #ti * whd in ⊢ (%→?); #Hti lapply (Hti … Hth)
[ (* memb_reverse *) @daemon ] -Hti -Hth #Hti
whd in ⊢ (%→?); #Houtc lapply (Houtc (l1::curconfig) … Hti)
#Htapein #Htc change with (leftof ???) in Htc:(???%); >Htc #_ #Htd
* #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?)
[ (*memb_reverse*) @daemon ] -Hte -Htd >reverse_reverse #Hte
- * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf -Hte #Htf
+ * #tf * whd in ⊢ (%→?); #Htf lapply (proj2 ?? Htf … Hte) -Htf -Hte #Htf
* #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?)
[ @(no_grids_in_table … Htable) ] -Htg -Htf >reverse_reverse #Htg
- * #th * whd in ⊢ (%→?); #Hth lapply (Hth … Htg) -Hth -Htg #Hth
+ * #th * whd in ⊢ (%→?); #Hth lapply (proj2 ?? Hth … Htg) -Hth -Htg #Hth
* #ti * whd in ⊢ (%→?); #Hti lapply (Hti … Hth)
[ (*memb_reverse*) @daemon ] -Hti -Hth #Hti
whd in ⊢ (%→?); #Houtc lapply (Houtc (〈null,false〉::curconfig) … Hti)
qed.
(*definition mtl_aux ≝
- seq ? (move_r …) (seq ? (move_char_c STape 〈grid,false〉) (move_l …)).
+ seq ? (move_r …) (seq ? (move_char_r STape 〈grid,false〉) (move_l …)).
definition R_mtl_aux ≝ λt1,t2.
∀l1,l2,l3,r. t1 = midtape STape l1 r (l2@〈grid,false〉::l3) → no_grids l2 →
t2 = midtape STape (reverse ? l2@l1) r (〈grid,false〉::l3).
lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux.
#intape
-cases (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_c STape 〈grid,false〉) (sem_move_l …)) intape)
+cases (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_r STape 〈grid,false〉) (sem_move_l …)) intape)
#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
#l1 #l2 #l3 #r #Hintape #Hl2
cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
[ bit x ⇒ match x with [ true ⇒ R | false ⇒ L ]
| _ ⇒ N ].
-definition R_uni_step ≝ λt1,t2.
- ∀n,table,c,c1,ls,rs,curs,curc,news,newc,mv.
- table_TM n table →
- match_in_table n (〈c,false〉::curs) 〈curc,false〉
- (〈c1,false〉::news) 〈newc,false〉 〈mv,false〉 table →
- t1 = midtape STape (〈grid,false〉::ls) 〈c,false〉
- (curs@〈curc,false〉::〈grid,false〉::table@〈grid,false〉::rs) →
- ∀t1',ls1,rs1.t1' = lift_tape ls 〈curc,false〉 rs →
- (t2 = midtape STape (〈grid,false〉::ls1) 〈c1,false〉
- (news@〈newc,false〉::〈grid,false〉::table@〈grid,false〉::rs1) ∧
- lift_tape ls1 〈newc,false〉 rs1 =
- tape_move STape t1' (Some ? 〈〈newc,false〉,move_of_unialpha mv〉)).
-
definition no_nulls ≝
λl:list STape.∀x.memb ? x l = true → is_null (\fst x) = false.
] ] ]
| #x #Hx @Hbits @memb_append_l1 @Hx ]
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
-cases (HR1 intape) -HR1 #k * #outc * #Hloop #HR1
-@(ex_intro ?? k) @(ex_intro ?? outc) % /2/
-qed.
lemma sem_move_tape_l_abstract : Realize … move_tape_l R_move_tape_l_abstract.
@(Realize_to_Realize … mtl_concrete_to_abstract) //
ifTM ? (test_char ? (λc:STape.c == 〈bit false,false〉))
(* spostamento a sinistra: verificare se per caso non conviene spostarsi
sulla prima grid invece dell'ultima *)
- (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c))) move_tape_l)
+ (adv_to_mark_r ? (λc:STape.is_grid (\fst c)) · move_tape_l)
(ifTM ? (test_char ? (λc:STape.c == 〈bit true,false〉))
- (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c))) move_tape_r)
- (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
- (seq ? (move_l …) (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))))
+ (adv_to_mark_r ? (λc:STape.is_grid (\fst c)) · move_tape_r)
+ (adv_to_mark_l ? (λc:STape.is_grid (\fst c)) ·
+ move_l … · adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
tc_true) tc_true.
definition R_move_tape ≝ λt1,t2.
((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
cases (sem_if ? (test_char ??) … tc_true (sem_test_char ? (λc:STape.c == 〈bit false,false〉))
#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 〈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 ??) ?)
+[* #ta * whd in ⊢ (%→?); * * #c * >Hintape normalize in ⊢ (%→?);
+ #Hdes destruct (Hdes) #eqmv
+ cut (mv = bit false) [lapply (\P eqmv) #Hdes destruct (Hdes) %] -eqmv #eqmv #Hta
+ * #tb * whd in ⊢ (%→?); #Htb cases (proj2 ?? Htb … Hta) -Htb -Hta
+ [ * >eqmv normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
+ * * #_ #Htb #_ lapply (Htb ??? (refl ??) (refl …) ?)
[ @daemon ] -Htb >append_cons <associative_append #Htb
whd in ⊢ (%→?); #Houtc lapply (Houtc … Htb … Ht1') //
- [ >reverse_append >reverse_append >reverse_reverse @Htable
- | /2/
- ||]
+ [ >reverse_append >reverse_append >reverse_reverse @Htable |@Hmvcurc >eqmv % ||]
-Houtc -Htb * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal
@(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) %
[ //
>associative_append >associative_append %
| % % % // ]
]
-| * #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 〈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 <associative_append #Htc
- whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc … Ht1') //
- [ >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) %
- [ //
- | %
- [ >Houtc >reverse_append >reverse_append >reverse_reverse
- >associative_append >associative_append %
- | % %2 % // ]
- ]
- | * #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 … 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 *
- [ * cases Htape * * #_ #_ #Hcurc #_
- >(bit_or_null_not_grid … Hcurc) #Hfalse destruct (Hfalse) ]
- * #_ #Houtc lapply (Houtc … (refl ??) (refl ??) ?) [@daemon] -Houtc #Houtc
+| * #ta * whd in ⊢ (%→?); * >Hintape #Hcneq #Hta
+ cut (mv ≠ bit false)
+ [lapply (\Pf (Hcneq … (refl …))) @not_to_not #Heq >Heq % ] -Hcneq #Hcneq
+ *
+ [* #tb * * * #ca >Hta -Hta * normalize in ⊢ (%→?); #Hdes destruct (Hdes) #eqmv
+ cut (mv = bit true) [lapply (\P eqmv) #Hdes destruct (Hdes) %] -eqmv #eqmv
+ #Htb * #tc * whd in ⊢ (%→?); #Htc cases (proj2 ?? Htc … Htb) -Htc
+ [ * >(bit_or_null_not_grid … Hmv) #Hfalse destruct (Hfalse) ]
+ * * #_ #Htc lapply (Htc ???(refl ??) (refl ??) ?)
+ [ @daemon ] -Htc >append_cons <associative_append #Htc
+ #_ whd in ⊢ (%→?); #Houtc lapply (Houtc ? n … Htc … Ht1') //
+ [ >reverse_append >reverse_append >reverse_reverse @Htable
+ | @Hmvcurc @daemon]
+ -Houtc -Htc * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal
+ @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) %
+ [ //
+ | %
+ [ >Houtc >reverse_append >reverse_append >reverse_reverse
+ >associative_append >associative_append %
+ | % %2 % //
+ ]
+ ]
+ |* #tb * whd in ⊢ (%→?); * >Hta #Hcneq' #Htb
+ cut (mv ≠ bit true)
+ [lapply (\Pf (Hcneq' … (refl …))) @not_to_not #Heq >Heq % ] -Hcneq' #Hcneq'
+ * #tc * whd in ⊢ (%→?); #Htc cases (proj2 ?? Htc … Htb) -Htc
+ #_ #Htc cases (Htc (bit_or_null_not_grid … Hmv)) -Htc #Htc #_
+ lapply (Htc … (refl ??) (refl ??) ?) [@daemon] -Htc #Htc
+ * #td * whd in ⊢ (%→?); #Htd lapply (proj2 ?? Htd … Htc) -Htd -Htc
+ whd in ⊢ (???%→?); #Htd whd in ⊢ (%→?); #Houtc cases (proj2 ?? Houtc … Htd)
+ -Houtc #_ #Houtc cases (Houtc ?)
+ [2: cases Htape * * #_ #_ #Hcurc #_ >(bit_or_null_not_grid … Hcurc) %]
+ #Houtc #_ lapply (Houtc … (refl ??) (refl ??) ?) [@daemon] -Houtc #Houtc
@(ex_intro ?? ls) @(ex_intro ?? rs) @(ex_intro ?? curc) %
[ //
| %
]
]
]
-qed.
\ No newline at end of file
+qed.
+
projects / helm.git / blobdiff