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/while_machine.ma".
14 (******************* write a given symbol under the head **********************)
15 definition write_states ≝ initN 2.
17 definition wr0 : write_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
18 definition wr1 : write_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
20 definition write ≝ λalpha,c.
21 mk_TM alpha write_states
24 [ O ⇒ 〈wr1,Some ? c,N〉
25 | S _ ⇒ 〈wr1,None ?,N〉 ])
28 definition R_write ≝ λalpha,c,t1,t2.
29 ∀ls,x,rs.t1 = midtape alpha ls x rs → t2 = midtape alpha ls c rs.
31 lemma sem_write : ∀alpha,c.Realize ? (write alpha c) (R_write alpha c).
32 #alpha #c #t @(ex_intro … 2) @ex_intro
33 [|% [% |#ls #c #rs #Ht >Ht % ] ]
36 definition R_write_strong ≝ λalpha,c,t1,t2.
37 t2 = midtape alpha (left ? t1) c (right ? t1).
39 lemma sem_write_strong : ∀alpha,c.Realize ? (write alpha c) (R_write_strong alpha c).
40 #alpha #c #t @(ex_intro … 2) @ex_intro
41 [|% [% |cases t normalize // ] ]
44 (******************** moves the head one step to the right ********************)
46 definition move_states ≝ initN 2.
47 definition move0 : move_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
48 definition move1 : move_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
51 λalpha:FinSet.mk_TM alpha move_states
54 [ None ⇒ 〈move1,None ?,N〉
55 | Some a' ⇒ match (pi1 … q) with
56 [ O ⇒ 〈move1,Some ? a',R〉
57 | S q ⇒ 〈move1,None ?,N〉 ] ])
58 move0 (λq.q == move1).
60 definition R_move_r ≝ λalpha,t1,t2.
61 (current ? t1 = None ? → t1 = t2) ∧
63 t1 = midtape alpha ls c rs →
64 t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
66 (current ? t1 = None ? ∧ t1 = t2) ∨
68 t1 = midtape alpha ls c rs ∧
69 t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).*)
72 ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
73 #alpha #intape @(ex_intro ?? 2) cases intape
75 [| % [ % | % // #ls #c #rs #H destruct ] ]
77 [| % [ % | % // #ls #c #rs #H destruct ] ]
79 [| % [ % | % // #ls #c #rs #H destruct ] ]
81 @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct]
82 #ls1 #c1 #rs1 #H destruct cases rs1 // ] ] ]
85 (******************** moves the head one step to the left *********************)
88 λalpha:FinSet.mk_TM alpha move_states
91 [ None ⇒ 〈move1,None ?,N〉
92 | Some a' ⇒ match pi1 … q with
93 [ O ⇒ 〈move1,Some ? a',L〉
94 | S q ⇒ 〈move1,None ?,N〉 ] ])
95 move0 (λq.q == move1).
97 definition R_move_l ≝ λalpha,t1,t2.
98 (current ? t1 = None ? → t1 = t2) ∧
100 t1 = midtape alpha ls c rs →
101 t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
104 ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
105 #alpha #intape @(ex_intro ?? 2) cases intape
107 [| % [ % | % // #ls #c #rs #H destruct ] ]
109 [| % [ % | % // #ls #c #rs #H destruct ] ]
111 [| % [ % | % // #ls #c #rs #H destruct ] ]
113 @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct]
114 #ls1 #c1 #rs1 #H destruct cases ls1 // ] ] ]
117 (* a slightly different move machine. *)
118 definition smove_states ≝ initN 2.
120 definition smove0 : smove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
121 definition smove1 : smove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
123 definition trans_smove ≝
125 λp:smove_states × (option sig).
126 let 〈q,a〉 ≝ p in match (pi1 … q) with
127 [ O ⇒ 〈smove1,None sig, D〉
128 | S _ ⇒ 〈smove1,None sig, N〉 ].
131 λsig,D.mk_TM sig smove_states (trans_smove sig D) smove0 (λq.q == smove1).
134 λalpha,D,t1,t2. t2 = tape_move alpha t1 D.
136 lemma sem_move_single :
137 ∀alpha,D.move alpha D ⊨ Rmove alpha D.
138 #alpha #D #int %{2} %{(mk_config ? smove_states smove1 ?)} [| % % ]
141 (********************************* test char **********************************)
143 (* the test_char machine ends up in two different states q1 and q2 wether or not
144 the current character satisfies a boolean test function passed as a parameter to
146 The machine ends up in q1 also in case there is no current character.
149 definition tc_states ≝ initN 3.
151 definition tc_start : tc_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
152 definition tc_true : tc_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
153 definition tc_false : tc_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
155 definition test_char ≝
156 λalpha:FinSet.λtest:alpha→bool.
157 mk_TM alpha tc_states
160 [ None ⇒ 〈tc_false, None ?,N〉
163 [ true ⇒ 〈tc_true,None ?,N〉
164 | false ⇒ 〈tc_false,None ?,N〉 ]])
165 tc_start (λx.notb (x == tc_start)).
167 definition Rtc_true ≝
169 (∃c. current alpha t1 = Some ? c ∧ test c = true) ∧ t2 = t1.
171 definition Rtc_false ≝
173 (∀c. current alpha t1 = Some ? c → test c = false) ∧ t2 = t1.
176 ∀alpha,test,ls,a0,rs. test a0 = true →
177 step alpha (test_char alpha test)
178 (mk_config ?? tc_start (midtape … ls a0 rs)) =
179 mk_config alpha (states ? (test_char alpha test)) tc_true
180 (midtape … ls a0 rs).
181 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
182 whd in match (trans … 〈?,?〉); >Htest %
186 ∀alpha,test,ls,a0,rs. test a0 = false →
187 step alpha (test_char alpha test)
188 (mk_config ?? tc_start (midtape … ls a0 rs)) =
189 mk_config alpha (states ? (test_char alpha test)) tc_false
190 (midtape … ls a0 rs).
191 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
192 whd in match (trans … 〈?,?〉); >Htest %
195 lemma sem_test_char :
197 accRealize alpha (test_char alpha test)
198 tc_true (Rtc_true alpha test) (Rtc_false alpha test).
201 @(ex_intro ?? (mk_config ?? tc_false (niltape ?))) %
202 [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
203 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (leftof ? a al)))
204 % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
205 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (rightof ? a al)))
206 % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
207 | #ls #c #rs @(ex_intro ?? 2)
208 cases (true_or_false (test c)) #Htest
209 [ @(ex_intro ?? (mk_config ?? tc_true ?))
212 [ whd in ⊢ (??%?); >tc_q0_q1 //
213 | #_ % // @(ex_intro … c) /2/]
214 | * #Hfalse @False_ind @Hfalse % ]
216 | @(ex_intro ?? (mk_config ?? tc_false (midtape ? ls c rs)))
219 [ whd in ⊢ (??%?); >tc_q0_q2 //
220 | whd in ⊢ ((??%%)→?); #Hfalse destruct (Hfalse) ]
221 | #_ % // #c0 whd in ⊢ ((??%?)→?); #Hc0 destruct (Hc0) //
227 lemma test_char_inv :
228 ∀sig.∀P:tape sig → Prop.∀f,t,t0.P t → Rtc_true sig f t t0 → P t0.
229 #sig #P #f #t #t0 #HPt * #_ //
232 definition test_null ≝ λalpha.test_char alpha (λ_.true).
234 definition R_test_null_true ≝ λalpha,t1,t2.
235 current alpha t1 ≠ None ? ∧ t1 = t2.
237 definition R_test_null_false ≝ λalpha,t1,t2.
238 current alpha t1 = None ? ∧ t1 = t2.
240 lemma sem_test_null : ∀alpha.
241 test_null alpha ⊨ [ tc_true : R_test_null_true alpha, R_test_null_false alpha].
242 #alpha #t1 cases (sem_test_char alpha (λ_.true) t1) #k * #outc * * #Hloop #Htrue
243 #Hfalse %{k} %{outc} % [ %
245 | #Houtc cases (Htrue ?) [| @Houtc] * #c * #Hcurt1 #_ #Houtc1 %
246 [ >Hcurt1 % #H destruct (H) | <Houtc1 % ] ]
247 | #Houtc cases (Hfalse ?) [| @Houtc] #Habsurd #Houtc %
248 [ cases (current alpha t1) in Habsurd; // #c1 #Habsurd
249 lapply (Habsurd ? (refl ??)) #H destruct (H)
253 (************************************* swap ***********************************)
254 definition swap_states : FinSet → FinSet ≝
255 λalpha:FinSet.FinProd (initN 4) alpha.
257 definition swap0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)).
258 definition swap1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
259 definition swap2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
260 definition swap3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
263 λalpha:FinSet.λfoo:alpha.
264 mk_TM alpha (swap_states alpha)
267 let q' ≝ pi1 nat (λi.i<4) q' in
269 [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
272 [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',R〉 (* save in register and move R *)
273 | S q' ⇒ match q' with
274 [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,L〉 (* swap with register and move L *)
275 | S q' ⇒ match q' with
276 [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
277 | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
282 (λq.\fst q == swap3).
287 t1 = midtape alpha ls b [ ] →
288 t2 = rightof ? b ls) ∧
290 t1 = midtape alpha ls b (a::rs) →
291 t2 = midtape alpha ls a (b::rs)).
293 lemma sem_swap_r : ∀alpha,foo.
294 swap_r alpha foo ⊨ Rswap_r alpha.
296 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
297 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
298 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
299 % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
300 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
301 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
302 | #lt #c #rt @(ex_intro ?? 4) cases rt
303 [@ex_intro [|% [ % | %
304 [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
305 |#r0 #rt0 @ex_intro [| % [ % | %
306 [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
312 λalpha:FinSet.λfoo:alpha.
313 mk_TM alpha (swap_states alpha)
316 let q' ≝ pi1 nat (λi.i<4) q' in
318 [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
321 [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',L〉 (* save in register and move L *)
322 | S q' ⇒ match q' with
323 [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,R〉 (* swap with register and move R *)
324 | S q' ⇒ match q' with
325 [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
326 | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
331 (λq.\fst q == swap3).
336 t1 = midtape alpha [ ] b rs →
337 t2 = leftof ? b rs) ∧
339 t1 = midtape alpha (a::ls) b rs →
340 t2 = midtape alpha (b::ls) a rs).
342 lemma sem_swap_l : ∀alpha,foo.
343 swap_l alpha foo ⊨ Rswap_l alpha.
345 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
346 % [% |% [#b #rs | #a #b #ls #rs] #H destruct]
347 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
348 % [% | % [#b #rs | #a #b #ls #rs] #H destruct]
349 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
350 % [% |% [#b #rs | #a #b #ls #rs] #H destruct]
351 | #lt #c #rt @(ex_intro ?? 4) cases lt
352 [@ex_intro [|% [ % | %
353 [#b #rs #H destruct normalize // |#a #b #ls #rs #H destruct]]]
354 |#r0 #rt0 @ex_intro [| % [ % | %
355 [#b #rs #H destruct | #a #b #ls #rs #H destruct normalize //
360 (********************************** combine ***********************************)
361 (* replace the content x of a cell with a combiation f(x,y) of x and the content
362 y of the adiacent cell *)
364 definition combf_states : FinSet → FinSet ≝
365 λalpha:FinSet.FinProd (initN 4) alpha.
367 definition combf0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)).
368 definition combf1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
369 definition combf2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
370 definition combf3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
373 λalpha:FinSet.λf.λfoo:alpha.
374 mk_TM alpha (combf_states alpha)
377 let q' ≝ pi1 nat (λi.i<4) q' in
379 [ None ⇒ 〈〈combf3,foo〉,None ?,N〉 (* if tape is empty then stop *)
382 [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',R〉 (* save in register and move R *)
383 | S q' ⇒ match q' with
384 [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',L〉
385 (* combine in register and move L *)
386 | S q' ⇒ match q' with
387 [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,R〉
388 (* copy from register and move R *)
389 | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
394 (λq.\fst q == combf3).
396 definition Rcombf_r ≝
399 t1 = midtape alpha ls b [ ] →
400 t2 = rightof ? b ls) ∧
402 t1 = midtape alpha ls b (a::rs) →
403 t2 = midtape alpha ((f b a)::ls) a rs).
405 lemma sem_combf_r : ∀alpha,f,foo.
406 combf_r alpha f foo ⊨ Rcombf_r alpha f.
408 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
409 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
410 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
411 % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
412 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
413 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
414 | #lt #c #rt @(ex_intro ?? 4) cases rt
415 [@ex_intro [|% [ % | %
416 [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
417 |#r0 #rt0 @ex_intro [| % [ % | %
418 [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
424 λalpha:FinSet.λf.λfoo:alpha.
425 mk_TM alpha (combf_states alpha)
428 let q' ≝ pi1 nat (λi.i<4) q' in
430 [ None ⇒ 〈〈combf3,foo〉,None ?,N〉 (* if tape is empty then stop *)
433 [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',L〉 (* save in register and move R *)
434 | S q' ⇒ match q' with
435 [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',R〉
436 (* combine in register and move L *)
437 | S q' ⇒ match q' with
438 [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,L〉
439 (* copy from register and move R *)
440 | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
445 (λq.\fst q == combf3).
447 definition Rcombf_l ≝
450 t1 = midtape alpha [ ] b rs →
451 t2 = leftof ? b rs) ∧
453 t1 = midtape alpha (a::ls) b rs →
454 t2 = midtape alpha ls a ((f b a)::rs)).
456 lemma sem_combf_l : ∀alpha,f,foo.
457 combf_l alpha f foo ⊨ Rcombf_l alpha f.
459 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
460 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
461 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
462 % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
463 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
464 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
465 | #lt #c #rt @(ex_intro ?? 4) cases lt
466 [@ex_intro [|% [ % | %
467 [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
468 |#r0 #rt0 @ex_intro [| % [ % | %
469 [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
474 (********************************* new_combine ********************************)
475 (* replace the content x of a cell with a combiation f(x,y) of x and the content
476 y of the adiacent cell; if there is no adjacent cell, combines with a default
479 definition ncombf_r ≝
480 λalpha:FinSet.λf.λfoo:alpha.
481 mk_TM alpha (combf_states alpha)
484 let q' ≝ pi1 nat (λi.i<4) q' in
486 [ None ⇒ if (eqb q' 1)then (* if on right cell, combine in register and move L *)
487 〈〈combf2,f b foo〉,None ?,L〉
488 else 〈〈combf3,foo〉,None ?,N〉 (* else stop *)
491 [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',R〉 (* save in register and move R *)
492 | S q' ⇒ match q' with
493 [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',L〉
494 (* combine in register and move L *)
495 | S q' ⇒ match q' with
496 [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,R〉
497 (* copy from register and move R *)
498 | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
503 (λq.\fst q == combf3).
505 definition Rncombf_r ≝
508 t1 = midtape alpha ls b [ ] →
509 t2 = rightof ? (f b foo) ls) ∧
511 t1 = midtape alpha ls b (a::rs) →
512 t2 = midtape alpha ((f b a)::ls) a rs).
514 lemma sem_ncombf_r : ∀alpha,f,foo.
515 ncombf_r alpha f foo ⊨ Rncombf_r alpha f foo.
517 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
518 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
519 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
520 % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
521 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
522 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
523 | #lt #c #rt @(ex_intro ?? 4) cases rt
524 [@ex_intro [|% [ % | %
525 [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
526 |#r0 #rt0 @ex_intro [| % [ % | %
527 [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
532 definition ncombf_l ≝
533 λalpha:FinSet.λf.λfoo:alpha.
534 mk_TM alpha (combf_states alpha)
537 let q' ≝ pi1 nat (λi.i<4) q' in
539 [ None ⇒ if (eqb q' 1)then
540 (* if on left cell, combine in register and move R *)
541 〈〈combf2,f b foo〉,None ?,R〉
542 else 〈〈combf3,foo〉,None ?,N〉 (* else stop *)
545 [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',L〉 (* save in register and move R *)
546 | S q' ⇒ match q' with
547 [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',R〉
548 (* combine in register and move L *)
549 | S q' ⇒ match q' with
550 [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,L〉
551 (* copy from register and move R *)
552 | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
557 (λq.\fst q == combf3).
559 definition Rncombf_l ≝
562 t1 = midtape alpha [ ] b rs →
563 t2 = leftof ? (f b foo) rs) ∧
565 t1 = midtape alpha (a::ls) b rs →
566 t2 = midtape alpha ls a ((f b a)::rs)).
568 lemma sem_ncombf_l : ∀alpha,f,foo.
569 ncombf_l alpha f foo ⊨ Rncombf_l alpha f foo.
571 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
572 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
573 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
574 % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
575 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
576 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
577 | #lt #c #rt @(ex_intro ?? 4) cases lt
578 [@ex_intro [|% [ % | %
579 [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
580 |#r0 #rt0 @ex_intro [| % [ % | %
581 [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //