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