+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.
+
+lemma sem_compare : Realize ? compare R_compare.
+/2/ qed.
+
+(* new *)
+definition R_compare_new :=
+ λt1,t2.
+ ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
+ (∀c'.bit_or_null c' = false → c = 〈c',true〉 → t2 = midtape ? ls 〈c',false〉 rs) ∧
+ (∀c'. c = 〈c',false〉 → t2 = t1) ∧
+(* forse manca il caso no marks in rs *)
+ ∀b,b0,bs,b0s,comma,l1,l2.
+ |bs| = |b0s| →
+ (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → bit_or_null (\fst c) = true) →
+ (∀c.memb ? c bs = true → is_marked ? c = false) →
+ (∀c.memb ? c b0s = true → is_marked ? c = false) →
+ (∀c.memb ? c l1 = true → is_marked ? c = false) →
+ c = 〈b,true〉 → bit_or_null b = true →
+ rs = bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2 →
+ (〈b,true〉::bs = 〈b0,true〉::b0s ∧
+ t2 = midtape ? (reverse ? bs@〈b,false〉::ls)
+ 〈grid,false〉 (l1@〈b0,false〉::b0s@〈comma,true〉::l2)) ∨
+ (∃la,c',d',lb,lc.c' ≠ d' ∧
+ 〈b,false〉::bs = la@〈c',false〉::lb ∧
+ 〈b0,false〉::b0s = la@〈d',false〉::lc ∧
+ t2 = midtape (FinProd … FSUnialpha FinBool) (reverse ? la@
+ reverse ? l1@
+ 〈grid,false〉::
+ reverse ? lb@
+ 〈c',true〉::
+ reverse ? la@ls)
+ 〈d',false〉 (lc@〈comma,false〉::l2)).
+
+lemma wsem_compare_new : WRealize ? compare R_compare_new.