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 (***************************** replace a with f a *****************************)
46 definition writef ≝ λalpha,f.
47 mk_TM alpha write_states
50 [ O ⇒ 〈wr1,Some ? (f a),N〉
51 | S _ ⇒ 〈wr1,None ?,N〉 ])
54 definition R_writef ≝ λalpha,f,t1,t2.
55 ∀c. current ? t1 = c →
56 t2 = midtape alpha (left ? t1) (f c) (right ? t1).
58 lemma sem_writef : ∀alpha,f.
59 writef alpha f ⊨ R_writef alpha f.
60 #alpha #f #t @(ex_intro … 2) @ex_intro
61 [|% [% |cases t normalize // ] ]
64 (******************** moves the head one step to the right ********************)
66 definition move_states ≝ initN 2.
67 definition move0 : move_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
68 definition move1 : move_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
71 λalpha:FinSet.mk_TM alpha move_states
74 [ None ⇒ 〈move1,None ?,N〉
75 | Some a' ⇒ match (pi1 … q) with
76 [ O ⇒ 〈move1,Some ? a',R〉
77 | S q ⇒ 〈move1,None ?,N〉 ] ])
78 move0 (λq.q == move1).
80 definition R_move_r ≝ λalpha,t1,t2.
81 (current ? t1 = None ? → t1 = t2) ∧
83 t1 = midtape alpha ls c rs →
84 t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
86 (current ? t1 = None ? ∧ t1 = t2) ∨
88 t1 = midtape alpha ls c rs ∧
89 t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).*)
92 ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
93 #alpha #intape @(ex_intro ?? 2) cases intape
95 [| % [ % | % // #ls #c #rs #H destruct ] ]
97 [| % [ % | % // #ls #c #rs #H destruct ] ]
99 [| % [ % | % // #ls #c #rs #H destruct ] ]
101 @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct]
102 #ls1 #c1 #rs1 #H destruct cases rs1 // ] ] ]
105 (******************** moves the head one step to the left *********************)
108 λalpha:FinSet.mk_TM alpha move_states
111 [ None ⇒ 〈move1,None ?,N〉
112 | Some a' ⇒ match pi1 … q with
113 [ O ⇒ 〈move1,Some ? a',L〉
114 | S q ⇒ 〈move1,None ?,N〉 ] ])
115 move0 (λq.q == move1).
117 definition R_move_l ≝ λalpha,t1,t2.
118 (current ? t1 = None ? → t1 = t2) ∧
120 t1 = midtape alpha ls c rs →
121 t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
124 ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
125 #alpha #intape @(ex_intro ?? 2) cases intape
127 [| % [ % | % // #ls #c #rs #H destruct ] ]
129 [| % [ % | % // #ls #c #rs #H destruct ] ]
131 [| % [ % | % // #ls #c #rs #H destruct ] ]
133 @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct]
134 #ls1 #c1 #rs1 #H destruct cases ls1 // ] ] ]
137 (* a slightly different move machine. *)
138 definition smove_states ≝ initN 2.
140 definition smove0 : smove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
141 definition smove1 : smove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
143 definition trans_smove ≝
145 λp:smove_states × (option sig).
146 let 〈q,a〉 ≝ p in match (pi1 … q) with
147 [ O ⇒ 〈smove1,None sig, D〉
148 | S _ ⇒ 〈smove1,None sig, N〉 ].
151 λsig,D.mk_TM sig smove_states (trans_smove sig D) smove0 (λq.q == smove1).
154 λalpha,D,t1,t2. t2 = tape_move alpha t1 D.
156 lemma sem_move_single :
157 ∀alpha,D.move alpha D ⊨ Rmove alpha D.
158 #alpha #D #int %{2} %{(mk_config ? smove_states smove1 ?)} [| % % ]
161 (********************************* test char **********************************)
163 (* the test_char machine ends up in two different states q1 and q2 wether or not
164 the current character satisfies a boolean test function passed as a parameter to
166 The machine ends up in q1 also in case there is no current character.
169 definition tc_states ≝ initN 3.
171 definition tc_start : tc_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
172 definition tc_true : tc_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
173 definition tc_false : tc_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
175 definition test_char ≝
176 λalpha:FinSet.λtest:alpha→bool.
177 mk_TM alpha tc_states
180 [ None ⇒ 〈tc_false, None ?,N〉
183 [ true ⇒ 〈tc_true,None ?,N〉
184 | false ⇒ 〈tc_false,None ?,N〉 ]])
185 tc_start (λx.notb (x == tc_start)).
187 definition Rtc_true ≝
189 (∃c. current alpha t1 = Some ? c ∧ test c = true) ∧ t2 = t1.
191 definition Rtc_false ≝
193 (∀c. current alpha t1 = Some ? c → test c = false) ∧ t2 = t1.
196 ∀alpha,test,ls,a0,rs. test a0 = true →
197 step alpha (test_char alpha test)
198 (mk_config ?? tc_start (midtape … ls a0 rs)) =
199 mk_config alpha (states ? (test_char alpha test)) tc_true
200 (midtape … ls a0 rs).
201 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
202 whd in match (trans … 〈?,?〉); >Htest %
206 ∀alpha,test,ls,a0,rs. test a0 = false →
207 step alpha (test_char alpha test)
208 (mk_config ?? tc_start (midtape … ls a0 rs)) =
209 mk_config alpha (states ? (test_char alpha test)) tc_false
210 (midtape … ls a0 rs).
211 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
212 whd in match (trans … 〈?,?〉); >Htest %
215 lemma sem_test_char :
217 accRealize alpha (test_char alpha test)
218 tc_true (Rtc_true alpha test) (Rtc_false alpha test).
221 @(ex_intro ?? (mk_config ?? tc_false (niltape ?))) %
222 [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
223 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (leftof ? a al)))
224 % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
225 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (rightof ? a al)))
226 % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
227 | #ls #c #rs @(ex_intro ?? 2)
228 cases (true_or_false (test c)) #Htest
229 [ @(ex_intro ?? (mk_config ?? tc_true ?))
232 [ whd in ⊢ (??%?); >tc_q0_q1 //
233 | #_ % // @(ex_intro … c) /2/]
234 | * #Hfalse @False_ind @Hfalse % ]
236 | @(ex_intro ?? (mk_config ?? tc_false (midtape ? ls c rs)))
239 [ whd in ⊢ (??%?); >tc_q0_q2 //
240 | whd in ⊢ ((??%%)→?); #Hfalse destruct (Hfalse) ]
241 | #_ % // #c0 whd in ⊢ ((??%?)→?); #Hc0 destruct (Hc0) //
247 lemma test_char_inv :
248 ∀sig.∀P:tape sig → Prop.∀f,t,t0.P t → Rtc_true sig f t t0 → P t0.
249 #sig #P #f #t #t0 #HPt * #_ //
252 definition test_null ≝ λalpha.test_char alpha (λ_.true).
254 definition R_test_null_true ≝ λalpha,t1,t2.
255 current alpha t1 ≠ None ? ∧ t1 = t2.
257 definition R_test_null_false ≝ λalpha,t1,t2.
258 current alpha t1 = None ? ∧ t1 = t2.
260 lemma sem_test_null : ∀alpha.
261 test_null alpha ⊨ [ tc_true : R_test_null_true alpha, R_test_null_false alpha].
262 #alpha #t1 cases (sem_test_char alpha (λ_.true) t1) #k * #outc * * #Hloop #Htrue
263 #Hfalse %{k} %{outc} % [ %
265 | #Houtc cases (Htrue ?) [| @Houtc] * #c * #Hcurt1 #_ #Houtc1 %
266 [ >Hcurt1 % #H destruct (H) | <Houtc1 % ] ]
267 | #Houtc cases (Hfalse ?) [| @Houtc] #Habsurd #Houtc %
268 [ cases (current alpha t1) in Habsurd; // #c1 #Habsurd
269 lapply (Habsurd ? (refl ??)) #H destruct (H)
273 (************************************* swap ***********************************)
274 definition swap_states : FinSet → FinSet ≝
275 λalpha:FinSet.FinProd (initN 4) alpha.
277 definition swap0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)).
278 definition swap1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
279 definition swap2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
280 definition swap3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
283 λalpha:FinSet.λfoo:alpha.
284 mk_TM alpha (swap_states alpha)
287 let q' ≝ pi1 nat (λi.i<4) q' in
289 [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
292 [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',R〉 (* save in register and move R *)
293 | S q' ⇒ match q' with
294 [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,L〉 (* swap with register and move L *)
295 | S q' ⇒ match q' with
296 [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
297 | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
302 (λq.\fst q == swap3).
307 t1 = midtape alpha ls b [ ] →
308 t2 = rightof ? b ls) ∧
310 t1 = midtape alpha ls b (a::rs) →
311 t2 = midtape alpha ls a (b::rs)).
313 lemma sem_swap_r : ∀alpha,foo.
314 swap_r alpha foo ⊨ Rswap_r alpha.
316 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
317 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
318 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
319 % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
320 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
321 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
322 | #lt #c #rt @(ex_intro ?? 4) cases rt
323 [@ex_intro [|% [ % | %
324 [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
325 |#r0 #rt0 @ex_intro [| % [ % | %
326 [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
332 λalpha:FinSet.λfoo:alpha.
333 mk_TM alpha (swap_states alpha)
336 let q' ≝ pi1 nat (λi.i<4) q' in
338 [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
341 [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',L〉 (* save in register and move L *)
342 | S q' ⇒ match q' with
343 [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,R〉 (* swap with register and move R *)
344 | S q' ⇒ match q' with
345 [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
346 | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
351 (λq.\fst q == swap3).
356 t1 = midtape alpha [ ] b rs →
357 t2 = leftof ? b rs) ∧
359 t1 = midtape alpha (a::ls) b rs →
360 t2 = midtape alpha (b::ls) a rs).
362 lemma sem_swap_l : ∀alpha,foo.
363 swap_l alpha foo ⊨ Rswap_l alpha.
365 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
366 % [% |% [#b #rs | #a #b #ls #rs] #H destruct]
367 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
368 % [% | % [#b #rs | #a #b #ls #rs] #H destruct]
369 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
370 % [% |% [#b #rs | #a #b #ls #rs] #H destruct]
371 | #lt #c #rt @(ex_intro ?? 4) cases lt
372 [@ex_intro [|% [ % | %
373 [#b #rs #H destruct normalize // |#a #b #ls #rs #H destruct]]]
374 |#r0 #rt0 @ex_intro [| % [ % | %
375 [#b #rs #H destruct | #a #b #ls #rs #H destruct normalize //
380 (********************************** combine ***********************************)
381 (* replace the content x of a cell with a combiation f(x,y) of x and the content
382 y of the adiacent cell *)
384 definition combf_states : FinSet → FinSet ≝
385 λalpha:FinSet.FinProd (initN 4) alpha.
387 definition combf0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)).
388 definition combf1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
389 definition combf2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
390 definition combf3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
393 λalpha:FinSet.λf.λfoo:alpha.
394 mk_TM alpha (combf_states alpha)
397 let q' ≝ pi1 nat (λi.i<4) q' in
399 [ None ⇒ 〈〈combf3,foo〉,None ?,N〉 (* if tape is empty then stop *)
402 [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',R〉 (* save in register and move R *)
403 | S q' ⇒ match q' with
404 [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',L〉
405 (* combine in register and move L *)
406 | S q' ⇒ match q' with
407 [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,R〉
408 (* copy from register and move R *)
409 | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
414 (λq.\fst q == combf3).
416 definition Rcombf_r ≝
419 t1 = midtape alpha ls b [ ] →
420 t2 = rightof ? b ls) ∧
422 t1 = midtape alpha ls b (a::rs) →
423 t2 = midtape alpha ((f b a)::ls) a rs).
425 lemma sem_combf_r : ∀alpha,f,foo.
426 combf_r alpha f foo ⊨ Rcombf_r alpha f.
428 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
429 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
430 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
431 % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
432 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
433 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
434 | #lt #c #rt @(ex_intro ?? 4) cases rt
435 [@ex_intro [|% [ % | %
436 [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
437 |#r0 #rt0 @ex_intro [| % [ % | %
438 [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
444 λalpha:FinSet.λf.λfoo:alpha.
445 mk_TM alpha (combf_states alpha)
448 let q' ≝ pi1 nat (λi.i<4) q' in
450 [ None ⇒ 〈〈combf3,foo〉,None ?,N〉 (* if tape is empty then stop *)
453 [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',L〉 (* save in register and move R *)
454 | S q' ⇒ match q' with
455 [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',R〉
456 (* combine in register and move L *)
457 | S q' ⇒ match q' with
458 [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,L〉
459 (* copy from register and move R *)
460 | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
465 (λq.\fst q == combf3).
467 definition Rcombf_l ≝
470 t1 = midtape alpha [ ] b rs →
471 t2 = leftof ? b rs) ∧
473 t1 = midtape alpha (a::ls) b rs →
474 t2 = midtape alpha ls a ((f b a)::rs)).
476 lemma sem_combf_l : ∀alpha,f,foo.
477 combf_l alpha f foo ⊨ Rcombf_l alpha f.
479 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
480 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
481 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
482 % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
483 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
484 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
485 | #lt #c #rt @(ex_intro ?? 4) cases lt
486 [@ex_intro [|% [ % | %
487 [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
488 |#r0 #rt0 @ex_intro [| % [ % | %
489 [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
494 (********************************* new_combine ********************************)
495 (* replace the content x of a cell with a combiation f(x,y) of x and the content
496 y of the adiacent cell; if there is no adjacent cell, combines with a default
499 definition ncombf_r ≝
500 λalpha:FinSet.λf.λfoo:alpha.
501 mk_TM alpha (combf_states alpha)
504 let q' ≝ pi1 nat (λi.i<4) q' in
506 [ None ⇒ if (eqb q' 1)then (* if on right cell, combine in register and move L *)
507 〈〈combf2,f b foo〉,None ?,L〉
508 else 〈〈combf3,foo〉,None ?,N〉 (* else stop *)
511 [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',R〉 (* save in register and move R *)
512 | S q' ⇒ match q' with
513 [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',L〉
514 (* combine in register and move L *)
515 | S q' ⇒ match q' with
516 [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,R〉
517 (* copy from register and move R *)
518 | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
523 (λq.\fst q == combf3).
525 definition Rncombf_r ≝
528 t1 = midtape alpha ls b [ ] →
529 t2 = rightof ? (f b foo) ls) ∧
531 t1 = midtape alpha ls b (a::rs) →
532 t2 = midtape alpha ((f b a)::ls) a rs).
534 lemma sem_ncombf_r : ∀alpha,f,foo.
535 ncombf_r alpha f foo ⊨ Rncombf_r alpha f foo.
537 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
538 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
539 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
540 % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
541 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
542 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
543 | #lt #c #rt @(ex_intro ?? 4) cases rt
544 [@ex_intro [|% [ % | %
545 [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
546 |#r0 #rt0 @ex_intro [| % [ % | %
547 [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
552 definition ncombf_l ≝
553 λalpha:FinSet.λf.λfoo:alpha.
554 mk_TM alpha (combf_states alpha)
557 let q' ≝ pi1 nat (λi.i<4) q' in
559 [ None ⇒ if (eqb q' 1)then
560 (* if on left cell, combine in register and move R *)
561 〈〈combf2,f b foo〉,None ?,R〉
562 else 〈〈combf3,foo〉,None ?,N〉 (* else stop *)
565 [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',L〉 (* save in register and move R *)
566 | S q' ⇒ match q' with
567 [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',R〉
568 (* combine in register and move L *)
569 | S q' ⇒ match q' with
570 [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,L〉
571 (* copy from register and move R *)
572 | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
577 (λq.\fst q == combf3).
579 definition Rncombf_l ≝
582 t1 = midtape alpha [ ] b rs →
583 t2 = leftof ? (f b foo) rs) ∧
585 t1 = midtape alpha (a::ls) b rs →
586 t2 = midtape alpha ls a ((f b a)::rs)).
588 lemma sem_ncombf_l : ∀alpha,f,foo.
589 ncombf_l alpha f foo ⊨ Rncombf_l alpha f foo.
591 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
592 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
593 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
594 % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
595 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
596 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
597 | #lt #c #rt @(ex_intro ?? 4) cases lt
598 [@ex_intro [|% [ % | %
599 [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
600 |#r0 #rt0 @ex_intro [| % [ % | %
601 [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //