matita/matita/lib/turing/universal/marks.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/if_machine.ma".
  18 include "turing/basic_machines.ma".
  19 include "turing/universal/alphabet.ma".
  20
  21 (* ADVANCE TO MARK (right)
  22
  23    sposta la testina a destra fino a raggiungere il primo carattere marcato
  24
  25 *)
  26
  27 (* 0, a ≠ mark _ ⇒ 0, R
  28 0, a = mark _ ⇒ 1, N *)
  29
  30 definition atm_states ≝ initN 3.
  31
  32 definition atm0 : atm_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
  33 definition atm1 : atm_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
  34 definition atm2 : atm_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
  35
  36 definition atmr_step ≝
  37   λalpha:FinSet.λtest:alpha→bool.
  38   mk_TM alpha atm_states
  39   (λp.let 〈q,a〉 ≝ p in
  40    match a with
  41    [ None ⇒ 〈atm1, None ?〉
  42    | Some a' ⇒
  43      match test a' with
  44      [ true ⇒ 〈atm1,None ?〉
  45      | false ⇒ 〈atm2,Some ? 〈a',R〉〉 ]])
  46   atm0 (λx.notb (x == atm0)).
  47
  48 definition Ratmr_step_true ≝
  49   λalpha,test,t1,t2.
  50    ∃ls,a,rs.
  51    t1 = midtape alpha ls a rs ∧ test a = false ∧
  52    t2 = mk_tape alpha (a::ls) (option_hd ? rs) (tail ? rs).
  53
  54 definition Ratmr_step_false ≝
  55   λalpha,test,t1,t2.
  56     t1 = t2 ∧
  57     (current alpha t1 = None ? ∨
  58      (∃a.current ? t1 = Some ? a ∧ test a = true)).
  59
  60 lemma atmr_q0_q1 :
  61   ∀alpha,test,ls,a0,rs. test a0 = true →
  62   step alpha (atmr_step alpha test)
  63     (mk_config ?? atm0 (midtape … ls a0 rs)) =
  64   mk_config alpha (states ? (atmr_step alpha test)) atm1
  65     (midtape … ls a0 rs).
  66 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
  67 whd in match (trans … 〈?,?〉); >Htest %
  68 qed.
  69
  70 lemma atmr_q0_q2 :
  71   ∀alpha,test,ls,a0,rs. test a0 = false →
  72   step alpha (atmr_step alpha test)
  73     (mk_config ?? atm0 (midtape … ls a0 rs)) =
  74   mk_config alpha (states ? (atmr_step alpha test)) atm2
  75     (mk_tape … (a0::ls) (option_hd ? rs) (tail ? rs)).
  76 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
  77 whd in match (trans … 〈?,?〉); >Htest cases ts //
  78 qed.
  79
  80 lemma sem_atmr_step :
  81   ∀alpha,test.
  82   accRealize alpha (atmr_step alpha test)
  83     atm2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
  84 #alpha #test *
  85 [ @(ex_intro ?? 2)
  86   @(ex_intro ?? (mk_config ?? atm1 (niltape ?))) %
  87   [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
  88 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (leftof ? a al)))
  89   % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
  90 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (rightof ? a al)))
  91   % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
  92 | #ls #c #rs @(ex_intro ?? 2)
  93   cases (true_or_false (test c)) #Htest
  94   [ @(ex_intro ?? (mk_config ?? atm1 ?))
  95     [| %
  96       [ %
  97         [ whd in ⊢ (??%?); >atmr_q0_q1 //
  98         | whd in ⊢ ((??%%)→?); #Hfalse destruct ]
  99       | #_ % // %2 @(ex_intro ?? c) % // ]
 100     ]
 101   | @(ex_intro ?? (mk_config ?? atm2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
 102     %
 103     [ %
 104       [ whd in ⊢ (??%?); >atmr_q0_q2 //
 105       | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
 106         % // % //
 107       ]
 108     | #Hfalse @False_ind @(absurd ?? Hfalse) %
 109     ]
 110   ]
 111 ]
 112 qed.
 113
 114 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
 115   ∀ls,c,rs.
 116   (t1 = midtape alpha ls c rs  →
 117   ((test c = true ∧ t2 = t1) ∨
 118    (test c = false ∧
 119     ∀rs1,b,rs2. rs = rs1@b::rs2 →
 120      test b = true → (∀x.memb ? x rs1 = true → test x = false) →
 121      t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
 122
 123 definition adv_to_mark_r ≝
 124   λalpha,test.whileTM alpha (atmr_step alpha test) atm2.
 125
 126 lemma wsem_adv_to_mark_r :
 127   ∀alpha,test.
 128   WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 129 #alpha #test #t #i #outc #Hloop
 130 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
 131 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 132 [ #tapea * #Htapea *
 133   [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 134     #Hfalse destruct (Hfalse)
 135   | * #a * #Ha #Htest #ls #c #rs #H2 %
 136     >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
 137     <Htapea //
 138   ]
 139 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 140   lapply (IH HRfalse) -IH #IH
 141   #ls #c #rs #Htapea %2
 142   cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
 143
 144   >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
 145   [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
 146     cases (IH … Htapeb)
 147     [ * #_ #Houtc >Houtc >Htapeb %
 148     | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
 149   | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
 150     cases (IH … Htapeb)
 151     [ * #Hfalse >(Hmemb …) in Hfalse;
 152       [ #Hft destruct (Hft)
 153       | @memb_hd ]
 154     | * #Htestr1 #H1 >reverse_cons >associative_append
 155       @H1 // #x #Hx @Hmemb @memb_cons //
 156     ]
 157   ]
 158 qed.
 159
 160 lemma terminate_adv_to_mark_r :
 161   ∀alpha,test.
 162   ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
 163 #alpha #test #t
 164 @(terminate_while … (sem_atmr_step alpha test))
 165   [ %
 166   | cases t
 167     [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 168     |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 169     | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
 170       elim rs
 171       [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 172        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 173        % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
 174        normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 175       | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 176         #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 177         >Ht1 @IH
 178       ]
 179     ]
 180   ]
 181 qed.
 182
 183 lemma sem_adv_to_mark_r :
 184   ∀alpha,test.
 185   Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 186 /2/
 187 qed.
 188
 189 (* MARK machine
 190
 191    marks the current character
 192  *)
 193
 194 definition mark_states ≝ initN 2.
 195
 196 definition ms0 : mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
 197 definition ms1 : mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
 198
 199 definition mark ≝
 200   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
 201   (λp.let 〈q,a〉 ≝ p in
 202     match a with
 203     [ None ⇒ 〈ms1,None ?〉
 204     | Some a' ⇒ match (pi1 … q) with
 205       [ O ⇒ let 〈a'',b〉 ≝ a' in 〈ms1,Some ? 〈〈a'',true〉,N〉〉
 206       | S q ⇒ 〈ms1,None ?〉 ] ])
 207   ms0 (λq.q == ms1).
 208
 209 definition R_mark ≝ λalpha,t1,t2.
 210   ∀ls,c,b,rs.
 211   t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
 212   t2 = midtape ? ls 〈c,true〉 rs.
 213
 214 lemma sem_mark :
 215   ∀alpha.Realize ? (mark alpha) (R_mark alpha).
 216 #alpha #intape @(ex_intro ?? 2) cases intape
 217 [ @ex_intro
 218   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 219 |#a #al @ex_intro
 220   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 221 |#a #al @ex_intro
 222   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 223 | #ls * #c #b #rs
 224   @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
 225 qed.
 226
 227
 228 (* MOVE RIGHT AND MARK machine
 229
 230    marks the first character on the right
 231
 232    (could be rewritten using (mark; move_right))
 233  *)
 234
 235 definition mrm_states ≝ initN 3.
 236
 237 definition mrm0 : mrm_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 238 definition mrm1 : mrm_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 239 definition mrm2 : mrm_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
 240
 241 definition move_right_and_mark ≝
 242   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mrm_states
 243   (λp.let 〈q,a〉 ≝ p in
 244     match a with
 245     [ None ⇒ 〈mrm2,None ?〉
 246     | Some a' ⇒ match pi1 … q with
 247       [ O ⇒ 〈mrm1,Some ? 〈a',R〉〉
 248       | S q ⇒ match q with
 249         [ O ⇒ let 〈a'',b〉 ≝ a' in
 250               〈mrm2,Some ? 〈〈a'',true〉,N〉〉
 251         | S _ ⇒ 〈mrm2,None ?〉 ] ] ])
 252   mrm0 (λq.q == mrm2).
 253
 254 definition R_move_right_and_mark ≝ λalpha,t1,t2.
 255   ∀ls,c,d,b,rs.
 256   t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
 257   t2 = midtape ? (c::ls) 〈d,true〉 rs.
 258
 259 lemma sem_move_right_and_mark :
 260   ∀alpha.Realize ? (move_right_and_mark alpha) (R_move_right_and_mark alpha).
 261 #alpha #intape @(ex_intro ?? 3) cases intape
 262 [ @ex_intro
 263   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 264 |#a #al @ex_intro
 265   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 266 |#a #al @ex_intro
 267   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 268 | #ls #c *
 269   [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
 270   | * #d #b #rs @ex_intro
 271     [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
 272 qed.
 273
 274 (* CLEAR MARK machine
 275
 276    clears the mark in the current character
 277  *)
 278
 279 definition clear_mark_states ≝ initN 3.
 280
 281 definition clear0 : clear_mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 282 definition clear1 : clear_mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 283 definition claer2 : clear_mark_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
 284
 285 definition clear_mark ≝
 286   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) clear_mark_states
 287   (λp.let 〈q,a〉 ≝ p in
 288     match a with
 289     [ None ⇒ 〈clear1,None ?〉
 290     | Some a' ⇒ match pi1 … q with
 291       [ O ⇒ let 〈a'',b〉 ≝ a' in 〈clear1,Some ? 〈〈a'',false〉,N〉〉
 292       | S q ⇒ 〈clear1,None ?〉 ] ])
 293   clear0 (λq.q == clear1).
 294
 295 definition R_clear_mark ≝ λalpha,t1,t2.
 296   ∀ls,c,b,rs.
 297   t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
 298   t2 = midtape ? ls 〈c,false〉 rs.
 299
 300 lemma sem_clear_mark :
 301   ∀alpha.Realize ? (clear_mark alpha) (R_clear_mark alpha).
 302 #alpha #intape @(ex_intro ?? 2) cases intape
 303 [ @ex_intro
 304   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 305 |#a #al @ex_intro
 306   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 307 |#a #al @ex_intro
 308   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 309 | #ls * #c #b #rs
 310   @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
 311 qed.
 312
 313 (* ADVANCE MARK RIGHT machine
 314
 315    clears mark on current char,
 316    moves right, and marks new current char
 317
 318 *)
 319
 320 definition adv_mark_r ≝
 321   λalpha:FinSet.
 322     clear_mark alpha · move_r ? · mark alpha.
 323
 324 definition R_adv_mark_r ≝ λalpha,t1,t2.
 325   ∀ls,c,d,b,rs.
 326   t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 (〈d,b〉::rs) →
 327   t2 = midtape ? (〈c,false〉::ls) 〈d,true〉 rs.
 328
 329 lemma sem_adv_mark_r :
 330   ∀alpha.Realize ? (adv_mark_r alpha) (R_adv_mark_r alpha).
 331 #alpha #intape
 332 cases (sem_seq ????? (sem_clear_mark …)
 333          (sem_seq ????? (sem_move_r ?) (sem_mark alpha)) intape)
 334 #k * #outc * #Hloop whd in ⊢ (%→?);
 335 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→%→?); #Hs2 #Hs3
 336 @(ex_intro ?? k) @(ex_intro ?? outc) %
 337 [ @Hloop
 338 | -Hloop #ls #c #d #b #rs #Hintape @(Hs3 … b)
 339   @(Hs2 ls 〈c,false〉 (〈d,b〉::rs))
 340   @(Hs1 … Hintape)
 341 ]
 342 qed.
 343
 344 (* ADVANCE TO MARK (left)
 345
 346 axiomatized
 347
 348 *)
 349 definition atml_step ≝
 350   λalpha:FinSet.λtest:alpha→bool.
 351   mk_TM alpha atm_states
 352   (λp.let 〈q,a〉 ≝ p in
 353    match a with
 354    [ None ⇒ 〈atm1, None ?〉
 355    | Some a' ⇒
 356      match test a' with
 357      [ true ⇒ 〈atm1,None ?〉
 358      | false ⇒ 〈atm2,Some ? 〈a',L〉〉 ]])
 359   atm0 (λx.notb (x == atm0)).
 360
 361 definition Ratml_step_true ≝
 362   λalpha,test,t1,t2.
 363    ∃ls,a,rs.
 364    t1 = midtape alpha ls a rs ∧ test a = false ∧
 365    t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a :: rs).
 366
 367 definition Ratml_step_false ≝
 368   λalpha,test,t1,t2.
 369     t1 = t2 ∧
 370     (current alpha t1 = None ? ∨
 371      (∃a.current ? t1 = Some ? a ∧ test a = true)).
 372
 373 lemma atml_q0_q1 :
 374   ∀alpha,test,ls,a0,rs. test a0 = true →
 375   step alpha (atml_step alpha test)
 376     (mk_config ?? atm0 (midtape … ls a0 rs)) =
 377   mk_config alpha (states ? (atml_step alpha test)) atm1
 378     (midtape … ls a0 rs).
 379 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
 380 whd in match (trans … 〈?,?〉); >Htest %
 381 qed.
 382
 383 lemma atml_q0_q2 :
 384   ∀alpha,test,ls,a0,rs. test a0 = false →
 385   step alpha (atml_step alpha test)
 386     (mk_config ?? atm0 (midtape … ls a0 rs)) =
 387   mk_config alpha (states ? (atml_step alpha test)) atm2
 388     (mk_tape … (tail ? ls) (option_hd ? ls) (a0 :: rs)).
 389 #alpha #test #ls #a0 #rs #Htest whd in ⊢ (??%?);
 390 whd in match (trans … 〈?,?〉); >Htest cases ls //
 391 qed.
 392
 393 lemma sem_atml_step :
 394   ∀alpha,test.
 395   accRealize alpha (atml_step alpha test)
 396     atm2 (Ratml_step_true alpha test) (Ratml_step_false alpha test).
 397 #alpha #test *
 398 [ @(ex_intro ?? 2)
 399   @(ex_intro ?? (mk_config ?? atm1 (niltape ?))) %
 400   [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
 401 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (leftof ? a al)))
 402   % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
 403 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (rightof ? a al)))
 404   % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
 405 | #ls #c #rs @(ex_intro ?? 2)
 406   cases (true_or_false (test c)) #Htest
 407   [ @(ex_intro ?? (mk_config ?? atm1 ?))
 408     [| %
 409       [ %
 410         [ whd in ⊢ (??%?); >atml_q0_q1 //
 411         | whd in ⊢ ((??%%)→?); #Hfalse destruct ]
 412       | #_ % // %2 @(ex_intro ?? c) % // ]
 413     ]
 414   | @(ex_intro ?? (mk_config ?? atm2 (mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs))))
 415     %
 416     [ %
 417       [ whd in ⊢ (??%?); >atml_q0_q2 //
 418       | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
 419         % // % //
 420       ]
 421     | #Hfalse @False_ind @(absurd ?? Hfalse) %
 422     ]
 423   ]
 424 ]
 425 qed.
 426
 427 definition R_adv_to_mark_l ≝ λalpha,test,t1,t2.
 428   ∀ls,c,rs.
 429   (t1 = midtape alpha ls c rs  →
 430   ((test c = true ∧ t2 = t1) ∨
 431    (test c = false ∧
 432     ∀ls1,b,ls2. ls = ls1@b::ls2 →
 433      test b = true → (∀x.memb ? x ls1 = true → test x = false) →
 434      t2 = midtape ? ls2 b (reverse ? ls1@c::rs)))).
 435
 436 definition adv_to_mark_l ≝
 437   λalpha,test.whileTM alpha (atml_step alpha test) atm2.
 438
 439 lemma wsem_adv_to_mark_l :
 440   ∀alpha,test.
 441   WRealize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
 442 #alpha #test #t #i #outc #Hloop
 443 lapply (sem_while … (sem_atml_step alpha test) t i outc Hloop) [%]
 444 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 445 [ #tapea * #Htapea *
 446   [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 447     #Hfalse destruct (Hfalse)
 448   | * #a * #Ha #Htest #ls #c #rs #H2 %
 449     >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
 450     <Htapea //
 451   ]
 452 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 453   lapply (IH HRfalse) -IH #IH
 454   #ls #c #rs #Htapea %2
 455   cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
 456   >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
 457   [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
 458     cases (IH … Htapeb)
 459     [ * #_ #Houtc >Houtc >Htapeb %
 460     | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
 461   | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
 462     cases (IH … Htapeb)
 463     [ * #Hfalse >(Hmemb …) in Hfalse;
 464       [ #Hft destruct (Hft)
 465       | @memb_hd ]
 466     | * #Htestr1 #H1 >reverse_cons >associative_append
 467       @H1 // #x #Hx @Hmemb @memb_cons //
 468     ]
 469   ]
 470 qed.
 471
 472 lemma terminate_adv_to_mark_l :
 473   ∀alpha,test.
 474   ∀t.Terminate alpha (adv_to_mark_l alpha test) t.
 475 #alpha #test #t
 476 @(terminate_while … (sem_atml_step alpha test))
 477   [ %
 478   | cases t
 479     [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 480     |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 481     | #ls elim ls
 482       [#c #rs % #t1 * #ls0 * #c0 * #rs0 * *
 483        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 484        % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
 485        normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 486       | #rs0 #r0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 487         #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 488         >Ht1 @IH
 489       ]
 490     ]
 491   ]
 492 qed.
 493
 494 lemma sem_adv_to_mark_l :
 495   ∀alpha,test.
 496   Realize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
 497 /2/
 498 qed.
 499
 500 (*
 501    ADVANCE BOTH MARKS machine
 502
 503    l1 does not contain marks ⇒
 504
 505
 506    input:
 507    l0 x* a l1 x0* a0 l2
 508               ^
 509
 510    output:
 511    l0 x a* l1 x0 a0* l2
 512         ^
 513 *)
 514
 515 definition adv_both_marks ≝ λalpha.
 516   adv_mark_r alpha · move_l ? ·
 517     adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha) ·
 518       adv_mark_r alpha.
 519
 520 definition R_adv_both_marks ≝
 521   λalpha,t1,t2.
 522     ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 523     t1 = midtape (FinProd … alpha FinBool)
 524         (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
 525     t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2).
 526
 527 lemma sem_adv_both_marks :
 528   ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).
 529 #alpha #intape
 530 cases (sem_seq ????? (sem_adv_mark_r …)
 531         (sem_seq ????? (sem_move_l …)
 532           (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
 533             (sem_adv_mark_r alpha))) intape)
 534 #k * #outc * #Hloop whd in ⊢ (%→?);
 535 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→?); #Hs2
 536 * #tc * whd in ⊢ (%→%→?); #Hs3 #Hs4
 537 @(ex_intro ?? k) @(ex_intro ?? outc) %
 538 [ @Hloop
 539 | -Hloop #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
 540   @(Hs4 … false) -Hs4
 541   lapply (Hs1 … Hintape) #Hta
 542   lapply (Hs2 … Hta) #Htb
 543   cases (Hs3 … Htb)
 544   [ * #Hfalse normalize in Hfalse; destruct (Hfalse)
 545   | * #_ -Hs3 #Hs3
 546     lapply (Hs3 (l1@[〈a,false〉]) 〈x,true〉 l0 ???)
 547     [ #x1 #Hx1 cases (memb_append … Hx1)
 548       [ @Hl1
 549       | #Hx1' >(memb_single … Hx1') % ]
 550     | %
 551     | >associative_append %
 552     | >reverse_append #Htc @Htc ]
 553   ]
 554 qed.
 555
 556 (*
 557    MATCH AND ADVANCE(f)
 558
 559    input:
 560    l0 x* a l1 x0* a0 l2
 561               ^
 562
 563    output:
 564    l0 x a* l1 x0 a0* l2   (f(x0) == true)
 565         ^
 566    l0 x* a l1 x0* a0 l2   (f(x0) == false)
 567               ^
 568 *)
 569
 570 definition match_and_adv ≝
 571   λalpha,f.ifTM ? (test_char ? f)
 572      (adv_both_marks alpha) (clear_mark ?) tc_true.
 573
 574 definition R_match_and_adv ≝
 575   λalpha,f,t1,t2.
 576     ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 577     t1 = midtape (FinProd … alpha FinBool)
 578         (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
 579     (f 〈x0,true〉 = true ∧ t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2))
 580     ∨ (f 〈x0,true〉 = false ∧
 581     t2 = midtape ? (l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)).
 582
 583 lemma sem_match_and_adv :
 584   ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
 585 #alpha #f #intape
 586 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
 587 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
 588 % [ @Hloop ] -Hloop
 589 cases Hif
 590 [ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
 591   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
 592   >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta % %
 593   [ @Hf | @Houtc [ @Hl1 | @Hta ] ]
 594 | * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
 595   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
 596   >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta %2 %
 597   [ @Hf | >(Houtc … Hta) % ]
 598 ]
 599 qed.
 600
 601 (*
 602  if x = c
 603       then move_right; ----
 604            adv_to_mark_r;
 605            if current (* x0 *) = 0
 606               then advance_mark ----
 607                    adv_to_mark_l;
 608                    advance_mark
 609               else STOP
 610       else M
 611 *)
 612
 613 definition comp_step_subcase ≝ λalpha,c,elseM.
 614   ifTM ? (test_char ? (λx.x == c))
 615     (move_r … · adv_to_mark_r ? (is_marked alpha) · match_and_adv ? (λx.x == c))
 616     elseM tc_true.
 617
 618 definition R_comp_step_subcase ≝
 619   λalpha,c,RelseM,t1,t2.
 620     ∀l0,x,rs.t1 = midtape (FinProd … alpha FinBool) l0 〈x,true〉 rs →
 621     (〈x,true〉 = c ∧
 622      ∀a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 623      rs = 〈a,false〉::l1@〈x0,true〉::〈a0,false〉::l2 →
 624      ((x = x0 ∧
 625       t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1@〈x0,false〉::〈a0,true〉::l2)) ∨
 626       (x ≠ x0 ∧
 627       t2 = midtape (FinProd … alpha FinBool)
 628         (reverse ? l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)))) ∨
 629     (〈x,true〉 ≠ c ∧ RelseM t1 t2).
 630
 631 lemma sem_comp_step_subcase :
 632   ∀alpha,c,elseM,RelseM.
 633   Realize ? elseM RelseM →
 634   Realize ? (comp_step_subcase alpha c elseM)
 635     (R_comp_step_subcase alpha c RelseM).
 636 #alpha #c #elseM #RelseM #Helse #intape
 637 cases (sem_if ? (test_char ? (λx.x == c)) … tc_true
 638         (sem_test_char ? (λx.x == c))
 639         (sem_seq ????? (sem_move_r …)
 640           (sem_seq ????? (sem_adv_to_mark_r ? (is_marked alpha))
 641              (sem_match_and_adv ? (λx.x == c)))) Helse intape)
 642 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)
 643 % [ @Hloop ] -Hloop cases HR -HR
 644 [ * #ta * whd in ⊢ (%→?); #Hta * #tb * whd in ⊢ (%→?); #Htb
 645   * #tc * whd in ⊢ (%→?); #Htc whd in ⊢ (%→?); #Houtc
 646   #l0 #x #rs #Hintape cases (true_or_false (〈x,true〉==c)) #Hc
 647   [ % % [ @(\P Hc) ]
 648     #a #l1 #x0 #a0 #l2 #Hl1 #Hrs >Hrs in Hintape; #Hintape
 649     >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta
 650     #Hx #Hta lapply (Htb … Hta) -Htb #Htb
 651     cases (Htc … Htb) [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
 652     -Htc * #_ #Htc lapply (Htc l1 〈x0,true〉 (〈a0,false〉::l2) (refl ??) (refl ??) Hl1)
 653     -Htc #Htc cases (Houtc ???????? Htc) -Houtc
 654     [ * #Hx0 #Houtc %
 655       % [ <(\P Hx0) in Hx; #Hx lapply (\P Hx) #Hx' destruct (Hx') %
 656         | >Houtc >reverse_reverse % ]
 657     | * #Hx0 #Houtc %2
 658       % [ <(\P Hx) in Hx0; #Hx0 lapply (\Pf Hx0) @not_to_not #Hx' >Hx' %
 659         | >Houtc % ]
 660     | #x #membx @Hl1 <(reverse_reverse …l1) @memb_reverse @membx ]
 661   | %2 % [ @(\Pf Hc) ]
 662     >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hx #Hta
 663     >Hx in Hc;#Hc destruct (Hc) ]
 664 | * #ta * whd in ⊢ (%→?); #Hta #Helse #ls #c0 #rs #Hintape %2
 665   >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hc #Hta %
 666   [ @(\Pf Hc) | <Hta @Helse ]
 667 ]
 668 qed.
 669
 670 (*
 671 - se marcato, itero
 672 - se non è marcato
 673   + se è un bit, ho fallito il confronto della tupla corrente
 674   + se è un separatore, la tupla fa match
 675
 676
 677 ifTM ? (test_char ? is_marked)
 678   (single_finalTM … (comp_step_subcase unialpha 〈bit false,true〉
 679     (comp_step_subcase unialpha 〈bit true,true〉
 680       (clear_mark …))))
 681   (nop ?)
 682 *)
 683
 684 definition comp_step ≝
 685   ifTM ? (test_char ? (is_marked ?))
 686   (single_finalTM … (comp_step_subcase FSUnialpha 〈bit false,true〉
 687     (comp_step_subcase FSUnialpha 〈bit true,true〉
 688       (comp_step_subcase FSUnialpha 〈null,true〉
 689         (clear_mark …)))))
 690   (nop ?)
 691   tc_true.
 692
 693 definition R_comp_step_true ≝
 694   λt1,t2.
 695     ∀l0,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) l0 c rs →
 696     ∃c'. c = 〈c',true〉 ∧
 697     ((bit_or_null c' = true ∧
 698      ∀a,l1,c0,a0,l2.
 699       rs = 〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2 →
 700       (∀c.memb ? c l1 = true → is_marked ? c = false) →
 701       (c0 = c' ∧
 702        t2 = midtape ? (〈c',false〉::l0) 〈a,true〉 (l1@〈c0,false〉::〈a0,true〉::l2)) ∨
 703       (c0 ≠ c' ∧
 704        t2 = midtape (FinProd … FSUnialpha FinBool)
 705         (reverse ? l1@〈a,false〉::〈c',true〉::l0) 〈c0,false〉 (〈a0,false〉::l2))) ∨
 706      (bit_or_null c' = false ∧ t2 = midtape ? l0 〈c',false〉 rs)).
 707
 708 definition R_comp_step_false ≝
 709   λt1,t2.
 710    ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
 711    is_marked ? c = false ∧ t2 = t1.
 712
 713 lemma sem_comp_step :
 714   accRealize ? comp_step (inr … (inl … (inr … start_nop)))
 715     R_comp_step_true R_comp_step_false.
 716 #intape
 717 cases (acc_sem_if … (sem_test_char ? (is_marked ?))
 718         (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
 719           (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
 720             (sem_comp_step_subcase FSUnialpha 〈null,true〉 ??
 721               (sem_clear_mark …))))
 722         (sem_nop …) intape)
 723 #k * #outc * * #Hloop #H1 #H2
 724 @(ex_intro ?? k) @(ex_intro ?? outc) %
 725 [ % [@Hloop ] ] -Hloop
 726 [ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 *
 727   #ta * whd in ⊢ (%→?); #Hleft #Hright #ls #c #rs #Hintape
 728   >Hintape in Hleft; #Hleft cases (Hleft ? (refl ??)) -Hleft
 729   cases c in Hintape; #c' #b #Hintape whd in ⊢ (??%?→?);
 730   #Hb >Hb #Hta @(ex_intro ?? c') % //
 731   cases (Hright … Hta)
 732   [ * #Hc' #H1 % % [destruct (Hc') % ]
 733     #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
 734     cases (H1 … Hl1 Hrs)
 735     [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
 736     | * #Hneq #Houtc %2 %
 737       [ @sym_not_eq //
 738       | @Houtc ]
 739     ]
 740   | * #Hc #Helse1 cases (Helse1 … Hta)
 741     [ * #Hc' #H1 % % [destruct (Hc') % ]
 742       #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
 743       cases (H1 … Hl1 Hrs)
 744       [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
 745       | * #Hneq #Houtc %2 %
 746         [ @sym_not_eq //
 747         | @Houtc ]
 748       ]
 749     | * #Hc' #Helse2 cases (Helse2 … Hta)
 750       [ * #Hc'' #H1 % % [destruct (Hc'') % ]
 751         #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
 752         cases (H1 … Hl1 Hrs)
 753         [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
 754         | * #Hneq #Houtc %2 %
 755           [ @sym_not_eq //
 756           | @Houtc ]
 757         ]
 758       | * #Hc'' whd in ⊢ (%→?); #Helse3 %2 %
 759         [ generalize in match Hc''; generalize in match Hc'; generalize in match Hc;
 760           cases c'
 761           [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
 762               | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
 763           | #_ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
 764           |*: #_ #_ #_ % ]
 765         | @(Helse3 … Hta)
 766         ]
 767       ]
 768     ]
 769   ]
 770 | #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 *
 771   #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
 772   >Hintape in Hleft; #Hleft
 773   cases (Hleft ? (refl ??)) -Hleft
 774   #Hc #Hta % // >Hright //
 775 ]
 776 qed.
 777
 778 definition compare ≝
 779   whileTM ? comp_step (inr … (inl … (inr … start_nop))).
 780
 781 (*
 782 definition R_compare :=
 783   λt1,t2.
 784   (t
 785
 786   ∀ls,c,b,rs.t1 = midtape ? ls 〈c,b〉 rs →
 787   (b = true → rs = ....) →
 788   (b = false ∧ ....) ∨
 789   (b = true ∧
 790
 791    rs = cs@l1@〈c0,true〉::cs0@l2
 792    (
 793
 794
 795   ls 〈c,b〉 cs l1 〈c0,b0〉 cs0 l2
 796
 797
 798 ACCETTAZIONE:
 799   ls (hd (Ls@〈grid,false〉))* (tail (Ls@〈grid,false〉)) l1 (hd (Ls@〈comma,false〉))* (tail (Ls@〈comma,false〉)) l2
 800      ^^^^^^^^^^^^^^^^^^^^^^^
 801
 802   ls Ls 〈grid,false〉 l1 Ls 〈comma,true〉 l2
 803         ^^^^^^^^^^^^
 804
 805 RIFIUTO: c ≠ d
 806
 807   ls (hd (Ls@〈c,false〉))* (tail (Ls@〈c,false〉)) l1 (hd (Ls@〈d,false〉))* (tail (Ls@〈d,false〉)) l2
 808      ^^^^^^^^^^^^^^^^^^^^^^^
 809
 810
 811   ls Ls 〈c,true〉 l1 Ls 〈d,false〉 l2
 812                        ^^^^^^^^
 813
 814   ).
 815
 816   |bs| = |b0s| →
 817   (∃la,d.〈b,true〉::bs = la@[〈grid,d〉] ∧ ∀x.memb ? x la → is_bit (\fst x) = true) →
 818   (∃lb,d0.〈b0,true〉::b0s = lb@[〈comma,d0〉] ∧ ∀x.memb ? x lb → is_bit (\fst x) = true) →
 819   t1 = midtape ? l0 〈b,true〉 (bs@l1@〈b0,true〉::b0s@l2 →
 820
 821   mk_tape left (option current) right
 822
 823   (b = grid ∧ b0 = comma ∧ bs = [] ∧ b0s = [] ∧
 824    t2 = midtape ? l0 〈grid,false〉 (l1@〈comma,true〉::l2)) ∨
 825   (b = bit x ∧ b = c ∧ bs = b0s
 826   *)
 827 definition R_compare :=
 828   λt1,t2.
 829   ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
 830   (∀c'.bit_or_null c' = false → c = 〈c',true〉 → t2 = midtape ? ls 〈c',false〉 rs) ∧
 831   (∀c'. c = 〈c',false〉 → t2 = t1) ∧
 832   ∀b,b0,bs,b0s,l1,l2.
 833   |bs| = |b0s| →
 834   (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → bit_or_null (\fst c) = true) →
 835   (∀c.memb (FinProd … FSUnialpha FinBool) c b0s = true → bit_or_null (\fst c) = true) →
 836   (∀c.memb ? c bs = true → is_marked ? c = false) →
 837   (∀c.memb ? c b0s = true → is_marked ? c = false) →
 838   (∀c.memb ? c l1 = true → is_marked ? c = false) →
 839   c = 〈b,true〉 → bit_or_null b = true →
 840   rs = bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2 →
 841   (〈b,true〉::bs = 〈b0,true〉::b0s ∧
 842    t2 = midtape ? (reverse ? bs@〈b,false〉::ls)
 843           〈grid,false〉 (l1@〈b0,false〉::b0s@〈comma,true〉::l2)) ∨
 844   (∃la,c',d',lb,lc.c' ≠ d' ∧
 845     〈b,false〉::bs = la@〈c',false〉::lb ∧
 846     〈b0,false〉::b0s = la@〈d',false〉::lc ∧
 847     t2 = midtape (FinProd … FSUnialpha FinBool) (reverse ? la@
 848                     reverse ? l1@
 849                     〈grid,false〉::
 850                     reverse ? lb@
 851                     〈c',true〉::
 852                     reverse ? la@ls)
 853                     〈d',false〉 (lc@〈comma,false〉::l2)).
 854
 855 lemma wsem_compare : WRealize ? compare R_compare.
 856 #t #i #outc #Hloop
 857 lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%]
 858 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 859 [ #tapea whd in ⊢ (%→?); #Rfalse #ls #c #rs #Htapea %
 860   [ %
 861     [ #c' #Hc' #Hc lapply (Rfalse … Htapea) -Rfalse * >Hc
 862       whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
 863     | #c' #Hc lapply (Rfalse … Htapea) -Rfalse * #_
 864       #Htrue @Htrue ]
 865   | #b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1 #Hc
 866     cases (Rfalse … Htapea) -Rfalse >Hc whd in ⊢ (??%?→?);#Hfalse destruct (Hfalse)
 867   ]
 868 | #tapea #tapeb #tapec #Hleft #Hright #IH #Htapec lapply (IH Htapec) -Htapec -IH #IH
 869   whd in Hleft; #ls #c #rs #Htapea cases (Hleft … Htapea) -Hleft
 870   #c' * #Hc >Hc cases (true_or_false (bit_or_null c')) #Hc'
 871   [2: *
 872     [ * >Hc' #H @False_ind destruct (H)
 873     | * #_ #Htapeb cases (IH … Htapeb) * #_ #H #_ %
 874       [%
 875         [#c1 #Hc1 #Heqc destruct (Heqc) <Htapeb @(H c1) %
 876         |#c1 #Hfalse destruct (Hfalse)
 877         ]
 878       |#b #b0 #bs #b0s #l1 #l2 #_ #_ #_ #_ #_ #_
 879        #Heq destruct (Heq) >Hc' #Hfalse @False_ind destruct (Hfalse)
 880       ]
 881     ]
 882  |#Hleft %
 883     [ %
 884       [ #c'' #Hc'' #Heq destruct (Heq) >Hc'' in Hc'; #H destruct (H)
 885       | #c0 #Hfalse destruct (Hfalse)
 886       ]
 887     |#b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1
 888      #Heq destruct (Heq) #_ #Hrs cases Hleft -Hleft
 889       [2: * >Hc' #Hfalse @False_ind destruct ] * #_
 890        @(list_cases2 … Hlen)
 891        [ #Hbs #Hb0s generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
 892        -Hrs #Hrs normalize in Hrs; #Hleft cases (Hleft ????? Hrs ?) -Hleft
 893          [ * #Heqb #Htapeb cases (IH … Htapeb) -IH * #IH #_ #_
 894           % %
 895             [ >Heqb >Hbs >Hb0s %
 896             | >Hbs >Hb0s @IH %
 897             ]
 898          |* #Hneqb #Htapeb %2
 899           @(ex_intro … [ ]) @(ex_intro … b)
 900           @(ex_intro … b0) @(ex_intro … [ ])
 901           @(ex_intro … [ ]) %
 902             [ % [ % [@sym_not_eq //| >Hbs %] | >Hb0s %]
 903             | cases (IH … Htapeb) -IH * #_ #IH #_ >(IH ? (refl ??))
 904               @Htapeb
 905             ]
 906          | @Hl1 ]
 907       | * #b' #bitb' * #b0' #bitb0' #bs' #b0s' #Hbs #Hb0s
 908         generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
 909         cut (bit_or_null b' = true ∧ bit_or_null b0' = true ∧
 910              bitb' = false ∧ bitb0' = false)
 911         [ % [ % [ % [ >Hbs in Hbs1; #Hbs1 @(Hbs1 〈b',bitb'〉) @memb_hd
 912             | >Hb0s in Hb0s1; #Hb0s1 @(Hb0s1 〈b0',bitb0'〉) @memb_hd ]
 913             | >Hbs in Hbs2; #Hbs2 @(Hbs2 〈b',bitb'〉) @memb_hd ]
 914             | >Hb0s in Hb0s2; #Hb0s2 @(Hb0s2 〈b0',bitb0'〉) @memb_hd ]
 915         | * * * #Ha #Hb #Hc #Hd >Hc >Hd
 916           #Hrs #Hleft
 917           cases (Hleft b' (bs'@〈grid,false〉::l1) b0 b0'
 918                          (b0s'@〈comma,false〉::l2) ??) -Hleft
 919           [ 3: >Hrs normalize @eq_f >associative_append %
 920           | * #Hb0 #Htapeb cases (IH …Htapeb) -IH * #_ #_ #IH
 921             cases (IH b' b0' bs' b0s' (l1@[〈b0,false〉]) l2 ??????? Ha ?) -IH
 922             [ * #Heq #Houtc % %
 923               [ >Hb0 @eq_f >Hbs in Heq; >Hb0s in ⊢ (%→?); #Heq
 924                 destruct (Heq) >Hb0s >Hc >Hd %
 925               | >Houtc >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
 926                 >associative_append %
 927               ]
 928             | * #la * #c' * #d' * #lb * #lc * * * #H1 #H2 #H3 #H4 %2
 929               @(ex_intro … (〈b,false〉::la)) @(ex_intro … c') @(ex_intro … d')
 930               @(ex_intro … lb) @(ex_intro … lc)
 931               % [ % [ % // >Hbs >Hc >H2 % | >Hb0s >Hd >H3 >Hb0 % ]
 932                 | >H4 >Hbs >Hb0s >Hc >Hd >Hb0 >reverse_append
 933                   >reverse_cons >reverse_cons
 934                   >associative_append >associative_append
 935                   >associative_append >associative_append %
 936                 ]
 937             | generalize in match Hlen; >Hbs >Hb0s
 938               normalize #Hlen destruct (Hlen) @e0
 939             | #c0 #Hc0 @Hbs1 >Hbs @memb_cons //
 940             | #c0 #Hc0 @Hb0s1 >Hb0s @memb_cons //
 941             | #c0 #Hc0 @Hbs2 >Hbs @memb_cons //
 942             | #c0 #Hc0 @Hb0s2 >Hb0s @memb_cons //
 943             | #c0 #Hc0 cases (memb_append … Hc0)
 944               [ @Hl1 | #Hc0' >(memb_single … Hc0') % ]
 945             | %
 946             | >associative_append >associative_append % ]
 947          | * #Hneq #Htapeb %2
 948             @(ex_intro … []) @(ex_intro … b) @(ex_intro … b0)
 949             @(ex_intro … bs) @(ex_intro … b0s) %
 950            [ % // % // @sym_not_eq //
 951            | >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
 952              >reverse_append in Htapeb; >reverse_cons
 953              >associative_append >associative_append
 954              #Htapeb <Htapeb
 955              cases (IH … Htapeb) -Htapeb -IH * #_ #IH #_ @(IH ? (refl ??))
 956            ]
 957          | #c1 #Hc1 cases (memb_append … Hc1) #Hyp
 958            [ @Hbs2 >Hbs @memb_cons @Hyp
 959            | cases (orb_true_l … Hyp)
 960              [ #Hyp2 >(\P Hyp2) %
 961              | @Hl1
 962              ]
 963            ]
 964          ]
 965 ]]]]]
 966 qed.
 967
 968 axiom sem_compare : Realize ? compare R_compare.