2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
12 include "turing/universal/move_char_c.ma".
13 include "turing/universal/move_char_l.ma".
14 include "turing/universal/tuples.ma".
16 definition init_cell_states ≝ initN 2.
18 definition init_cell ≝
19 mk_TM STape init_cell_states
23 [ None ⇒ 〈1, Some ? 〈〈null,false〉,N〉〉
24 | Some _ ⇒ 〈1, None ?〉 ]
28 definition R_init_cell ≝ λt1,t2.
29 (∃c.current STape t1 = Some ? c ∧ t2 = t1) ∨
30 (current STape t1 = None ? ∧ t2 = midtape ? (left ? t1) 〈null,false〉 (right ? t1)).
32 axiom sem_init_cell : Realize ? init_cell R_init_cell.
34 definition swap_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 4) alpha.
37 λalpha:FinSet.λd:alpha.
38 mk_TM alpha (mcl_states alpha)
42 [ None ⇒ 〈〈3,d〉,None ?〉
46 〈〈1,a'〉,Some ? 〈a',R〉〉
47 | S q' ⇒ match q' with
50 | S q' ⇒ match q' with
54 〈〈3,d〉,None ?〉 ] ] ] ])
56 (λq.let 〈q',a〉 ≝ q in q' == 3).
61 t1 = midtape alpha ls b (a::rs) →
62 t2 = midtape alpha ls a (b::rs).
66 ∀alpha:FinSet.∀d,a,ls,a0,rs.
67 step alpha (swap alpha d)
68 (mk_config ?? 〈0,a〉 (mk_tape … ls (Some ? a0) rs)) =
69 mk_config alpha (states ? (swap alpha d)) 〈1,a0〉
70 (tape_move_right alpha ls a0 rs).
78 ∀alpha:FinSet.∀d,a,ls,a0,rs.
79 step alpha (swap alpha d)
80 (mk_config ?? 〈1,a〉 (mk_tape … ls (Some ? a0) rs)) =
81 mk_config alpha (states ? (swap alpha d)) 〈2,a0〉
82 (tape_move_left alpha ls a rs).
83 #alpha #sep #a #ls #a0 * //
87 ∀alpha:FinSet.∀d,a,ls,a0,rs.
88 step alpha (swap alpha d)
89 (mk_config ?? 〈2,a〉 (mk_tape … ls (Some ? a0) rs)) =
90 mk_config alpha (states ? (swap alpha d)) 〈3,d〉
91 (tape_move_left alpha ls a rs).
92 #alpha #sep #a #ls #a0 * //
98 Realize alpha (swap alpha d) (R_swap alpha).
99 #alpha #d #tapein @(ex_intro ?? 4) cases tapein
100 [ @ex_intro [| % [ % | #a #b #ls #rs #Hfalse destruct (Hfalse) ] ]
101 | #a #al @ex_intro [| % [ % | #a #b #ls #rs #Hfalse destruct (Hfalse) ] ]
102 | #a #al @ex_intro [| % [ % | #a #b #ls #rs #Hfalse destruct (Hfalse) ] ]
103 | #ls #c #rs cases rs
104 [ @ex_intro [| % [ % | #a #b #ls0 #rs0 #Hfalse destruct (Hfalse) ] ]
105 | -rs #r #rs @ex_intro
108 | #r0 #c0 #ls0 #rs0 #Htape destruct (Htape) normalize cases ls0
109 [% | #l1 #ls1 %] ] ] ] ]
112 axiom ssem_move_char_l :
114 Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
119 ls # current c # table # d? rs
121 ls # current c # table # d? rs init
123 ls # current c # table # d? rs
125 ls # current c # table # d rs ----------------------
127 ls # current c # table # d rs
129 ls # current c # table d # rs --------------------
131 ls # current c # table d # rs
133 ls # current c # d table # rs sub1
135 ls # current c # d table # rs
137 ls # current c d # table # rs -------------------
139 ls # current c d # table # rs -------------------
141 ls # current c d # table # rs
143 ls # c current d # table # rs sub1
145 ls # c current d # table # rs
147 ls c # current d # table # rs ------------------
169 (* l1 # l2 r ---> l1 r # l2
173 seq ? (move_l …) (seq ? (move_char_l STape 〈grid,false〉)
174 (swap STape 〈grid,false〉)).
175 definition R_mtr_aux ≝ λt1,t2.
176 ∀l1,l2,l3,r. t1 = midtape STape (l2@〈grid,false〉::l1) r l3 → no_grids l2 →
177 t2 = midtape STape l1 r (〈grid,false〉::reverse ? l2@l3).
179 lemma sem_mtr_aux : Realize ? mtr_aux R_mtr_aux.
181 cases (sem_seq … (sem_move_l …) (sem_seq … (ssem_move_char_l STape 〈grid,false〉)
182 (sem_swap STape 〈grid,false〉)) intape)
183 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
184 #l1 #l2 #l3 #r #Hintape #Hl2
185 cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
186 * #tb * whd in ⊢(%→?); generalize in match Hta; -Hta cases l2 in Hl2;
187 [ #_ #Hta #Htb lapply (Htb … Hta) -Htb * #Htb lapply (Htb (refl ??)) -Htb #Htb #_
188 whd in ⊢(%→?); >Htb #Houtc lapply (Houtc … Hta) -Houtc #Houtc @Houtc
189 | #c0 #l0 #Hnogrids #Hta #Htb lapply (Htb … Hta) -Htb * #_ #Htb
190 lapply (Htb … (refl ??) ??)
191 [ cases (true_or_false (memb STape 〈grid,false〉 l0)) #Hmemb
192 [ @False_ind lapply (Hnogrids 〈grid,false〉 ?)
193 [ @memb_cons // | normalize #Hfalse destruct (Hfalse) ]
195 | % #Hc0 lapply (Hnogrids c0 ?)
196 [ @memb_hd | >Hc0 normalize #Hfalse destruct (Hfalse) ]
197 | #Htb whd in ⊢(%→?); >Htb #Houtc lapply (Houtc … (refl ??)) -Houtc #Houtc
198 >reverse_cons >associative_append @Houtc
202 definition move_tape_r ≝
203 seq ? (move_r …) (seq ? init_cell (seq ? (move_l …)
204 (seq ? (swap STape 〈grid,false〉)
205 (seq ? mtr_aux (seq ? (move_l …) (seq ? mtr_aux (move_r …))))))).
207 definition R_move_tape_r ≝ λt1,t2.
208 ∀rs,n,table,c0,bc0,curconfig,ls0.
209 bit_or_null c0 = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) →
210 t1 = midtape STape (table@〈grid,false〉::〈c0,bc0〉::curconfig@〈grid,false〉::ls0)
213 t2 = midtape STape (〈c0,bc0〉::ls0) 〈grid,false〉 (reverse STape curconfig@〈null,false〉::
214 〈grid,false〉::reverse STape table@[〈grid,false〉])) ∨
215 (∃r0,rs0.rs = r0::rs0 ∧
216 t2 = midtape STape (〈c0,bc0〉::ls0) 〈grid,false〉 (reverse STape curconfig@r0::
217 〈grid,false〉::reverse STape table@〈grid,false〉::rs0)).
219 lemma sem_move_tape_r : Realize ? move_tape_r R_move_tape_r.
221 cases (sem_seq …(sem_move_r …) (sem_seq … sem_init_cell (sem_seq … (sem_move_l …)
222 (sem_seq … (sem_swap STape 〈grid,false〉) (sem_seq … sem_mtr_aux
223 (sem_seq … (sem_move_l …) (sem_seq … sem_mtr_aux (sem_move_r …))))))) tapein)
224 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
225 #rs #n #table #c0 #bc0 #curconfig #ls0 #Hbitnullc0 #Hbitnullcc #Htable #Htapein
226 cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Htapein) -Hta #Hta
227 * #tb * whd in ⊢ (%→?); *
229 generalize in match Hta; generalize in match Htapein; -Htapein -Hta cases rs
230 [ #_ #Hta >Hta normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
231 #r1 #rs1 #Htapein #Hta change with (midtape ?? r1 rs1) in Hta:(???%); >Hta
232 #Hr0 whd in Hr0:(??%?); #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc #Htc
233 * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd #Htd
234 * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?) [ (*memb_reverse @(no_grids_in_table … Htable)*) @daemon ] -Hte #Hte
235 * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf #Htf
236 * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?) [ #x #Hx @bit_or_null_not_grid @Hbitnullcc // ] -Htg #Htg
237 whd in ⊢ (%→?); #Houtc lapply (Houtc … Htg) -Houtc #Houtc
238 %2 @(ex_intro ?? r1) @(ex_intro ?? rs1) % [%] @Houtc
239 | * generalize in match Hta; generalize in match Htapein; -Htapein -Hta cases rs
240 [|#r1 #rs1 #_ #Hta >Hta normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
241 #Htapein #Hta change with (rightof ???) in Hta:(???%); >Hta
242 #Hr0 whd in Hr0:(??%?); #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc #Htc
243 * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd #Htd
244 * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?) [(*same as above @(no_grids_in_table … Htable) *) @daemon ] -Hte #Hte
245 * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf #Htf
246 * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?) [ #x #Hx @bit_or_null_not_grid @Hbitnullcc // ] -Htg #Htg
247 whd in ⊢ (%→?); #Houtc lapply (Houtc … Htg) -Houtc #Houtc
254 ls # current c # table # d rs
256 ls # current c # table # d rs
258 ls # current c # table d # rs
260 ls # current c # d table # rs
262 ls # current c # d table # rs
264 ls # current c d # table # rs
266 ls # current c d # table # rs
268 ls # c current c # table # rs
270 ls # c current c # table # rs
272 ls c # current c # table # rs
285 axiom move_tape_l : TM STape.
286 (* seq ? (move_r …) (seq ? init_cell (seq ? (move_l …)
287 (seq ? (swap STape 〈grid,false〉)
288 (seq ? mtr_aux (seq ? (move_l …) mtr_aux))))). *)
290 definition R_move_tape_l ≝ λt1,t2.
291 ∀rs,n,table,c0,bc0,curconfig,ls0.
292 bit_or_null c0 = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) →
293 t1 = midtape STape (table@〈grid,false〉::〈c0,bc0〉::curconfig@〈grid,false〉::ls0)
296 t2 = midtape STape [] 〈grid,false〉
297 (reverse ? curconfig@〈null,false〉::〈grid,false〉::reverse ? table@〈grid,false〉::〈c0,bc0〉::rs)) ∨
298 (∃l1,ls1. ls0 = l1::ls1 ∧
299 t2 = midtape STape ls1 〈grid,false〉
300 (reverse ? curconfig@l1::〈grid,false〉::reverse ? table@〈grid,false〉::〈c0,bc0〉::rs)).
302 axiom sem_move_tape_l : Realize ? move_tape_l R_move_tape_l.
306 case bit false: move_tape_l
307 case bit true: move_tape_r
308 case null: adv_to_grid_l; move_l; adv_to_grid_l;
311 definition lift_tape ≝ λls,c,rs.
313 let c' ≝ match c0 with
317 mk_tape STape ls c' rs.
319 definition sim_current_of_tape ≝ λt.
320 match current STape t with
321 [ None ⇒ 〈null,false〉
324 definition mk_tuple ≝ λc,newc,mv.
325 c @ 〈comma,false〉:: newc @ 〈comma,false〉 :: [〈mv,false〉].
327 inductive match_in_table (c,newc:list STape) (mv:unialpha) : list STape → Prop ≝
330 match_in_table c newc mv (mk_tuple c newc mv@〈bar,false〉::tb)
333 match_in_table c newc mv tb →
334 match_in_table c newc mv (mk_tuple c0 newc0 mv0@〈bar,false〉::tb).
336 definition move_of_unialpha ≝
338 [ bit x ⇒ match x with [ true ⇒ R | false ⇒ L ]
341 definition R_uni_step ≝ λt1,t2.
342 ∀n,table,c,c1,ls,rs,curs,curc,news,newc,mv.
344 match_in_table (〈c,false〉::curs@[〈curc,false〉])
345 (〈c1,false〉::news@[〈newc,false〉]) mv table →
346 t1 = midtape STape (〈grid,false〉::ls) 〈c,false〉
347 (curs@〈curc,false〉::〈grid,false〉::table@〈grid,false〉::rs) →
348 ∀t1',ls1,rs1.t1' = lift_tape ls 〈curc,false〉 rs →
349 (t2 = midtape STape (〈grid,false〉::ls1) 〈c1,false〉
350 (news@〈newc,false〉::〈grid,false〉::table@〈grid,false〉::rs1) ∧
351 lift_tape ls1 〈newc,false〉 rs1 =
352 tape_move STape t1' (Some ? 〈〈newc,false〉,move_of_unialpha mv〉)).
354 definition no_nulls ≝
355 λl:list STape.∀x.memb ? x l = true → is_null (\fst x) = false.
357 definition current_of_alpha ≝ λc:STape.
358 match \fst c with [ null ⇒ None ? | _ ⇒ Some ? c ].
360 definition legal_tape ≝ λls,c,rs.
361 let t ≝ mk_tape STape ls (current_of_alpha c) rs in
362 left ? t = ls ∧ right ? t = rs ∧ current ? t = current_of_alpha c.
364 lemma legal_tape_cases :
365 ∀ls,c,rs.legal_tape ls c rs →
366 \fst c ≠ null ∨ (\fst c = null ∧ (ls = [] ∨ rs = [])).
367 #ls #c #rs cases c #c0 #bc0 cases c0
368 [ #c1 normalize #_ % % #Hfalse destruct (Hfalse)
373 | #r0 #rs0 normalize * * #_ #Hrs destruct (Hrs) ]
375 |*: #_ % % #Hfalse destruct (Hfalse) ]
378 axiom legal_tape_conditions :
379 ∀ls,c,rs.(\fst c ≠ null ∨ ls = [] ∨ rs = []) → legal_tape ls c rs.
382 [ >(eq_pair_fst_snd ?? c) cases (\fst c)
384 | * #Hfalse @False_ind /2/
387 | cases ls [ * #Hfalse @False_ind /2/ ]
393 definition R_move_tape_r_abstract ≝ λt1,t2.
394 ∀rs,n,table,curc,curconfig,ls.
395 bit_or_null curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) →
396 t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls)
398 no_nulls rs → no_marks rs →
399 legal_tape ls 〈curc,false〉 rs →
400 ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs →
402 (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉::
403 〈grid,false〉::reverse ? table@〈grid,false〉::rs1) ∧
404 lift_tape ls1 〈newc,false〉 rs1 =
405 tape_move_right STape ls 〈curc,false〉 rs ∧ legal_tape ls1 〈newc,false〉 rs1).
407 lemma lift_tape_not_null :
408 ∀ls,c,rs. is_null (\fst c) = false →
409 lift_tape ls c rs = mk_tape STape ls (Some ? c) rs.
410 #ls * #c0 #bc0 #rs cases c0
411 [|normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
415 lemma mtr_concrete_to_abstract :
416 ∀t1,t2.R_move_tape_r t1 t2 → R_move_tape_r_abstract t1 t2.
417 #t1 #t2 whd in ⊢(%→?); #Hconcrete
418 #rs #n #table #curc #curconfig #ls #Hcurc #Hcurconfig #Htable #Ht1
419 #Hrsnonulls #Hrsnomarks #Htape #t1' #Ht1'
420 cases (Hconcrete … Htable Ht1) //
422 @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? [])
423 @(ex_intro ?? null) %
428 | * * #r0 #br0 * #rs0 * #Hrs
429 cut (br0 = false) [@(Hrsnomarks 〈r0,br0〉) >Hrs @memb_hd]
430 #Hbr0 >Hbr0 in Hrs; #Hrs #Ht2
431 @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? rs0)
435 | >Hrs >lift_tape_not_null
437 | @(Hrsnonulls 〈r0,false〉) >Hrs @memb_hd ] ]
438 | @legal_tape_conditions % % % #Hr0 >Hr0 in Hrs; #Hrs
439 lapply (Hrsnonulls 〈null,false〉 ?)
440 [ >Hrs @memb_hd | normalize #H destruct (H) ]
445 definition R_move_tape_l_abstract ≝ λt1,t2.
446 ∀rs,n,table,curc,curconfig,ls.
447 bit_or_null curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) →
448 t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls)
450 no_nulls ls → no_marks ls →
451 legal_tape ls 〈curc,false〉 rs →
452 ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs →
454 (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉::
455 〈grid,false〉::reverse ? table@〈grid,false〉::rs1) ∧
456 lift_tape ls1 〈newc,false〉 rs1 =
457 tape_move_left STape ls 〈curc,false〉 rs ∧ legal_tape ls1 〈newc,false〉 rs1).
459 lemma mtl_concrete_to_abstract :
460 ∀t1,t2.R_move_tape_l t1 t2 → R_move_tape_l_abstract t1 t2.
461 #t1 #t2 whd in ⊢(%→?); #Hconcrete
462 #rs #n #table #curc #curconfig #ls #Hcurc #Hcurconfig #Htable #Ht1
463 #Hlsnonulls #Hlsnomarks #Htape #t1' #Ht1'
464 cases (Hconcrete … Htable Ht1) //
467 @(ex_intro ?? (〈curc,false〉::rs))
468 @(ex_intro ?? null) %
473 | * * #l0 #bl0 * #ls0 * #Hls
474 cut (bl0 = false) [@(Hlsnomarks 〈l0,bl0〉) >Hls @memb_hd]
475 #Hbl0 >Hbl0 in Hls; #Hls #Ht2
477 @(ex_intro ?? (〈curc,false〉::rs))
481 | >Hls >lift_tape_not_null
483 | @(Hlsnonulls 〈l0,false〉) >Hls @memb_hd ] ]
484 | @legal_tape_conditions % % % #Hl0 >Hl0 in Hls; #Hls
485 lapply (Hlsnonulls 〈null,false〉 ?)
486 [ >Hls @memb_hd | normalize #H destruct (H) ]
490 lemma Realize_to_Realize :
491 ∀alpha,M,R1,R2.(∀t1,t2.R1 t1 t2 → R2 t1 t2) → Realize alpha M R1 → Realize alpha M R2.
492 #alpha #M #R1 #R2 #Himpl #HR1 #intape
493 cases (HR1 intape) -HR1 #k * #outc * #Hloop #HR1
494 @(ex_intro ?? k) @(ex_intro ?? outc) % /2/
497 lemma sem_move_tape_l_abstract : Realize … move_tape_l R_move_tape_l_abstract.
498 @(Realize_to_Realize … mtl_concrete_to_abstract) //
501 lemma sem_move_tape_r_abstract : Realize … move_tape_r R_move_tape_r_abstract.
502 @(Realize_to_Realize … mtr_concrete_to_abstract) //
506 t1 = ls # cs c # table # rs
508 let simt ≝ lift_tape ls c rs in
509 let simt' ≝ move_left simt' in
511 t2 = left simt'# cs (sim_current_of_tape simt') # table # right simt'
517 definition R_exec_move ≝ λt1,t2.
518 ∀ls,current,table1,newcurrent,table2,rs.
519 t1 = midtape STape (current@〈grid,false〉::ls) 〈grid,false〉
520 (table1@〈comma,true〉::newcurrent@〈comma,false〉::move::table2@
522 table_TM (table1@〈comma,false〉::newcurrent@〈comma,false〉::move::table2) →
530 if is_true(current) (* current state is final *)
535 if is_marked(current) = false (* match ok *)
542 definition move_tape ≝
543 ifTM ? (test_char ? (λc:STape.c == 〈bit false,false〉))
544 (* spostamento a sinistra: verificare se per caso non conviene spostarsi
545 sulla prima grid invece dell'ultima *)
546 (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c))) move_tape_l)
547 (ifTM ? (test_char ? (λc:STape.c == 〈bit true,false〉))
548 (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c))) move_tape_r)
549 (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
550 (seq ? (move_l …) (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))))
553 definition R_move_tape ≝ λt1,t2.
554 ∀rs,n,table1,c,table2,curc,curconfig,ls.
555 bit_or_null curc = true → bit_or_null c = true → only_bits_or_nulls curconfig →
556 table_TM n (reverse ? table1@〈c,false〉::table2) →
557 t1 = midtape STape (table1@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls)
558 〈c,false〉 (table2@〈grid,false〉::rs) →
559 no_nulls ls → no_nulls rs → no_marks ls → no_marks rs →
560 legal_tape ls 〈curc,false〉 rs →
561 ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs →
563 legal_tape ls1 〈newc,false〉 rs1 ∧
564 (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉::
565 〈grid,false〉::reverse ? table1@〈c,false〉::table2@〈grid,false〉::rs1) ∧
566 ((c = bit false ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_left STape ls 〈curc,false〉 rs) ∨
567 (c = bit true ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_right STape ls 〈curc,false〉 rs) ∨
568 (c = null ∧ ls1 = ls ∧ rs1 = rs ∧ curc = newc))).
570 lemma sem_move_tape : Realize ? move_tape R_move_tape.
572 cases (sem_if ? (test_char ??) … tc_true (sem_test_char ? (λc:STape.c == 〈bit false,false〉))
573 (sem_seq … (sem_adv_to_mark_r ? (λc:STape.is_grid (\fst c))) sem_move_tape_l_abstract)
574 (sem_if ? (test_char ??) … tc_true (sem_test_char ? (λc:STape.c == 〈bit true,false〉))
575 (sem_seq … (sem_adv_to_mark_r ? (λc:STape.is_grid (\fst c))) sem_move_tape_r_abstract)
576 (sem_seq … (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
577 (sem_seq … (sem_move_l …) (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))))) intape)
578 #k * #outc * #Hloop #HR
579 @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
580 #rs #n #table1 #c #table2 #curc #curconfig #ls
581 #Hcurc #Hc #Hcurconfig #Htable #Hintape #Hls #Hrs #Hls1 #Hrs1 #Htape #t1' #Ht1'
582 generalize in match HR; -HR *
583 [ * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈c,false〉 ?)
584 [| >Hintape % ] -Hta #Hceq #Hta lapply (\P Hceq) -Hceq #Hceq destruct (Hta Hceq)
585 * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hintape) -Htb -Hintape
586 [ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
587 * #_ #Htb lapply (Htb … (refl ??) (refl ??) ?)
588 [ @daemon ] -Htb >append_cons <associative_append #Htb
589 whd in ⊢ (%→?); #Houtc lapply (Houtc … Htb … Ht1') //
590 [ >reverse_append >reverse_append >reverse_reverse @Htable |]
591 -Houtc -Htb * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal
592 @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) %
595 [ >Houtc >reverse_append >reverse_append >reverse_reverse
596 >associative_append >associative_append %
599 | * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈c,false〉 ?)
600 [| >Hintape % ] -Hta #Hcneq cut (c ≠ bit false)
601 [ lapply (\Pf Hcneq) @not_to_not #Heq >Heq % ] -Hcneq #Hcneq #Hta destruct (Hta)
603 [ * #tb * whd in ⊢ (%→?);#Htb cases (Htb 〈c,false〉 ?)
604 [| >Hintape % ] -Htb #Hceq #Htb lapply (\P Hceq) -Hceq #Hceq destruct (Htb Hceq)
605 * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Hintape) -Htc -Hintape
606 [ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
607 * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?)
608 [ @daemon ] -Htc >append_cons <associative_append #Htc
609 whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc … Ht1') //
610 [ >reverse_append >reverse_append >reverse_reverse @Htable |]
611 -Houtc -Htc * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal
612 @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) %
615 [ >Houtc >reverse_append >reverse_append >reverse_reverse
616 >associative_append >associative_append %
619 | * #tb * whd in ⊢ (%→?); #Htb cases (Htb 〈c,false〉 ?)
620 [| >Hintape % ] -Htb #Hcneq' cut (c ≠ bit true)
621 [ lapply (\Pf Hcneq') @not_to_not #Heq >Heq % ] -Hcneq' #Hcneq' #Htb destruct (Htb)
622 * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Hintape)
623 [ * >(bit_or_null_not_grid … Hc) #Hfalse destruct (Hfalse) ] -Htc
624 * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?) [@daemon] -Htc #Htc
625 * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd -Htc
626 whd in ⊢ (???%→?); #Htd whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc *
627 [ * >(bit_or_null_not_grid … Hcurc) #Hfalse destruct (Hfalse) ]
628 * #_ #Houtc lapply (Houtc … (refl ??) (refl ??) ?) [@daemon] -Houtc #Houtc
629 @(ex_intro ?? ls) @(ex_intro ?? rs) @(ex_intro ?? curc) %
634 generalize in match Hcneq; generalize in match Hcneq';
635 cases c in Hc; normalize //
636 [ * #_ normalize [ #Hfalse @False_ind cases Hfalse /2/ | #_ #Hfalse @False_ind cases Hfalse /2/ ]
637 |*: #Hfalse destruct (Hfalse) ]