]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/universal/uni_step.ma
Progress.
[helm.git] / matita / matita / lib / turing / universal / uni_step.ma
1 (*
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.           
5     ||I||                                                            
6     ||T||  
7     ||A||  
8     \   /  This file is distributed under the terms of the       
9      \ /   GNU General Public License Version 2   
10       V_____________________________________________________________*)
11
12
13 (* COMPARE BIT
14
15 *)
16
17 include "turing/universal/copy.ma".
18 include "turing/universal/move_tape.ma".
19
20 (*
21
22 step :
23
24 if is_true(current) (* current state is final *)
25    then nop
26    else 
27    (* init_match *)
28    mark;
29    adv_to_grid_r;
30    move_r;
31    mark;
32    move_l;
33    adv_to_mark_l
34    (* /init_match *)
35    match_tuple;
36    if is_marked(current) = false (* match ok *)
37       then 
38            (* init_copy *)
39            move_l;
40            init_current;
41            move_r;
42            adv_to_mark_r;
43            adv_mark_r;
44            (* /init_copy *)
45            copy;
46            move_r;
47            (* move_tape *)
48            by cases on current: 
49              case bit false: move_tape_l
50              case bit true: move_tape_r
51              case null: adv_to_grid_l; move_l; adv_to_grid_l;
52            move_r;
53            (* /move_tape *)
54       else sink;
55         
56 *)
57
58 definition init_match ≝ 
59   seq ? (mark ?) 
60     (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c)))
61       (seq ? (move_r ?) 
62         (seq ? (move_r ?)
63           (seq ? (mark ?)
64             (seq ? (move_l ?) 
65               (adv_to_mark_l ? (is_marked ?))))))).
66              
67 definition R_init_match ≝ λt1,t2.
68   ∀ls,l,rs,c,d. no_grids (〈c,false〉::l) → no_marks l → 
69   t1 = midtape STape ls 〈c,false〉 (l@〈grid,false〉::〈bar,false〉::〈d,false〉::rs) →
70   t2 = midtape STape ls 〈c,true〉 (l@〈grid,false〉::〈bar,false〉::〈d,true〉::rs).
71   
72 lemma sem_init_match : Realize ? init_match R_init_match.
73 #intape 
74 cases (sem_seq ????? (sem_mark ?)
75        (sem_seq ????? (sem_adv_to_mark_r ? (λc:STape.is_grid (\fst c)))
76         (sem_seq ????? (sem_move_r ?)
77          (sem_seq ????? (sem_move_r ?)
78           (sem_seq ????? (sem_mark ?)
79            (sem_seq ????? (sem_move_l ?)
80             (sem_adv_to_mark_l ? (is_marked ?))))))) intape)
81 #k * #outc * #Hloop #HR 
82 @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
83 #ls #l #rs #c #d #Hnogrids #Hnomarks #Hintape
84 cases HR -HR
85 #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta -Hintape #Hta
86 * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Htb -Hta 
87   [* #Hgridc @False_ind @(absurd … Hgridc) @eqnot_to_noteq 
88    @(Hnogrids 〈c,false〉) @memb_hd ]
89 * #Hgrdic #Htb lapply (Htb l 〈grid,false〉 (〈bar,false〉::〈d,false〉::rs) (refl …) (refl …) ?) 
90   [#x #membl @Hnogrids @memb_cons @membl] -Htb #Htb
91 * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb #Htc
92 * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd -Htc #Htd
93 * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Hte -Htd #Hte
94 * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf -Hte #Htf
95 whd in ⊢ (%→?); #Htg cases (Htg … Htf) -Htg -Htf
96   [* whd in ⊢ ((??%?)→?); #Habs destruct (Habs)]
97 * #_ #Htg lapply (Htg (〈grid,false〉::reverse ? l) 〈c,true〉 ls (refl …) (refl …) ?) 
98   [#x #membl @Hnomarks @daemon] -Htg #Htg >Htg >reverse_cons >reverse_reverse
99    >associative_append %
100 qed.
101
102
103 (* init_copy 
104
105            init_current_on_match; (* no marks in current *)
106            move_r;
107            adv_to_mark_r;
108            adv_mark_r;
109
110 *)
111
112 definition init_copy ≝ 
113   seq ? init_current_on_match
114     (seq ? (move_r ?) 
115       (seq ? (adv_to_mark_r ? (is_marked ?))
116         (adv_mark_r ?))).
117
118 definition R_init_copy ≝ λt1,t2.
119   ∀l1,l2,c,ls,d,rs. 
120   no_marks l1 → no_grids l1 → 
121   no_marks l2 → is_grid c = false → 
122   t1 = midtape STape (l1@〈c,false〉::〈grid,false〉::ls) 〈grid,false〉 (l2@〈comma,true〉::〈d,false〉::rs) → 
123   t2 = midtape STape (〈comma,false〉::(reverse ? l2)@〈grid,false〉::l1@〈c,true〉::〈grid,false〉::ls) 〈d,true〉 rs.
124
125 lemma list_last: ∀A.∀l:list A.
126   l = [ ] ∨ ∃a,l1. l = l1@[a].
127 #A #l <(reverse_reverse ? l) cases (reverse A l)
128   [%1 //
129   |#a #l1 %2 @(ex_intro ?? a) @(ex_intro ?? (reverse ? l1)) //
130   ]
131 qed.
132    
133 lemma sem_init_copy : Realize ? init_copy R_init_copy.
134 #intape 
135 cases (sem_seq ????? sem_init_current_on_match
136         (sem_seq ????? (sem_move_r ?)
137           (sem_seq ????? (sem_adv_to_mark_r ? (is_marked ?))
138             (sem_adv_mark_r ?))) intape)
139 #k * #outc * #Hloop #HR 
140 @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
141 #l1 #l2 #c #ls #d #rs #Hl1marks #Hl1grids #Hl2marks #Hc #Hintape
142 cases HR -HR
143 #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hl1grids Hc Hintape) -Hta -Hintape #Hta
144 * #tb * whd in ⊢ (%→?); #Htb lapply (Htb  … Hta) -Htb -Hta
145 generalize in match Hl1marks; -Hl1marks cases (list_last ? l1) 
146   [#eql1 >eql1 #Hl1marks whd in ⊢ ((???%)→?); whd in ⊢ ((???(????%))→?); #Htb
147    * #tc * whd in ⊢ (%→?); #Htc lapply (Htc  … Htb) -Htc -Htb *
148     [* whd in ⊢ ((??%?)→?); #Htemp destruct (Htemp)]
149    * #_ #Htc lapply (Htc … (refl …) (refl …) ?)
150     [#x #membx @Hl2marks @membx]
151    #Htc whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc) -Houtc -Htc #Houtc
152    >Houtc %
153   |* #c1 * #tl #eql1 >eql1 #Hl1marks >reverse_append >reverse_single 
154    whd in ⊢ ((???%)→?); whd in ⊢ ((???(????%))→?);
155    >associative_append whd in ⊢ ((???(????%))→?); #Htb
156    * #tc * whd in ⊢ (%→?); #Htc lapply (Htc  … Htb) -Htc -Htb *
157     [* >Hl1marks [#Htemp destruct (Htemp)] @memb_append_l2 @memb_hd]
158    * #_ >append_cons <associative_append #Htc lapply (Htc … (refl …) (refl …) ?)
159     [#x #membx cases (memb_append … membx) -membx #membx
160       [cases (memb_append … membx) -membx #membx
161         [@Hl1marks @memb_append_l1 @daemon
162         |>(memb_single … membx) %
163         ]
164       |@Hl2marks @membx
165       ]]
166   #Htc whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc) -Houtc -Htc #Houtc
167   >Houtc >reverse_append >reverse_append >reverse_single 
168   >reverse_reverse >associative_append >associative_append 
169   >associative_append %
170 qed.
171   
172 (* OLD 
173 definition init_copy ≝ 
174   seq ? (adv_mark_r ?) 
175     (seq ? init_current_on_match
176       (seq ? (move_r ?) 
177         (adv_to_mark_r ? (is_marked ?)))).
178
179 definition R_init_copy ≝ λt1,t2.
180   ∀l1,l2,c,l3,d,rs. 
181   no_marks l1 → no_grids l1 → 
182   no_marks l2 → no_grids l2 → is_grid c = false → is_grid d =false →
183   t1 = midtape STape (l1@〈grid,false〉::l2@〈c,false〉::〈grid,false〉::l3) 〈comma,true〉 (〈d,false〉::rs) → 
184   t2 = midtape STape (〈comma,false〉::l1@〈grid,false〉::l2@〈c,true〉::〈grid,false〉::l3) 〈d,true〉 rs.
185
186 lemma list_last: ∀A.∀l:list A.
187   l = [ ] ∨ ∃a,l1. l = l1@[a].
188 #A #l <(reverse_reverse ? l) cases (reverse A l)
189   [%1 //
190   |#a #l1 %2 @(ex_intro ?? a) @(ex_intro ?? (reverse ? l1)) //
191   ]
192 qed.
193    
194 lemma sem_init_copy : Realize ? init_copy R_init_copy.
195 #intape 
196 cases (sem_seq ????? (sem_adv_mark_r ?)
197        (sem_seq ????? sem_init_current_on_match
198         (sem_seq ????? (sem_move_r ?)
199          (sem_adv_to_mark_r ? (is_marked ?)))) intape)
200 #k * #outc * #Hloop #HR 
201 @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
202 #l1 #l2 #c #l3 #d #rs #Hl1marks #Hl1grids #Hl2marks #Hl2grids #Hc #Hd #Hintape
203 cases HR -HR
204 #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta -Hintape #Hta
205 * #tb * whd in ⊢ (%→?); 
206 >append_cons #Htb lapply (Htb (〈comma,false〉::l1) l2 c … Hta) 
207   [@Hd |@Hc |@Hl2grids 
208    |#x #membx cases (orb_true_l … membx) -membx #membx 
209      [>(\P membx) // | @Hl1grids @membx]
210   ] -Htb #Htb
211 * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb
212 >reverse_append >reverse_cons cases (list_last ? l2)
213   [#Hl2 >Hl2 >associative_append whd in ⊢ ((???(??%%%))→?); #Htc
214    whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd -Htc
215     [* whd in ⊢ ((??%?)→?); #Habs destruct (Habs)]
216    * #_ #Htf lapply (Htf … (refl …) (refl …) ?) 
217     [#x >reverse_cons #membx cases (memb_append … membx) -membx #membx
218       [@Hl1marks @daemon |>(memb_single … membx) //] 
219     -Htf
220     |#Htf >Htf >reverse_reverse >associative_append %
221     ]
222   |* #a * #l21 #Heq >Heq >reverse_append >reverse_single 
223    >associative_append >associative_append >associative_append whd in ⊢ ((???(??%%%))→?); #Htc
224    whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd -Htc
225     [* >Hl2marks [#Habs destruct (Habs) |>Heq @memb_append_l2 @memb_hd]]
226    * #_ <associative_append <associative_append #Htf lapply (Htf … (refl …) (refl …) ?) 
227     [#x >reverse_cons #membx cases (memb_append … membx) -membx #membx
228       [cases (memb_append … membx) -membx #membx
229         [@Hl2marks >Heq @memb_append_l1 @daemon
230         |>(memb_single … membx) //]
231       |cases (memb_append … membx) -membx #membx
232         [@Hl1marks @daemon |>(memb_single … membx) //]
233       ]
234     | #Htf >Htf >reverse_append >reverse_reverse
235       >reverse_append >reverse_reverse >associative_append 
236       >reverse_single >associative_append >associative_append 
237       >associative_append % 
238     ]
239   ]
240 qed. *)
241
242 definition exec_move ≝ 
243   seq ? init_copy
244     (seq ? copy
245       (seq ? (move_r …) move_tape)).
246
247 definition map_move ≝ 
248   λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ].
249
250 (* - aggiungere a legal_tape le condizioni
251        only_bits ls, rs; bit_or_null c
252    - ci vuole un lemma che dimostri 
253        bit_or_null c1 = true    bit_or_null mv = true
254        mv ≠ null → c1 ≠ null
255      dal fatto che c1 e mv sono contenuti nella table
256  *)
257 definition R_exec_move ≝ λt1,t2.
258   ∀n,curconfig,ls,rs,c0,c1,s0,s1,table1,newconfig,mv,table2.
259   table_TM n (table1@〈comma,false〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2) → 
260   no_marks curconfig → only_bits (curconfig@[〈s0,false〉]) → 
261   only_bits (〈s1,false〉::newconfig) → bit_or_null c1 = true → 
262   |curconfig| = |newconfig| → 
263   legal_tape ls 〈c0,false〉 rs →
264   t1 = midtape STape (〈c0,false〉::curconfig@〈s0,false〉::〈grid,false〉::ls) 〈grid,false〉 
265     (table1@〈comma,true〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) → 
266   ∀t1'.t1' = lift_tape ls 〈c0,false〉 rs → 
267   ∃ls1,rs1,c2.
268   t2 = midtape STape ls1 〈grid,false〉 
269     (〈s1,false〉::newconfig@〈c2,false〉::〈grid,false〉::
270      table1@〈comma,false〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs1) ∧   
271   lift_tape ls1 〈c2,false〉 rs1 = 
272   tape_move STape t1' (map_move c1 mv) ∧ legal_tape ls1 〈c2,false〉 rs1.
273   
274 (* move the following 2 lemmata to mono.ma *)
275 lemma tape_move_left_eq :
276   ∀A.∀t:tape A.∀c.
277   tape_move ? t (Some ? 〈c,L〉) = 
278   tape_move_left ? (left ? t) c (right ? t).
279 //
280 qed.
281
282 lemma tape_move_right_eq :
283   ∀A.∀t:tape A.∀c.
284   tape_move ? t (Some ? 〈c,R〉) = 
285   tape_move_right ? (left ? t) c (right ? t).
286 //
287 qed.
288
289 lemma lift_tape_not_null : 
290  ∀ls,c,bc,rs.c ≠ null → lift_tape ls 〈c,bc〉 rs = midtape ? ls 〈c,bc〉 rs.
291 #ls #c #bc #rs cases c //
292 #Hfalse @False_ind /2/
293 qed.
294
295 lemma merge_char_not_null :
296   ∀c1,c2.c1 ≠ null → merge_char c1 c2 ≠ null.
297 #c1 #c2 @not_to_not cases c2
298 [ #c1' normalize #Hfalse destruct (Hfalse)
299 | normalize //
300 | *: normalize #Hfalse destruct (Hfalse)
301 ]
302 qed.
303
304 lemma merge_char_null : ∀c.merge_char null c = c.
305 * //
306 qed.
307
308 lemma merge_char_cases : ∀c1,c2.merge_char c1 c2 = c1 ∨ merge_char c1 c2 = c2.
309 #c1 *
310 [ #c1' %2 %
311 | % %
312 | *: %2 % ]
313 qed.
314
315 (* lemma merge_char_c_bit :
316   ∀c1,c2.is_bit c2 = true → merge_char c1 c2 = c2.
317 #c1 *
318 [ #c2' #_ %
319 |*: normalize #Hfalse destruct (Hfalse) ]
320 qed.
321
322 lemma merge_char_c_bit :
323   ∀c1,c2.is_null c2 = true → merge_char c1 c2 = c1.
324 #c1 *
325 [ #c2' #_ %
326 |*: normalize #Hfalse destruct (Hfalse) ]
327 qed.
328
329 *)
330
331 lemma sem_exec_move : Realize ? exec_move R_exec_move.
332 #intape
333 cases (sem_seq … sem_init_copy
334         (sem_seq … sem_copy
335           (sem_seq … (sem_move_r …) sem_move_tape )) intape)
336 #k * #outc * #Hloop #HR
337 @(ex_intro ?? k) @(ex_intro ?? outc) % [ @Hloop ] -Hloop
338 #n #curconfig #ls #rs #c0 #c1 #s0 #s1 #table1 #newconfig #mv #table2
339 #Htable #Hcurconfig1 #Hcurconfig2 #Hnewconfig #Hc1 #Hlen #Htape #Hintape #t1' #Ht1'
340 cases HR -HR #ta * whd in ⊢ (%→?); #Hta
341 lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1
342         (newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) … Hintape) -Hta
343 [ (*Hcurconfig2*) @daemon
344 | (*Htable*) @daemon
345 | (*bit_or_null c0 = true *) @daemon
346 | (*Hcurconfig1*) @daemon
347 | #Hta * #tb * whd in ⊢ (%→?); #Htb
348   lapply (Htb (〈grid,false〉::ls) s0 s1 c0 c1 (〈mv,false〉::table2@〈grid,false〉::rs) newconfig (〈comma,false〉::reverse ? table1) curconfig Hta ????????) -Htb
349   [9:|*:(* bit_or_null c0,c1; |curconfig| = |newconfig|*) @daemon ]
350   #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc whd in ⊢(???(??%%%)→?);#Htc
351   whd in ⊢ (%→?); #Houtc whd in Htc:(???%); whd in Htc:(???(??%%%));
352   lapply (Houtc rs n 
353     (〈comma,false〉::〈c1,false〉::reverse ? newconfig@〈s1,false〉::〈comma,false〉::reverse ? table1)
354     mv table2 (merge_char c0 c1) (reverse ? newconfig@[〈s1,false〉]) ls ????????)
355   [3: cases Htape -Htape * * #Hnomarks #Hbits #Hc0 #Hlsrs % [ % [ %
356     [ #x #Hx cases (orb_true_l … Hx) #Hx'
357       [ >(\P Hx') %
358       | @Hnomarks @memb_cons // ]
359     | @Hbits ]
360     | cases (merge_char_cases c0 c1) #Hmerge >Hmerge // ]
361     | cases (true_or_false (c0 == null)) #Hc0'
362       [ cases Hlsrs -Hlsrs 
363         [ *
364           [ >(\P Hc0') * #Hfalse @False_ind /2/
365           | #Hlsnil % %2 // ]
366         | #Hrsnil %2 // ] 
367       | % % @merge_char_not_null @(\Pf Hc0') ] ]
368   |4:>Htc @(eq_f3 … (midtape ?))
369     [ @eq_f @eq_f >associative_append >associative_append %
370     | %
371     | % ]
372   | %
373   || >reverse_cons >reverse_cons >reverse_append >reverse_reverse 
374      >reverse_cons >reverse_cons >reverse_reverse
375      >associative_append >associative_append >associative_append
376      >associative_append >associative_append
377      @Htable
378   | (* well formedness of table *) @daemon
379   | (* Hnewconfig *) @daemon
380   | (* bit_or_null mv = true (well formedness of table) *) @daemon
381   | -Houtc * #ls1 * #rs1 * #newc * #Hnewtapelegal * #Houtc *
382     [ *
383       [ * #Hmv #Htapemove
384         @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc)
385         %
386         [ %
387           [ >Houtc -Houtc >reverse_append
388             >reverse_reverse >reverse_single @eq_f
389             >reverse_cons >reverse_cons >reverse_append >reverse_cons
390             >reverse_cons >reverse_reverse >reverse_reverse
391             >associative_append >associative_append
392             >associative_append >associative_append
393             >associative_append >associative_append %
394           | >Hmv >Ht1' >Htapemove 
395             (* mv = bit false -→ c1 = bit ? *)
396             cut (∃c1'.c1 = bit c1') [ @daemon ] * #c1' #Hc1
397             >Hc1 >tape_move_left_eq >(legal_tape_left … Htape) 
398             >(legal_tape_right … Htape) %
399           ]
400         | //
401         ]
402       | * #Hmv #Htapemove 
403         @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) %
404         [ %
405           [ >Houtc -Houtc >reverse_append
406             >reverse_reverse >reverse_single @eq_f
407             >reverse_cons >reverse_cons >reverse_append >reverse_cons
408             >reverse_cons >reverse_reverse >reverse_reverse
409             >associative_append >associative_append
410             >associative_append >associative_append
411             >associative_append >associative_append %
412           |>Hmv >Ht1' >Htapemove 
413             cut (∃c1'.c1 = bit c1') [ @daemon ] * #c1' #Hc1
414             >Hc1 >tape_move_right_eq >(legal_tape_left … Htape) 
415             >(legal_tape_right … Htape) %
416           ]
417         | //
418         ]
419       ]
420     | * * * #Hmv #Hlseq #Hrseq #Hnewc 
421       @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) %
422       [ %
423         [ >Houtc -Houtc >reverse_append
424           >reverse_reverse >reverse_single @eq_f
425           >reverse_cons >reverse_cons >reverse_append >reverse_cons
426           >reverse_cons >reverse_reverse >reverse_reverse
427           >associative_append >associative_append
428           >associative_append >associative_append
429           >associative_append >associative_append %
430         |>Hmv >Ht1' cases c1 in Hnewc;
431           [ #c1' whd in ⊢ (??%?→?);#Hnewc <Hnewc
432             >Hlseq >Hrseq whd in ⊢ (??%%);
433             >(legal_tape_left … Htape) >(legal_tape_right … Htape) %
434           | whd in ⊢ (??%?→?); #Hnewc >Hnewc >Hlseq >Hrseq %
435           |*: whd in ⊢ (??%?→?);#Hnewc <Hnewc
436             >Hlseq >Hrseq whd in ⊢ (??%%);
437             >(legal_tape_left … Htape) >(legal_tape_right … Htape) %
438           ]
439         ]
440       | //
441       ]
442     ]
443   ]
444 ]
445 qed.
446
447 (*
448 if is_false(current) (* current state is not final *)
449    then init_match;
450     match_tuple;
451     if is_marked(current) = false (* match ok *)
452       then 
453            exec_move
454            move_r;
455       else sink;
456    else nop;
457 *)
458
459 definition uni_step ≝ 
460   ifTM ? (test_char STape (λc.\fst c == bit false))
461     (single_finalTM ? (seq ? init_match
462       (seq ? match_tuple
463         (ifTM ? (test_char ? (λc.¬is_marked ? c))
464           (seq ? exec_move (move_r …))
465           (nop ?) (* sink *)
466           tc_true))))
467     (nop ?)
468     tc_true.
469
470 definition R_uni_step_true ≝ λt1,t2.
471   ∀n,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
472   0 < |table| → table_TM (S n) table → 
473   match_in_table (S n) (〈s0,false〉::curconfig) 〈c0,false〉
474     (〈s1,false〉::newconfig) 〈c1,false〉 〈mv,false〉 table → 
475   legal_tape ls 〈c0,false〉 rs → 
476   t1 = midtape STape (〈grid,false〉::ls) 〈s0,false〉 
477     (curconfig@〈c0,false〉::〈grid,false〉::table@〈grid,false〉::rs) → 
478   ∀t1'.t1' = lift_tape ls 〈c0,false〉 rs → 
479   s0 = bit false ∧
480   ∃ls1,rs1,c2.
481   (t2 = midtape STape (〈grid,false〉::ls1) 〈s1,false〉 
482     (newconfig@〈c2,false〉::〈grid,false〉::table@〈grid,false〉::rs1) ∧
483    lift_tape ls1 〈c2,false〉 rs1 = 
484    tape_move STape t1' (map_move c1 mv) ∧ legal_tape ls1 〈c2,false〉 rs1).
485    
486 definition R_uni_step_false ≝ λt1,t2.
487   ∀b. current STape t1 = Some ? 〈bit b,false〉 → b = true ∧ t2 = t1.
488   
489 axiom sem_match_tuple : Realize ? match_tuple R_match_tuple.
490
491 lemma sem_uni_step :
492   accRealize ? uni_step (inr … (inl … (inr … start_nop)))
493      R_uni_step_true R_uni_step_false. 
494 @(acc_sem_if_app STape … (sem_test_char ? (λc:STape.\fst c == bit false))
495    (sem_seq … sem_init_match      
496      (sem_seq … sem_match_tuple        
497        (sem_if … (* ????????? (sem_test_char …  (λc.¬is_marked FSUnialpha c)) *)
498           (sem_seq … sem_exec_move (sem_move_r …))
499           (sem_nop …))))
500    (sem_nop …)
501    …)
502 [@sem_test_char||]
503 [ #intape #outtape 
504   #ta whd in ⊢ (%→?); #Hta #HR
505   #n #fulltable #s0 #s1 #c0 #c1 #ls #rs #curconfig #newconfig #mv
506   #Htable_len cut (∃t0,table. fulltable =〈bar,false〉::〈t0,false〉::table) [(* 0 < |table| *) @daemon]
507   * #t0 * #table #Hfulltable >Hfulltable -fulltable 
508   #Htable #Hmatch #Htape #Hintape #t1' #Ht1'
509   >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta 
510   #Hs0 lapply (\P Hs0) -Hs0 #Hs0 #Hta % //
511   cases HR -HR 
512   #tb * whd in ⊢ (%→?); #Htb
513   lapply (Htb (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) (table@〈grid,false〉::rs) s0 t0 ???)
514   [ >Hta >associative_append %
515   | @daemon
516   | @daemon
517   | -Hta -Htb #Htb * 
518     #tc * whd in ⊢ (%→?); #Htc cases (Htc … Htable … Htb) -Htb -Htc
519     [| * #Hcurrent #Hfalse @False_ind
520       (* absurd by Hmatch *) @daemon
521     | >Hs0 %
522     | (* Htable (con lemma) *) @daemon
523     | (* Hmatch *) @daemon
524     | (* Htable *) @daemon
525     | (* Htable, Hmatch → |config| = n 
526        necessaria modifica in R_match_tuple, le dimensioni non corrispondono
527       *) @daemon
528     ]
529     * #table1 * #newc * #mv1 * #table2 * #Htableeq #Htc *
530     [ * #td * whd in ⊢ (%→?); >Htc -Htc #Htd
531       cases (Htd ? (refl ??)) #_ -Htd
532       cut (newc = 〈s1,false〉::newconfig@[〈c1,false〉]) [@daemon] #Hnewc
533       >Hnewc #Htd cut (mv1 = 〈mv,false〉)
534       [@daemon] #Hmv1
535       * #te * whd in ⊢ (%→?); #Hte
536       cut (td = midtape STape (〈c0,false〉::reverse STape curconfig@〈s0,false〉::〈grid,false〉::ls) 
537               〈grid,false〉
538               ((table1@〈bar,false〉::〈s0,false〉::curconfig@[〈c0,false〉])@〈comma,true〉::〈s1,false〉::
539                newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs))
540       [ >Htd @eq_f3 //
541         [ >reverse_append >reverse_single %
542         | >associative_append >associative_append normalize
543           >associative_append >associative_append >Hmv1 % 
544         ]
545       ]
546       -Htd #Htd lapply (Hte … (S n) … Htd … Ht1') -Htd -Hte
547       [ //
548       | (*|curconfig| = |newconfig|*) @daemon
549       | (* Htable → bit_or_null c1 = true *) @daemon
550       | (* only_bits (〈s1,false〉::newconfig) *) @daemon
551       | (* only_bits (curconfig@[〈s0,false〉]) *) @daemon
552       | (* no_marks (reverse ? curconfig) *) @daemon
553       | >Hmv1 in Htableeq; >Hnewc 
554         >associative_append >associative_append normalize
555         >associative_append >associative_append
556         #Htableeq <Htableeq // ]
557       * #ls1 * #rs1 * #c2 * * #Hte #Hliftte #Hlegalte
558       whd in ⊢ (%→?); #Houttape lapply (Houttape … Hte) -Houttape #Houttape
559       whd in Houttape:(???%); whd in Houttape:(???(??%%%));
560       @ex_intro [| @(ex_intro ?? rs1) @ex_intro [| % [ % 
561       [ >Houttape @eq_f @eq_f @eq_f @eq_f
562         change with ((〈bar,false〉::〈t0,false〉::table)@?) in ⊢ (???%);
563         >Htableeq >associative_append >associative_append 
564         >associative_append normalize >associative_append
565         >associative_append normalize >Hnewc <Hmv1
566         >associative_append normalize >associative_append
567         >Hmv1 % 
568       | @Hliftte
569       ]
570      | //
571      ]
572     ]
573    ] 
574   | * #td * whd in ⊢ (%→%→?); >Htc #Htd
575     cases (Htd ? (refl ??)) normalize in ⊢ (%→?);
576     #Hfalse destruct (Hfalse)
577   ]
578  ]
579 | #t1 #t2 #t3 whd in ⊢ (%→%→?); #Ht1 #Ht2
580   #b #Hb cases (Ht1 ? Hb) #Hb' #Ht3 >Ht2 % //
581   cases b in Hb'; normalize #H1 //
582 ]
583 qed.