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