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