- | generalize in match Hlen; >Hbs >Hb0s
- normalize #Hlen destruct (Hlen) @e0
- | #c0 #Hc0 @Hbs1 >Hbs @memb_cons //
- | #c0 #Hc0 @Hb0s1 >Hb0s @memb_cons //
- | #c0 #Hc0 @Hbs2 >Hbs @memb_cons //
- | #c0 #Hc0 @Hb0s2 >Hb0s @memb_cons //
- | #c0 #Hc0 cases (memb_append … Hc0)
- [ @Hl1 | #Hc0' >(memb_single … Hc0') % ]
- | %
- | >associative_append >associative_append % ]
- | * #Hneq #Htapeb %2
- @(ex_intro … []) @(ex_intro … b) @(ex_intro … b0)
- @(ex_intro … bs) @(ex_intro … b0s) %
- [ % // % // @sym_not_eq //
- | >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
- >reverse_append in Htapeb; >reverse_cons
- >associative_append >associative_append
- #Htapeb <Htapeb
- cases (IH … Htapeb) -Htapeb -IH * #_ #IH #_ @(IH ? (refl ??))
- ]
- | #c1 #Hc1 cases (memb_append … Hc1) #Hyp
- [ @Hbs2 >Hbs @memb_cons @Hyp
- | cases (orb_true_l … Hyp)
- [ #Hyp2 >(\P Hyp2) %
- | @Hl1
- ]
- ]
- ]
-]]]]]
-qed.
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+]
+qed.
+
+lemma WF_cst_niltape:
+ WF ? (inv ? R_comp_step_true) (niltape (FinProd FSUnialpha FinBool)).
+@wf #t1 whd in ⊢ (%→?); * #ls * #c * #rs * #H destruct
+qed.
+
+lemma WF_cst_rightof:
+ ∀a,ls. WF ? (inv ? R_comp_step_true) (rightof (FinProd FSUnialpha FinBool) a ls).
+#a #ls @wf #t1 whd in ⊢ (%→?); * #ls * #c * #rs * #H destruct
+qed.
+
+lemma WF_cst_leftof:
+ ∀a,ls. WF ? (inv ? R_comp_step_true) (leftof (FinProd FSUnialpha FinBool) a ls).
+#a #ls @wf #t1 whd in ⊢ (%→?); * #ls * #c * #rs * #H destruct
+qed.
+
+lemma WF_cst_midtape_false:
+ ∀ls,c,rs. WF ? (inv ? R_comp_step_true)
+ (midtape (FinProd … FSUnialpha FinBool) ls 〈c,false〉 rs).
+#ls #c #rs @wf #t1 whd in ⊢ (%→?); * #ls' * #c' * #rs' * #H destruct
+qed.
+
+(* da spostare *)
+lemma not_nil_to_exists:∀A.∀l: list A. l ≠ [ ] →
+ ∃a,tl. a::tl = l.
+ #A * [* #H @False_ind @H // | #a #tl #_ @(ex_intro … a) @(ex_intro … tl) //]
+ qed.
+
+lemma terminate_compare:
+ ∀t. Terminate ? compare t.
+#t @(terminate_while … sem_comp_step) [%]
+cases t // #ls * #c * //
+#rs
+(* we cannot proceed by structural induction on the right tape,
+ since compare moves the marks! *)
+cut (∃len. |rs| = len) [/2/]
+* #len lapply rs lapply c lapply ls -ls -c -rs elim len
+ [#ls #c #rs #Hlen >(lenght_to_nil … Hlen) @wf #t1 whd in ⊢ (%→?); * #ls0 * #c0 * #rs0 * #Hmid destruct (Hmid)
+ * * #H1 #H2 #_ cases (true_or_false (bit_or_null c0)) #Hc0
+ [>(H2 Hc0 … (refl …)) // #x whd in ⊢ ((??%?)→?); #Hdes destruct
+ |>(H1 Hc0) //
+ ]
+ |-len #len #Hind #ls #c #rs #Hlen @wf #t1 whd in ⊢ (%→?); * #ls0 * #c0 * #rs0 * #Hmid destruct (Hmid)
+ * * #H1 #H2 #H3 cases (true_or_false (bit_or_null c0)) #Hc0
+ [-H1 cases (split_on_spec_ex ? rs0 (is_marked ?)) #rs1 * #rs2
+ cases rs2
+ [(* no marks in right tape *)
+ * * >append_nil #H >H -H #Hmarks #_
+ cases (not_nil_to_exists ? (reverse (FSUnialpha×bool) (〈c0,true〉::rs0)) ?)
+ [2: % >reverse_cons #H cases (nil_to_nil … H) #_ #H1 destruct]
+ #a0 * #tl #H4 >(H2 Hc0 Hmarks a0 tl H4) //
+ |(* the first marked element is a0 *)
+ * #a0 #a0b #rs3 * * #H4 #H5 #H6 lapply (H3 ? a0 rs3 … Hc0 H5 ?)
+ [<H4 @eq_f @eq_f2 [@eq_f @(H6 〈a0,a0b〉 … (refl …)) | %]
+ |cases (true_or_false (c0==a0)) #eqc0a0 (* comparing a0 with c0 *)
+ [* * (* we check if we have elements at the right of a0 *)
+ lapply H4 -H4 cases rs3
+ [#_ #Ht1 #_ #_ >(Ht1 (\P eqc0a0) (refl …)) //
+ |(* a1 will be marked *)
+ cases (not_nil_to_exists ? (rs1@[〈a0,false〉]) ?)
+ [2: % #H cases (nil_to_nil … H) #_ #H1 destruct]
+ * #a2 #a2b * #tl2 #H7 * #a1 #a1b #rs4 #H4 #_ #Ht1 #_
+ cut (a2b =false)
+ [lapply (memb_hd ? 〈a2,a2b〉 tl2) >H7 #mema2
+ cases (memb_append … mema2)
+ [@H5 |#H lapply(memb_single … H) #H2 destruct %]
+ ]
+ #Ha2b >Ha2b in H7; #H7
+ >(Ht1 (\P eqc0a0) … H7 (refl …)) @Hind -Hind -Ht1 -Ha2b -H2 -H3 -H5 -H6
+ <H4 in Hlen; >length_append normalize <plus_n_Sm #Hlen1
+ >length_append normalize <(injective_S … Hlen1) @eq_f2 //
+ cut (|〈a2,false〉::tl2|=|rs1@[〈a0,false〉]|) [>H7 %]
+ >length_append normalize <plus_n_Sm <plus_n_O //
+ ]
+ |(* c0 =/= a0 *) * * #_ #_ #Ht1 >(Ht1 (\Pf eqc0a0)) //
+ ]
+ ]
+ ]
+ |>(H1 Hc0) //
+ ]
+qed.