matita/matita/lib/turing/universal/compare.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
  19 (* ADVANCE TO MARK (right)
  20
  21    sposta la testina a destra fino a raggiungere il primo carattere marcato
  22
  23 *)
  24
  25 (* 0, a ≠ mark _ ⇒ 0, R
  26 0, a = mark _ ⇒ 1, N *)
  27
  28 definition atm_states ≝ initN 3.
  29
  30 definition atmr_step ≝
  31   λalpha:FinSet.λtest:alpha→bool.
  32   mk_TM alpha atm_states
  33   (λp.let 〈q,a〉 ≝ p in
  34    match a with
  35    [ None ⇒ 〈1, None ?〉
  36    | Some a' ⇒
  37      match test a' with
  38      [ true ⇒ 〈1,None ?〉
  39      | false ⇒ 〈2,Some ? 〈a',R〉〉 ]])
  40   O (λx.notb (x == 0)).
  41
  42 definition Ratmr_step_true ≝
  43   λalpha,test,t1,t2.
  44    ∃ls,a,rs.
  45    t1 = midtape alpha ls a rs ∧ test a = false ∧
  46    t2 = mk_tape alpha (a::ls) (option_hd ? rs) (tail ? rs).
  47
  48 definition Ratmr_step_false ≝
  49   λalpha,test,t1,t2.
  50     t1 = t2 ∧
  51     (current alpha t1 = None ? ∨
  52      (∃a.current ? t1 = Some ? a ∧ test a = true)).
  53
  54 lemma atmr_q0_q1 :
  55   ∀alpha,test,ls,a0,rs. test a0 = true →
  56   step alpha (atmr_step alpha test)
  57     (mk_config ?? 0 (midtape … ls a0 rs)) =
  58   mk_config alpha (states ? (atmr_step alpha test)) 1
  59     (midtape … ls a0 rs).
  60 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
  61 qed.
  62
  63 lemma atmr_q0_q2 :
  64   ∀alpha,test,ls,a0,rs. test a0 = false →
  65   step alpha (atmr_step alpha test)
  66     (mk_config ?? 0 (midtape … ls a0 rs)) =
  67   mk_config alpha (states ? (atmr_step alpha test)) 2
  68     (mk_tape … (a0::ls) (option_hd ? rs) (tail ? rs)).
  69 #alpha #test #ls #a0 #ts #Htest normalize >Htest cases ts //
  70 qed.
  71
  72 lemma sem_atmr_step :
  73   ∀alpha,test.
  74   accRealize alpha (atmr_step alpha test)
  75     2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
  76 #alpha #test *
  77 [ @(ex_intro ?? 2)
  78   @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
  79   [ % // #Hfalse destruct | #_ % // % % ]
  80 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
  81   % [ % // #Hfalse destruct | #_ % // % % ]
  82 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
  83   % [ % // #Hfalse destruct | #_ % // % % ]
  84 | #ls #c #rs @(ex_intro ?? 2)
  85   cases (true_or_false (test c)) #Htest
  86   [ @(ex_intro ?? (mk_config ?? 1 ?))
  87     [| %
  88       [ %
  89         [ whd in ⊢ (??%?); >atmr_q0_q1 //
  90         | #Hfalse destruct ]
  91       | #_ % // %2 @(ex_intro ?? c) % // ]
  92     ]
  93   | @(ex_intro ?? (mk_config ?? 2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
  94     %
  95     [ %
  96       [ whd in ⊢ (??%?); >atmr_q0_q2 //
  97       | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
  98         % // % //
  99       ]
 100     | #Hfalse @False_ind @(absurd ?? Hfalse) %
 101     ]
 102   ]
 103 ]
 104 qed.
 105
 106 (*
 107 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
 108   ∀ls,c,rs.
 109   t1 = mk_tape alpha ls c rs  →
 110   (c = None ? ∧ t2 = t1) ∨
 111   (∃c'.c = Some ? c' ∧
 112     ((test c' = true ∧ t2 = t1) ∨
 113      (test c' = false ∧
 114        (((∀x.memb ? x rs = true → test x = false) ∧
 115          t2 = mk_tape ? (reverse ? rs@c'::ls) (None ?) []) ∨
 116         (∃rs1,b,rs2.rs = rs1@b::rs2 ∧
 117          test b = true ∧ (∀x.memb ? x rs1 = true → test x = false) ∧
 118          t2 = midtape ? (reverse ? rs1@c'::rs) b rs2))))).
 119
 120 definition adv_to_mark_r ≝
 121   λalpha,test.whileTM alpha (atmr_step alpha test) 2.
 122
 123 lemma wsem_adv_to_mark_r :
 124   ∀alpha,test.
 125   WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 126 #alpha #test #t #i #outc #Hloop
 127 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
 128 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 129 [ #tapea * #Htapea *
 130   [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 131     #Hfalse destruct (Hfalse)
 132   | * #a * #Ha #Htest #ls #c #rs cases c
 133     [ #Htapea' % % // >Htapea %
 134     | #c' #Htapea' %2 @(ex_intro ?? c') % //
 135       cases (true_or_false (test c')) #Htestc
 136       [ % % // >Htapea %
 137       | %2 % // generalize in match Htapea'; -Htapea'
 138         cases rs
 139         [ #Htapea' % %
 140           [ normalize #x #Hfalse destruct (Hfalse)
 141           | <Htapea >Htapea' %
 142
 143
 144    #H2 %
 145     >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % // <Htapea //
 146   ]
 147 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 148   lapply (IH HRfalse) -IH #IH
 149   #ls #c #rs #Htapea
 150   cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
 151   >Htapea' in Htapea; #Htapea destruct (Htapea) %2 % //
 152   generalize in match Htapeb; -Htapeb
 153   generalize in match Htapea'; -Htapea'
 154   cases rs
 155   [ #Htapea #Htapeb % %
 156     [ #x0 normalize #Hfalse destruct (Hfalse)
 157     | normalize in Htapeb; cases (IH
 158
 159
 160    [//]
 161    cases (true_or_false (test c))
 162   [ #Htestc %
 163
 164
 165   [ #Htapea %2 % [ %2 // ]
 166     #rs #Htapea %2
 167
 168
 169    *
 170   [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
 171     cases (IH … Htapeb)
 172     [ * #_ #Houtc >Houtc >Htapeb %
 173     | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
 174   | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
 175     cases (IH … Htapeb)
 176     [ * #Hfalse >(Hmemb …) in Hfalse;
 177       [ #Hft destruct (Hft)
 178       | @memb_hd ]
 179     | * #Htestr1 #H1 >reverse_cons >associative_append
 180       @H1 // #x #Hx @Hmemb @memb_cons //
 181     ]
 182   ]
 183 qed. *)
 184
 185 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
 186   ∀ls,c,rs.
 187   (t1 = midtape alpha ls c rs  →
 188   ((test c = true ∧ t2 = t1) ∨
 189    (test c = false ∧
 190     ∀rs1,b,rs2. rs = rs1@b::rs2 →
 191      test b = true → (∀x.memb ? x rs1 = true → test x = false) →
 192      t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
 193
 194 definition adv_to_mark_r ≝
 195   λalpha,test.whileTM alpha (atmr_step alpha test) 2.
 196
 197 lemma wsem_adv_to_mark_r :
 198   ∀alpha,test.
 199   WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 200 #alpha #test #t #i #outc #Hloop
 201 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
 202 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 203 [ #tapea * #Htapea *
 204   [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 205     #Hfalse destruct (Hfalse)
 206   | * #a * #Ha #Htest #ls #c #rs #H2 %
 207     >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
 208     <Htapea //
 209   ]
 210 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 211   lapply (IH HRfalse) -IH #IH
 212   #ls #c #rs #Htapea %2
 213   cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
 214
 215   >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
 216   [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
 217     cases (IH … Htapeb)
 218     [ * #_ #Houtc >Houtc >Htapeb %
 219     | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
 220   | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
 221     cases (IH … Htapeb)
 222     [ * #Hfalse >(Hmemb …) in Hfalse;
 223       [ #Hft destruct (Hft)
 224       | @memb_hd ]
 225     | * #Htestr1 #H1 >reverse_cons >associative_append
 226       @H1 // #x #Hx @Hmemb @memb_cons //
 227     ]
 228   ]
 229 qed.
 230
 231 lemma terminate_adv_to_mark_r :
 232   ∀alpha,test.
 233   ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
 234 #alpha #test #t
 235 @(terminate_while … (sem_atmr_step alpha test))
 236   [ %
 237   | cases t
 238     [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 239     |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 240     | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
 241       elim rs
 242       [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 243        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 244        % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
 245        normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 246       | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 247         #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 248         >Ht1 @IH
 249       ]
 250     ]
 251   ]
 252 qed.
 253
 254 lemma sem_adv_to_mark_r :
 255   ∀alpha,test.
 256   Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 257 /2/
 258 qed.
 259
 260 (* NO OPERATION
 261
 262   t1 = t2
 263   *)
 264
 265 definition nop_states ≝ initN 1.
 266
 267 definition nop ≝
 268   λalpha:FinSet.mk_TM alpha nop_states
 269   (λp.let 〈q,a〉 ≝ p in 〈q,None ?〉)
 270   O (λ_.true).
 271
 272 definition R_nop ≝ λalpha.λt1,t2:tape alpha.t2 = t1.
 273
 274 lemma sem_nop :
 275   ∀alpha.Realize alpha (nop alpha) (R_nop alpha).
 276 #alpha #intape @(ex_intro ?? 1) @ex_intro [| % normalize % ]
 277 qed.
 278
 279 (*
 280    q0 _ → q1, R
 281    q1 〈a,false〉 → qF, 〈a,true〉, N
 282    q1 〈a,true〉 → qF, _ , N
 283    qF _ → None ?
 284  *)
 285
 286 definition mark_states ≝ initN 3.
 287
 288 definition mark ≝
 289   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
 290   (λp.let 〈q,a〉 ≝ p in
 291     match a with
 292     [ None ⇒ 〈2,None ?〉
 293     | Some a' ⇒ match q with
 294       [ O ⇒ 〈1,Some ? 〈a',R〉〉
 295       | S q ⇒ match q with
 296         [ O ⇒ let 〈a'',b〉 ≝ a' in
 297               〈2,Some ? 〈〈a'',true〉,N〉〉
 298         | S _ ⇒ 〈2,None ?〉 ] ] ])
 299   O (λq.q == 2).
 300
 301 definition R_mark ≝ λalpha,t1,t2.
 302   ∀ls,c,d,b,rs.
 303   t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
 304   t2 = midtape ? (c::ls) 〈d,true〉 rs.
 305
 306 (*lemma mark_q0_q1 :
 307   ∀alpha,ls,c,rs.
 308   step alpha (mark alpha)
 309     (mk_config ?? 0 (midtape … ls c rs)) =
 310   mk_config alpha (states ? (mark alpha)) 1
 311     (midtape … (ls a0 rs).*)
 312
 313 lemma sem_mark :
 314   ∀alpha.Realize ? (mark alpha) (R_mark alpha).
 315 #alpha #intape @(ex_intro ?? 3) cases intape
 316 [ @ex_intro
 317   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 318 |#a #al @ex_intro
 319   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 320 |#a #al @ex_intro
 321   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 322 | #ls #c *
 323   [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
 324   | * #d #b #rs @ex_intro
 325     [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
 326 qed.
 327
 328 include "turing/if_machine.ma".
 329
 330 (* TEST CHAR
 331
 332    stato finale diverso a seconda che il carattere
 333    corrente soddisfi un test booleano oppure no
 334
 335    q1 = true or no current char
 336    q2 = false
 337 *)
 338
 339 definition tc_states ≝ initN 3.
 340
 341 definition test_char ≝
 342   λalpha:FinSet.λtest:alpha→bool.
 343   mk_TM alpha tc_states
 344   (λp.let 〈q,a〉 ≝ p in
 345    match a with
 346    [ None ⇒ 〈1, None ?〉
 347    | Some a' ⇒
 348      match test a' with
 349      [ true ⇒ 〈1,None ?〉
 350      | false ⇒ 〈2,None ?〉 ]])
 351   O (λx.notb (x == 0)).
 352
 353 definition Rtc_true ≝
 354   λalpha,test,t1,t2.
 355    ∀c. current alpha t1 = Some ? c →
 356    test c = true ∧ t2 = t1.
 357
 358 definition Rtc_false ≝
 359   λalpha,test,t1,t2.
 360     ∀c. current alpha t1 = Some ? c →
 361     test c = false ∧ t2 = t1.
 362
 363 lemma tc_q0_q1 :
 364   ∀alpha,test,ls,a0,rs. test a0 = true →
 365   step alpha (test_char alpha test)
 366     (mk_config ?? 0 (midtape … ls a0 rs)) =
 367   mk_config alpha (states ? (test_char alpha test)) 1
 368     (midtape … ls a0 rs).
 369 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
 370 qed.
 371
 372 lemma tc_q0_q2 :
 373   ∀alpha,test,ls,a0,rs. test a0 = false →
 374   step alpha (test_char alpha test)
 375     (mk_config ?? 0 (midtape … ls a0 rs)) =
 376   mk_config alpha (states ? (test_char alpha test)) 2
 377     (midtape … ls a0 rs).
 378 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
 379 qed.
 380
 381 lemma sem_test_char :
 382   ∀alpha,test.
 383   accRealize alpha (test_char alpha test)
 384     1 (Rtc_true alpha test) (Rtc_false alpha test).
 385 #alpha #test *
 386 [ @(ex_intro ?? 2)
 387   @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
 388   [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
 389 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
 390   % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
 391 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
 392   % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
 393 | #ls #c #rs @(ex_intro ?? 2)
 394   cases (true_or_false (test c)) #Htest
 395   [ @(ex_intro ?? (mk_config ?? 1 ?))
 396     [| %
 397       [ %
 398         [ whd in ⊢ (??%?); >tc_q0_q1 //
 399         | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ]
 400       | * #Hfalse @False_ind @Hfalse % ]
 401     ]
 402   | @(ex_intro ?? (mk_config ?? 2 (midtape ? ls c rs)))
 403     %
 404     [ %
 405       [ whd in ⊢ (??%?); >tc_q0_q2 //
 406       | #Hfalse destruct (Hfalse) ]
 407     | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) //
 408     ]
 409   ]
 410 ]
 411 qed.
 412
 413 axiom myalpha : FinSet.
 414 axiom is_bar : FinProd … myalpha FinBool → bool.
 415 axiom is_grid : FinProd … myalpha FinBool → bool.
 416 definition bar_or_grid ≝ λc.is_bar c ∨ is_grid c.
 417 axiom bar : FinProd … myalpha FinBool.
 418 axiom grid : FinProd … myalpha FinBool.
 419
 420 definition mark_next_tuple ≝
 421   seq ? (adv_to_mark_r ? bar_or_grid)
 422      (ifTM ? (test_char ? is_bar)
 423        (mark ?) (nop ?) 1).
 424
 425 definition R_mark_next_tuple ≝
 426   λt1,t2.
 427     ∀ls,c,rs1,rs2.
 428     (* c non può essere un separatore ... speriamo *)
 429     t1 = midtape ? ls c (rs1@grid::rs2) →
 430     memb ? grid rs1 = false → bar_or_grid c = false →
 431     (∃rs3,rs4,d,b.rs1 = rs3 @ bar :: rs4 ∧
 432       memb ? bar rs3 = false ∧
 433       Some ? 〈d,b〉 = option_hd ? (rs4@grid::rs2) ∧
 434       t2 = midtape ? (bar::reverse ? rs3@c::ls) 〈d,true〉 (tail ? (rs4@grid::rs2)))
 435     ∨
 436     (memb ? bar rs1 = false ∧
 437      t2 = midtape ? (reverse ? rs1@c::ls) grid rs2).
 438
 439 axiom tech_split :
 440   ∀A:DeqSet.∀f,l.
 441    (∀x.memb A x l = true → f x = false) ∨
 442    (∃l1,c,l2.f c = true ∧ l = l1@c::l2 ∧ ∀x.memb ? x l1 = true → f c = false).
 443 (*#A #f #l elim l
 444 [ % #x normalize #Hfalse *)
 445
 446 theorem sem_mark_next_tuple :
 447   Realize ? mark_next_tuple R_mark_next_tuple.
 448 #intape
 449 lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid)
 450          (ifTM ? (test_char ? is_bar) (mark ?) (nop ?) 1) ????)
 451 [@sem_if //
 452 | //
 453 |||#Hif cases (Hif intape) -Hif
 454    #j * #outc * #Hloop * #ta * #Hleft #Hright
 455    @(ex_intro ?? j) @ex_intro [|% [@Hloop] ]
 456    -Hloop
 457    #ls #c #rs1 #rs2 #Hrs #Hrs1 #Hc
 458    cases (Hleft … Hrs)
 459    [ * #Hfalse >Hfalse in Hc; #Htf destruct (Htf)
 460    | * #_ #Hta cases (tech_split ? is_bar rs1)
 461      [ #H1 lapply (Hta rs1 grid rs2 (refl ??) ? ?)
 462        [ (* Hrs1, H1 *) @daemon
 463        | (* bar_or_grid grid = true *) @daemon
 464        | -Hta #Hta cases Hright
 465          [ * #tb * whd in ⊢ (%→?); #Hcurrent
 466            @False_ind cases(Hcurrent grid ?)
 467            [ #Hfalse (* grid is not a bar *) @daemon
 468            | >Hta % ]
 469          | * #tb * whd in ⊢ (%→?); #Hcurrent
 470            cases (Hcurrent grid ?)
 471            [  #_ #Htb whd in ⊢ (%→?); #Houtc
 472              %2 %
 473              [ (* H1 *) @daemon
 474              | >Houtc >Htb >Hta % ]
 475            | >Hta % ]
 476          ]
 477        ]
 478     | * #rs3 * #c0 * #rs4 * * #Hc0 #Hsplit #Hrs3
 479       % @(ex_intro ?? rs3) @(ex_intro ?? rs4)
 480      lapply (Hta rs3 c0 (rs4@grid::rs2) ???)
 481      [ #x #Hrs3' (* Hrs1, Hrs3, Hsplit *) @daemon
 482      | (* bar → bar_or_grid *) @daemon
 483      | >Hsplit >associative_append % ] -Hta #Hta
 484        cases Hright
 485        [ * #tb * whd in ⊢ (%→?); #Hta'
 486          whd in ⊢ (%→?); #Htb
 487          cases (Hta' c0 ?)
 488          [ #_ #Htb' >Htb' in Htb; #Htb
 489            generalize in match Hsplit; -Hsplit
 490            cases rs4 in Hta;
 491            [ >(eq_pair_fst_snd … grid)
 492              #Hta #Hsplit >(Htb … Hta)
 493              >(?:c0 = bar)
 494              [ @(ex_intro ?? (\fst grid)) @(ex_intro ?? (\snd grid))
 495                % [ % [ % [ (* Hsplit *) @daemon |(*Hrs3*) @daemon ] | % ] | % ]
 496                      | (* Hc0 *) @daemon ]
 497            | #r5 #rs5 >(eq_pair_fst_snd … r5)
 498              #Hta #Hsplit >(Htb … Hta)
 499              >(?:c0 = bar)
 500              [ @(ex_intro ?? (\fst r5)) @(ex_intro ?? (\snd r5))
 501                % [ % [ % [ (* Hc0, Hsplit *) @daemon | (*Hrs3*) @daemon ] | % ]
 502                      | % ] | (* Hc0 *) @daemon ] ] | >Hta % ]
 503              | * #tb * whd in ⊢ (%→?); #Hta'
 504                whd in ⊢ (%→?); #Htb
 505                cases (Hta' c0 ?)
 506                [ #Hfalse @False_ind >Hfalse in Hc0;
 507                  #Hc0 destruct (Hc0)
 508                | >Hta % ]
 509 ]]]]
 510 qed.