1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "turing/multi_universal/compare.ma".
16 include "turing/multi_universal/par_test.ma".
19 definition Rtc_multi_true ≝
20 λalpha,test,n,i.λt1,t2:Vector ? (S n).
21 (∃c. current alpha (nth i ? t1 (niltape ?)) = Some ? c ∧ test c = true) ∧ t2 = t1.
23 definition Rtc_multi_false ≝
24 λalpha,test,n,i.λt1,t2:Vector ? (S n).
25 (∀c. current alpha (nth i ? t1 (niltape ?)) = Some ? c → test c = false) ∧ t2 = t1.
27 lemma sem_test_char_multi :
28 ∀alpha,test,n,i.i ≤ n →
29 inject_TM ? (test_char ? test) n i ⊨
30 [ tc_true : Rtc_multi_true alpha test n i, Rtc_multi_false alpha test n i ].
31 #alpha #test #n #i #Hin #int
32 cases (acc_sem_inject … Hin (sem_test_char alpha test) int)
33 #k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
35 | #Hqtrue lapply (Htrue Hqtrue) * * * #c *
36 #Hcur #Htestc #Hnth_i #Hnth_j %
38 | @(eq_vec … (niltape ?)) #i0 #Hi0
39 cases (decidable_eq_nat i0 i) #Hi0i
41 | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
42 | #Hqfalse lapply (Hfalse Hqfalse) * * #Htestc #Hnth_i #Hnth_j %
44 | @(eq_vec … (niltape ?)) #i0 #Hi0
45 cases (decidable_eq_nat i0 i) #Hi0i
47 | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
50 definition Rm_test_null_true ≝
51 λalpha,n,i.λt1,t2:Vector ? (S n).
52 current alpha (nth i ? t1 (niltape ?)) ≠ None ? ∧ t2 = t1.
54 definition Rm_test_null_false ≝
55 λalpha,n,i.λt1,t2:Vector ? (S n).
56 current alpha (nth i ? t1 (niltape ?)) = None ? ∧ t2 = t1.
58 lemma sem_test_null_multi : ∀alpha,n,i.i ≤ n →
59 inject_TM ? (test_null ?) n i ⊨
60 [ tc_true : Rm_test_null_true alpha n i, Rm_test_null_false alpha n i ].
61 #alpha #n #i #Hin #int
62 cases (acc_sem_inject … Hin (sem_test_null alpha) int)
63 #k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
65 | #Hqtrue lapply (Htrue Hqtrue) * * #Hcur #Hnth_i #Hnth_j % //
66 @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i
67 [ >Hi0i @sym_eq @Hnth_i | @sym_eq @Hnth_j @sym_not_eq // ] ]
68 | #Hqfalse lapply (Hfalse Hqfalse) * * #Hcur #Hnth_i #Hnth_j %
70 | @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) //
71 #Hi0i @sym_eq @Hnth_j @sym_not_eq // ] ]
74 lemma comp_list: ∀S:DeqSet. ∀l1,l2:list S.∀is_endc. ∃l,tl1,tl2.
75 l1 = l@tl1 ∧ l2 = l@tl2 ∧ (∀c.c ∈ l = true → is_endc c = false) ∧
76 ∀a,tla. tl1 = a::tla →
77 is_endc a = true ∨ (is_endc a = false ∧∀b,tlb.tl2 = b::tlb → a≠b).
78 #S #l1 #l2 #is_endc elim l1 in l2;
79 [ #l2 %{[ ]} %{[ ]} %{l2} normalize %
80 [ % [ % // | #c #H destruct (H) ] | #a #tla #H destruct (H) ]
81 | #x #l3 #IH cases (true_or_false (is_endc x)) #Hendcx
82 [ #l %{[ ]} %{(x::l3)} %{l} normalize
83 % [ % [ % // | #c #H destruct (H) ] | #a #tla #H destruct (H) >Hendcx % % ]
85 [ %{[ ]} %{(x::l3)} %{[ ]} normalize %
86 [ % [ % // | #c #H destruct (H) ]
87 | #a #tla #H destruct (H) cases (is_endc a)
88 [ % % | %2 % // #b #tlb #H destruct (H) ]
90 | #y #l4 cases (true_or_false (x==y)) #Hxy
91 [ lapply (\P Hxy) -Hxy #Hxy destruct (Hxy)
92 cases (IH l4) -IH #l * #tl1 * #tl2 * * * #Hl3 #Hl4 #Hl #IH
93 %{(y::l)} %{tl1} %{tl2} normalize
95 | #c cases (true_or_false (c==y)) #Hcy >Hcy normalize
99 | #a #tla #Htl1 @(IH … Htl1) ]
100 | %{[ ]} %{(x::l3)} %{(y::l4)} normalize %
101 [ % [ % // | #c #H destruct (H) ]
102 | #a #tla #H destruct (H) cases (is_endc a)
103 [ % % | %2 % // #b #tlb #H destruct (H) @(\Pf Hxy) ]
111 definition match_test ≝ λsrc,dst.λsig:DeqSet.λn,is_endc.λv:Vector ? n.
112 match (nth src (option sig) v (None ?)) with
114 | Some x ⇒ notb ((is_endc x) ∨ (nth dst (DeqOption sig) v (None ?) == None ?))].
116 definition match_step ≝ λsrc,dst,sig,n,is_startc,is_endc.
117 compare src dst sig n is_endc ·
118 (ifTM ?? (partest sig n (match_test src dst sig ? is_endc))
120 (parmove src dst sig n L is_startc · (inject_TM ? (move_r ?) n dst)))
124 definition R_match_step_false ≝
125 λsrc,dst,sig,n,is_endc.λint,outt: Vector (tape sig) (S n).
127 nth src ? int (niltape ?) = midtape sig ls x (xs@end::rs) →
128 (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) → is_endc end = true →
129 ((current sig (nth dst (tape sig) int (niltape sig)) = None ?) ∧ outt = int) ∨
130 (∃ls0,rs0,xs0. nth dst ? int (niltape ?) = midtape sig ls0 x rs0 ∧
132 current sig (nth dst (tape sig) outt (niltape sig)) = None ?) ∨
134 nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) ∧
138 (change_vec ?? int (midtape sig (reverse ? xs@x::ls) end rs) src)
139 (midtape sig (reverse ? xs@x::ls0) c rsj) dst).
141 definition R_match_step_true ≝
142 λsrc,dst,sig,n,is_startc,is_endc.λint,outt: Vector (tape sig) (S n).
143 ∀s.current sig (nth src (tape sig) int (niltape sig)) = Some ? s →
144 current sig (nth dst (tape sig) int (niltape sig)) ≠ None ? ∧
145 (is_startc s = true →
146 (∀c.c ∈ right ? (nth src (tape sig) int (niltape sig)) = true → is_startc c = false) →
147 (∀s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 → s ≠ s1 →
148 outt = change_vec ?? int
149 (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈s1,R〉)) dst ∧ is_endc s = false) ∧
150 (∀ls,x,xs,ci,rs,ls0,rs0.
151 nth src ? int (niltape ?) = midtape sig ls x (xs@ci::rs) →
152 nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) →
153 (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) →
154 is_endc ci = false ∧ rs0 ≠ [] ∧
155 ∀cj,rs1.rs0 = cj::rs1 →
157 (outt = change_vec ?? int
158 (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈x,R〉)) dst ∧ is_endc ci = false))).
160 lemma sem_match_step :
161 ∀src,dst,sig,n,is_startc,is_endc.src ≠ dst → src < S n → dst < S n →
162 match_step src dst sig n is_startc is_endc ⊨
163 [ inr ?? (inr ?? (inl … (inr ?? start_nop))) :
164 R_match_step_true src dst sig n is_startc is_endc,
165 R_match_step_false src dst sig n is_endc ].
166 #src #dst #sig #n #is_startc #is_endc #Hneq #Hsrc #Hdst
167 @(acc_sem_seq_app sig n … (sem_compare src dst sig n is_endc Hneq Hsrc Hdst)
168 (acc_sem_if ? n … (sem_partest sig n (match_test src dst sig ? is_endc))
170 (sem_parmoveL ???? is_startc Hneq Hsrc Hdst)
171 (sem_inject … dst (le_S_S_to_le … Hdst) (sem_move_r ? )))
173 [#ta #tb #tc * #Hcomp1 #Hcomp2 * #td * * #Htest #Htd >Htd -Htd
174 * #te * #Hte #Htb whd
176 [ lapply (refl ? (current ? (nth dst ? ta (niltape ?))))
177 cases (current ? (nth dst ? ta (niltape ?))) in ⊢ (???%→%);
178 [| #c #_ % #Hfalse destruct (Hfalse) ]
179 #Hcurta_dst >Hcomp1 in Htest; [| %2 %2 //]
180 whd in ⊢ (??%?→?); change with (current ? (niltape ?)) in match (None ?);
181 <nth_vec_map >Hcurta_src whd in ⊢ (??%?→?); <nth_vec_map
182 >Hcurta_dst cases (is_endc s) normalize in ⊢ (%→?); #H destruct (H)
183 | #Hstart #Hnotstart %
184 [ #s1 #Hcurta_dst #Hneqss1 -Hcomp2
186 [@Hcomp1 %2 %1 %1 >Hcurta_src >Hcurta_dst @(not_to_not … Hneqss1) #H destruct (H) //]
187 #H destruct (H) -Hcomp1 cases Hte #_ -Hte #Hte
188 cut (te = ta) [@Hte %1 %1 %{s} % //] -Hte #H destruct (H) %
189 [cases Htb * #_ #Hmove #Hmove1 @(eq_vec … (niltape … ))
190 #i #Hi cases (decidable_eq_nat i dst) #Hidst
191 [ >Hidst >nth_change_vec // cases (current_to_midtape … Hcurta_dst)
192 #ls * #rs #Hta_mid >(Hmove … Hta_mid) >Hta_mid cases rs //
193 | >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @Hmove1 @sym_not_eq // ]
194 | whd in Htest:(??%?); >(nth_vec_map ?? (current sig)) in Hcurta_src; #Hcurta_src
195 >Hcurta_src in Htest; whd in ⊢ (??%?→?);
196 cases (is_endc s) // whd in ⊢ (??%?→?); #H @sym_eq //
198 |#ls #x #xs #ci #rs #ls0 #rs00 #Htasrc_mid #Htadst_mid #Hnotendc
199 cases (Hcomp2 … Htasrc_mid Htadst_mid Hnotendc)
200 [ * #Hrs00 #Htc >Htc in Htest; whd in ⊢ (??%?→?);
201 <(nth_vec_map ?? (current sig) ??? (niltape ?))
202 >change_vec_commute // >nth_change_vec // whd in ⊢ (??%?→?);
204 [ whd in ⊢ (??%?→?); #H destruct (H)
205 | <(nth_vec_map ?? (current sig) ??? (niltape ?))
206 >change_vec_commute [| @sym_not_eq // ] >nth_change_vec //
207 >(?:current ? (mk_tape ?? (None ?) ?) = None ?)
208 [ whd in ⊢ (??%?→?); #H destruct (H)
209 | cases (reverse sig xs@x::ls0) normalize // ] ] ]
210 * #cj' * #rs0' * #Hcjrs0 destruct (Hcjrs0) -Hcomp2 #Hcomp2 % [ %
211 [ cases (true_or_false (is_endc ci)) //
212 #Hendci >(Hcomp2 (or_introl … Hendci)) in Htest;
213 whd in ⊢ (??%?→?); <(nth_vec_map ?? (current sig) ??? (niltape ?))
214 >change_vec_commute // >nth_change_vec // whd in ⊢ (??%?→?);
216 | % #H destruct (H) ] ] #cj #rs1 #H destruct (H) #Hcicj
217 lapply (Hcomp2 (or_intror ?? Hcicj)) -Hcomp2 #Htc %
218 [ cases Hte -Hte #Hte #_ whd in Hte;
219 >Htasrc_mid in Hcurta_src; whd in ⊢ (??%?→?); #H destruct (H)
220 lapply (Hte ls ci (reverse ? xs) rs s ??? ls0 cj (reverse ? xs) s rs1 (refl ??) ?) //
221 [ >Htc >nth_change_vec //
222 | #c0 #Hc0 @(Hnotstart c0) >Htasrc_mid cases (orb_true_l … Hc0) -Hc0 #Hc0
223 [@memb_append_l2 >(\P Hc0) @memb_hd
224 |@memb_append_l1 <(reverse_reverse …xs) @memb_reverse //
226 | >Htc >change_vec_commute // >nth_change_vec // ] -Hte
227 >Htc >change_vec_commute // >change_vec_change_vec
228 >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec #Hte
229 >Hte in Htb; * * #_ >reverse_reverse #Htbdst1 #Htbdst2 -Hte @(eq_vec … (niltape ?))
230 #i #Hi cases (decidable_eq_nat i dst) #Hidst
231 [ >Hidst >nth_change_vec // >(Htbdst1 ls0 s (xs@cj::rs1))
232 [| >nth_change_vec // ]
233 >Htadst_mid cases xs //
234 | >nth_change_vec_neq [|@sym_not_eq // ]
235 <Htbdst2 [| @sym_not_eq // ] >nth_change_vec_neq [| @sym_not_eq // ]
236 <Htasrc_mid >change_vec_same % ]
237 | >Hcurta_src in Htest; whd in ⊢(??%?→?);
238 >Htc >change_vec_commute //
239 change with (current ? (niltape ?)) in match (None ?);
240 <nth_vec_map >nth_change_vec // whd in ⊢ (??%?→?);
241 cases (is_endc ci) whd in ⊢ (??%?→?); #H destruct (H) %
245 |#intape #outtape #ta * #Hcomp1 #Hcomp2 * #tb * * #Hc #Htb
246 whd in ⊢ (%→?); #Hout >Hout >Htb whd
247 #ls #c_src #xs #end #rs #Hmid_src #Hnotend #Hend
248 lapply (current_to_midtape sig (nth dst ? intape (niltape ?)))
249 cases (current … (nth dst ? intape (niltape ?))) in Hcomp1;
250 [#Hcomp1 #_ %1 % % [% | @Hcomp1 %2 %2 % ]
251 |#c_dst cases (true_or_false (c_src == c_dst)) #Hceq
252 [#_ #Hmid_dst cases (Hmid_dst c_dst (refl …)) -Hmid_dst
253 #ls_dst * #rs_dst #Hmid_dst
254 cases (comp_list … (xs@end::rs) rs_dst is_endc) #xs1 * #rsi * #rsj * * *
255 #Hrs_src #Hrs_dst #Hnotendxs1 #Hneq >Hrs_dst in Hmid_dst; #Hmid_dst
256 cut (∃r1,rs1.rsi = r1::rs1)
257 [cases rsi in Hrs_src;
258 [ >append_nil #H <H in Hnotendxs1; #Hnotendxs1
259 >(Hnotendxs1 end) in Hend; [ #H1 destruct (H1) ]
260 @memb_append_l2 @memb_hd
261 | #r1 #rs1 #_ %{r1} %{rs1} % ] ]
262 * #r1 * #rs1 #Hrs1 >Hrs1 in Hrs_src;
263 #Hrs_src >Hrs_src in Hmid_src; #Hmid_src <(\P Hceq) in Hmid_dst; #Hmid_dst
264 lapply (Hcomp2 ??????? Hmid_src Hmid_dst ?)
265 [ #c0 #Hc0 cases (orb_true_l … Hc0) -Hc0 #Hc0
266 [ >(\P Hc0) @Hnotend @memb_hd | @Hnotendxs1 //] ]
268 [ * #Hrsj >Hrsj #Hta % %2 >Hta >nth_change_vec //
269 %{ls_dst} %{xs1} cut (∃xs0.xs = xs1@xs0)
270 [lapply Hnotendxs1 -Hnotendxs1 lapply Hrs_src lapply xs elim xs1
273 [ whd in ⊢ (??%%→?); #H destruct (H) #Hnotendxs2
274 >Hnotendxs2 in Hend; [ #H destruct (H) |@memb_hd ]
275 | #x2' #xs2' whd in ⊢ (??%%→?); #H destruct (H)
276 #Hnotendxs2 cases (IH xs2' e0 ?)
277 [ #xs0 #Hxs2 %{xs0} @eq_f //
278 |#c #Hc @Hnotendxs2 @memb_cons // ]
281 ] * #xs0 #Hxs0 %{xs0} % [ %
282 [ >Hmid_dst >Hrsj >append_nil %
284 | cases (reverse ? xs1) // ]
285 | * #cj * #rs2 * #Hrsj #Hta lapply (Hta ?)
286 [ cases (Hneq ?? Hrs1) /2/ * #_ #Hr1 %2 @(Hr1 ?? Hrsj) ] -Hta #Hta
287 %2 >Hta in Hc; whd in ⊢ (??%?→?);
288 change with (current ? (niltape ?)) in match (None ?);
289 <nth_vec_map >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
290 whd in ⊢ (??%?→?); #Hc cut (is_endc r1 = true)
291 [ cases (is_endc r1) in Hc; whd in ⊢ (??%?→?); //
292 change with (current ? (niltape ?)) in match (None ?);
293 <nth_vec_map >nth_change_vec // normalize #H destruct (H) ]
294 #Hendr1 cut (xs = xs1)
295 [ lapply Hnotendxs1 lapply Hnotend lapply Hrs_src lapply xs1
296 -Hnotendxs1 -Hnotend -Hrs_src -xs1 elim xs
297 [ * normalize in ⊢ (%→?); //
298 #x2 #xs2 normalize in ⊢ (%→?); #Heq destruct (Heq) #_ #Hnotendxs1
299 lapply (Hnotendxs1 ? (memb_hd …)) >Hend #H destruct (H)
301 [ normalize in ⊢ (%→?); #Heq destruct (Heq) #Hnotendc
302 >Hnotendc in Hendr1; [| @memb_cons @memb_hd ]
303 normalize in ⊢ (%→?); #H destruct (H)
304 | #x3 #xs3 normalize in ⊢ (%→?); #Heq destruct (Heq)
305 #Hnotendc #Hnotendcxs1 @eq_f @IH
306 [ @(cons_injective_r … Heq)
307 | #c0 #Hc0 @Hnotendc cases (orb_true_l … Hc0) -Hc0 #Hc0
309 | @memb_cons @memb_cons // ]
310 | #c #Hc @Hnotendcxs1 @memb_cons // ]
313 | #Hxsxs1 destruct (Hxsxs1) >Hmid_dst %{ls_dst} %{rsj} % //
314 #rsj0 #c >Hrsj #Hrsj0 destruct (Hrsj0)
315 lapply (append_l2_injective … Hrs_src) // #Hrs' destruct (Hrs') %
318 |#Hcomp1 #Hsrc cases (Hsrc ? (refl ??)) -Hsrc #ls0 * #rs0 #Hdst
319 @False_ind lapply (Hcomp1 ?) [%2 %1 %1 >Hmid_src normalize
320 @(not_to_not ??? (\Pf Hceq)) #H destruct //] #Hintape >Hintape in Hc;
321 whd in ⊢(??%?→?); >Hmid_src
322 change with (current ? (niltape ?)) in match (None ?);
323 <nth_vec_map >Hmid_src whd in ⊢ (??%?→?);
324 >(Hnotend c_src) [|@memb_hd]
325 change with (current ? (niltape ?)) in match (None ?);
326 <nth_vec_map >Hmid_src whd in ⊢ (??%?→?); >Hdst normalize #H destruct (H)
332 definition match_m ≝ λsrc,dst,sig,n,is_startc,is_endc.
333 whileTM … (match_step src dst sig n is_startc is_endc)
334 (inr ?? (inr ?? (inl … (inr ?? start_nop)))).
336 definition R_match_m ≝
337 λsrc,dst,sig,n,is_startc,is_endc.λint,outt: Vector (tape sig) (S n).
339 nth src ? int (niltape ?) = midtape sig ls x (xs@end::rs) →
340 (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) → is_endc end = true →
341 (∀c0. memb ? c0 (xs@end::rs) = true → is_startc c0 = false) →
342 (current sig (nth dst (tape sig) int (niltape sig)) = None ? → outt = int) ∧
343 (is_startc x = true →
345 nth dst ? int (niltape ?) = midtape sig ls0 x0 rs0 →
346 (∃l,l1.x0::rs0 = l@x::xs@l1 ∧
349 (change_vec ?? int (midtape sig (reverse ? xs@x::ls) end rs) src)
350 (midtape sig ((reverse ? (l@x::xs))@ls0) cj l2) dst) ∨
351 ∀l,l1.x0::rs0 ≠ l@x::xs@l1)).
353 lemma not_sub_list_merge :
354 ∀T.∀a,b:list T. (∀l1.a ≠ b@l1) → (∀t,l,l1.a ≠ t::l@b@l1) → ∀l,l1.a ≠ l@b@l1.
355 #T #a #b #H1 #H2 #l elim l normalize //
358 lemma not_sub_list_merge_2 :
359 ∀T:DeqSet.∀a,b:list T.∀t. (∀l1.t::a ≠ b@l1) → (∀l,l1.a ≠ l@b@l1) → ∀l,l1.t::a ≠ l@b@l1.
360 #T #a #b #t #H1 #H2 #l elim l //
361 #t0 #l1 #IH #l2 cases (true_or_false (t == t0)) #Htt0
362 [ >(\P Htt0) % normalize #H destruct (H) cases (H2 l1 l2) /2/
363 | normalize % #H destruct (H) cases (\Pf Htt0) /2/ ]
367 lemma wsem_match_m : ∀src,dst,sig,n,is_startc,is_endc.
368 src ≠ dst → src < S n → dst < S n →
369 match_m src dst sig n is_startc is_endc ⊫ R_match_m src dst sig n is_startc is_endc.
370 #src #dst #sig #n #is_startc #is_endc #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
371 lapply (sem_while … (sem_match_step src dst sig n is_startc is_endc Hneq Hsrc Hdst) … Hloop) //
372 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
373 [ #tc #Hfalse #ls #x #xs #end #rs #Hmid_src #Hnotend #Hend #Hnotstart
374 cases (Hfalse … Hmid_src Hnotend Hend) -Hfalse
375 [(* current dest = None *) *
376 [ * #Hcur_dst #Houtc %
378 |#Hstart #ls0 #x0 #rs0 #Hmid_dst >Hmid_dst in Hcur_dst;
379 normalize in ⊢ (%→?); #H destruct (H)
381 | * #ls0 * #rs0 * #xs0 * * #Htc_dst #Hrs0 #HNone %
382 [ >Htc_dst normalize in ⊢ (%→?); #H destruct (H)
383 | #Hstart #ls1 #x1 #rs1 >Htc_dst #H destruct (H)
385 [ % %{[ ]} %{[ ]} % [ >append_nil >append_nil %]
386 #cj #ls2 #H destruct (H)
387 | #x2 #xs2 %2 #l #l1 % #Habs lapply (eq_f ?? (length ?) ?? Habs)
388 >length_append whd in ⊢ (??%(??%)→?); >length_append
389 >length_append normalize >commutative_plus whd in ⊢ (???%→?);
390 #H destruct (H) lapply e0 >(plus_n_O (|rs1|)) in ⊢ (??%?→?);
391 >associative_plus >associative_plus
392 #e1 lapply (injective_plus_r ??? e1) whd in ⊢ (???%→?);
397 |* #ls0 * #rs0 * #Hmid_dst #HFalse %
398 [ >Hmid_dst normalize in ⊢ (%→?); #H destruct (H)
399 | #Hstart #ls1 #x1 #rs1 >Hmid_dst #H destruct (H)
400 %1 %{[ ]} %{rs0} % [%] #cj #l2 #Hnotnil
401 >reverse_cons >associative_append @(HFalse ?? Hnotnil)
404 |-ta -tb #ta #tb #tc #Htrue #Hstar #IH #Hout lapply (IH Hout) -IH -Hout #IH whd
405 #ls #x #xs #end #rs #Hmid_src #Hnotend #Hend #Hnotstart
406 lapply (refl ? (current ? (nth dst ? ta (niltape ?))))
407 cases (current ? (nth dst ? ta (niltape ?))) in ⊢ (???%→?);
409 [#_ whd in Htrue; >Hmid_src in Htrue; #Htrue
410 cases (Htrue x (refl … )) -Htrue * #Htaneq #_
411 @False_ind >Hmid_dst in Htaneq; /2/
412 |#Hstart #ls0 #x0 #rs0 #Hmid_dst2 >Hmid_dst2 in Hmid_dst; normalize in ⊢ (%→?);
415 | #c #Hcurta_dst % [ >Hcurta_dst #H destruct (H) ]
416 #Hstart #ls0 #x0 #rs0 #Hmid_dst >Hmid_dst in Hcurta_dst; normalize in ⊢ (%→?);
417 #H destruct (H) whd in Htrue; >Hmid_src in Htrue; #Htrue
418 cases (Htrue x (refl …)) -Htrue #_ #Htrue cases (Htrue Hstart Hnotstart) -Htrue
419 cases (true_or_false (x==c)) #eqx
420 [ lapply (\P eqx) -eqx #eqx destruct (eqx)
421 #_ #Htrue cases (comp_list ? (xs@end::rs) rs0 is_endc)
422 #x1 * #tl1 * #tl2 * * * #Hxs #Hrs0 #Hnotendx1
424 [>append_nil #Hx1 <Hx1 in Hnotendx1; #Hnotendx1
425 lapply (Hnotendx1 end ?) [ @memb_append_l2 @memb_hd ]
426 >Hend #H destruct (H) ]
427 #ci -tl1 #tl1 #Hxs #H cases (H … (refl … )) -H
428 [ #Hendci % >Hrs0 in Hmid_dst; cut (ci = end ∧ x1 = xs)
429 [ lapply Hxs lapply Hnotendx1 lapply x1 elim xs in Hnotend;
431 [ #_ normalize #H destruct (H) /2/
432 | #x2 #xs2 #Hnotendx2 normalize #H destruct (H)
433 >(Hnotendx2 ? (memb_hd …)) in Hend; #H destruct (H) ]
434 | #x2 #xs2 #IH #Hnotendx2 *
435 [ #_ normalize #H destruct (H) >(Hnotendx2 ci ?) in Hendci;
437 | @memb_cons @memb_hd ]
438 | #x3 #xs3 #Hnotendx3 normalize #H destruct (H)
441 | #c0 #Hc0 @Hnotendx2 cases (orb_true_l … Hc0) -Hc0 #Hc0
443 | @memb_cons @memb_cons @Hc0 ]
444 | #c0 #Hc0 @Hnotendx3 @memb_cons @Hc0 ]
447 | * #Hcieq #Hx1eq >Hx1eq #Hmid_dst
448 cases (Htrue ??????? (refl ??) Hmid_dst Hnotend)
449 <Hcieq >Hendci * #H destruct (H) ]
451 [ >append_nil #Hrs0 destruct (Hrs0) * #Hcifalse#_ %2
452 cut (∃l.xs = x1@ci::l)
453 [lapply Hxs lapply Hnotendx1 lapply Hnotend lapply xs
454 -Hxs -xs -Hnotendx1 elim x1
456 [ #_ #_ normalize #H1 destruct (H1) >Hend in Hcifalse;
458 | #x2 #xs2 #_ #_ normalize #H >(cons_injective_l ????? H) %{xs2} % ]
460 [ #_ #Hnotendxs2 normalize #H destruct (H)
461 >(Hnotendxs2 ? (memb_hd …)) in Hend; #H destruct (H)
462 | #x3 #xs3 #Hnotendxs3 #Hnotendxs2 normalize #H destruct (H)
464 [ #xs4 #Hxs4 >Hxs4 %{xs4} %
465 | #c0 #Hc0 cases (orb_true_l … Hc0) -Hc0 #Hc0
466 [ >(\P Hc0) @Hnotendxs3 @memb_hd
467 | @Hnotendxs3 @memb_cons @memb_cons @Hc0 ]
468 | #c0 #Hc0 @Hnotendxs2 @memb_cons @Hc0 ]
472 #l0 #l1 % #H lapply (eq_f ?? (length ?) ?? H) -H
473 >length_append normalize >length_append >length_append
474 normalize >commutative_plus normalize #H destruct (H) -H
475 >associative_plus in e0; >associative_plus
476 >(plus_n_O (|x1|)) in ⊢(??%?→?); #H lapply (injective_plus_r … H)
477 -H normalize #H destruct (H)
478 | #cj #tl2' #Hrs0 * #Hcifalse #Hcomp
479 lapply (Htrue ls c x1 ci tl1 ls0 (cj::tl2') ???)
480 [ #c0 #Hc0 cases (orb_true_l … Hc0) #Hc0
481 [ @Hnotend >(\P Hc0) @memb_hd
485 | * * #_ #_ -Htrue #Htrue lapply (Htrue ?? (refl ??) ?) [ @(Hcomp ?? (refl ??)) ]
486 * #Htb >Htb #Hendci >Hrs0 >Hxs
487 cases (IH ls c xs end rs ? Hnotend Hend Hnotstart) -IH
488 [| >Htb >nth_change_vec_neq [|@sym_not_eq //] @Hmid_src ]
489 #_ #IH lapply Hxs lapply Hnotendx1 -Hxs -Hnotendx1 cases x1 in Hrs0;
490 [ #Hrs0 #_ whd in ⊢ (???%→?); #Hxs
491 cases (IH Hstart (c::ls0) cj tl2' ?)
492 [ -IH * #l * #l1 * #Hll1 #IH % %{(c::l)} %{l1}
494 #cj0 #l2 #Hcj0 >(IH … Hcj0) >Htb
495 >change_vec_commute // >change_vec_change_vec
496 >change_vec_commute [|@sym_not_eq // ] @eq_f3 //
497 >reverse_cons >associative_append %
498 | #IH %2 #l #l1 >(?:l@c::xs@l1 = l@(c::xs)@l1) [|%]
500 [ #l2 cut (∃xs'.xs = ci::xs')
502 [ normalize #H destruct (H) >Hend in Hendci; #H destruct (H)
503 | #ci' #xs' normalize #H lapply (cons_injective_l ????? H)
506 * #xs' #Hxs' >Hxs' normalize % #H destruct (H)
507 lapply (Hcomp … (refl ??)) * /2/
508 |#t #l2 #l3 % normalize #H lapply (cons_injective_r ????? H)
509 -H #H >H in IH; #IH cases (IH l2 l3) -IH #IH @IH % ]
510 | >Htb >nth_change_vec // >Hmid_dst >Hrs0 % ]
511 | #x2 #xs2 normalize in ⊢ (%→?); #Hrs0 #Hnotendxs2 normalize in ⊢ (%→?);
512 #Hxs cases (IH Hstart (c::ls0) x2 (xs2@cj::tl2') ?)
513 [ -IH * #l * #l1 * #Hll1 #IH % %{(c::l)} %{l1}
515 #cj0 #l2 #Hcj0 >(IH … Hcj0) >Htb
516 >change_vec_commute // >change_vec_change_vec
517 >change_vec_commute [|@sym_not_eq // ] @eq_f3 //
518 >reverse_cons >associative_append %
519 | -IH #IH %2 #l #l1 >(?:l@c::xs@l1 = l@(c::xs)@l1) [|%]
520 @not_sub_list_merge_2 [| @IH]
521 cut (∃l2.xs = (x2::xs2)@ci::l2)
523 lapply Hnotend -Hnotend lapply Hxs
524 >(?:x2::xs2@ci::tl1 = (x2::xs2)@ci::tl1) [|%]
525 lapply (x2::xs2) elim xs
527 [ normalize in ⊢ (%→?); #H1 destruct (H1)
528 >Hendci in Hend; #Hend destruct (Hend)
529 | #x3 #xs3 normalize in ⊢ (%→?); #H1 destruct (H1)
530 #_ #Hnotendx3 >(Hnotendx3 ? (memb_hd …)) in Hend;
531 #Hend destruct (Hend)
534 [ normalize in ⊢ (%→?); #Hxs3 destruct (Hxs3) #_ #_
536 | #x4 #xs4 normalize in ⊢ (%→?); #Hxs3xs4 #Hnotend
537 #Hnotendxs4 destruct (Hxs3xs4) cases (IHin ? e0 ??)
538 [ #l0 #Hxs3 >Hxs3 %{l0} %
539 | #c0 #Hc0 @Hnotend cases (orb_true_l … Hc0) -Hc0 #Hc0
541 | @memb_cons @memb_cons @Hc0 ]
542 | #c0 #Hc0 @Hnotendxs4 @memb_cons //
547 >Hxs' #l3 normalize >associative_append normalize % #H
548 destruct (H) lapply (append_l2_injective ?????? e1) //
549 #H1 destruct (H1) cases (Hcomp ?? (refl ??)) /2/
550 | >Htb >nth_change_vec // >Hmid_dst >Hrs0 % ]
555 |lapply (\Pf eqx) -eqx #eqx >Hmid_dst #Htrue
556 cases (Htrue ? (refl ??) eqx) -Htrue #Htb #Hendcx #_
558 [ #_ %2 #l #l1 cases l
561 [ normalize % #H destruct (H) cases eqx /2/
562 | #tmp1 #l2 normalize % #H destruct (H) ]
563 | #tmp1 #l2 normalize % #H destruct (H) ]
564 | #tmp1 #l2 normalize % #H destruct (H)cases l2 in e0;
565 [ normalize #H1 destruct (H1)
566 | #tmp2 #l3 normalize #H1 destruct (H1) ]
568 | #r1 #rs1 normalize in ⊢ (???(????%?)→?); #Htb >Htb in IH; #IH
569 cases (IH ls x xs end rs ? Hnotend Hend Hnotstart)
570 [| >Htb >nth_change_vec_neq [|@sym_not_eq //] @Hmid_src ] -IH
571 #_ #IH cases (IH Hstart (c::ls0) r1 rs1 ?)
572 [|| >nth_change_vec // ] -IH
573 [ * #l * #l1 * #Hll1 #Hout % %{(c::l)} %{l1} % >Hll1 //
574 >reverse_cons >associative_append #cj0 #ls #Hl1 >(Hout ?? Hl1)
575 >change_vec_commute in ⊢ (??(???%??)?); // @sym_not_eq //
576 | #IH %2 @(not_sub_list_merge_2 ?? (x::xs)) normalize [|@IH]
577 #l1 % #H destruct (H) cases eqx /2/