matita/matita/broken_lib/turing/multi_to_mono/multi_to_mono.ma

   1 include "turing/auxiliary_machines1.ma".
   2 include "turing/multi_to_mono/shift_trace_machines.ma".
   3
   4 (******************************************************************************)
   5 (* mtiL: complete move L for tape i. We reaching the left border of trace i,  *)
   6 (* add a blank if there is no more tape, then move the i-trace and finally    *)
   7 (* come back to the head position.                                            *)
   8 (******************************************************************************)
   9
  10 (* we say that a tape is regular if for any trace after the first blank we
  11   only have other blanks *)
  12
  13 definition all_blanks_in ≝ λsig,l.
  14   ∀x. mem ? x l → x = blank sig.
  15
  16 definition regular_i  ≝ λsig,n.λl:list (multi_sig sig n).λi.
  17   all_blanks_in ? (after_blank ? (trace sig n i l)).
  18
  19 definition regular_trace ≝ λsig,n,a.λls,rs:list (multi_sig sig n).λi.
  20   Or (And (regular_i sig n (a::ls) i) (regular_i sig n rs i))
  21      (And (regular_i sig n ls i) (regular_i sig n (a::rs) i)).
  22
  23 axiom regular_tail: ∀sig,n,l,i.
  24   regular_i sig n l i → regular_i sig n (tail ? l) i.
  25
  26 axiom regular_extend: ∀sig,n,l,i.
  27    regular_i sig n l i → regular_i sig n (l@[all_blank sig n]) i.
  28
  29 axiom all_blank_after_blank: ∀sig,n,l1,b,l2,i.
  30   nth i ? (vec … b) (blank ?) = blank ? →
  31   regular_i sig n (l1@b::l2) i → all_blanks_in ? (trace sig n i l2).
  32
  33 lemma regular_trace_extl:  ∀sig,n,a,ls,rs,i.
  34   regular_trace sig n a ls rs i →
  35     regular_trace sig n a (ls@[all_blank sig n]) rs i.
  36 #sig #n #a #ls #rs #i *
  37   [* #H1 #H2 % % // @(regular_extend … H1)
  38   |* #H1 #H2 %2 % // @(regular_extend … H1)
  39   ]
  40 qed.
  41
  42 lemma regular_cons_hd_rs: ∀sig,n.∀a:multi_sig sig n.∀ls,rs1,rs2,i.
  43   regular_trace sig n a ls (rs1@rs2) i →
  44     regular_trace sig n a ls (rs1@((hd ? rs2 (all_blank …))::(tail ? rs2))) i.
  45 #sig #n #a #ls #rs1 #rs2 #i cases rs2 [2: #b #tl #H @H]
  46 *[* #H1 >append_nil #H2 %1 %
  47    [@H1 | whd in match (hd ???); @(regular_extend … rs1) //]
  48  |* #H1 >append_nil #H2 %2 %
  49    [@H1 | whd in match (hd ???); @(regular_extend … (a::rs1)) //]
  50  ]
  51 qed.
  52
  53 lemma eq_trace_to_regular : ∀sig,n.∀a1,a2:multi_sig sig n.∀ls1,ls2,rs1,rs2,i.
  54    nth i ? (vec … a1) (blank ?) = nth i ? (vec … a2) (blank ?) →
  55    trace sig n i ls1 = trace sig n i ls2 →
  56    trace sig n i rs1 = trace sig n i rs2 →
  57    regular_trace sig n a1 ls1 rs1 i →
  58      regular_trace sig n a2 ls2 rs2 i.
  59 #sig #n #a1 #a2 #ls1 #ls2 #rs1 #rs2 #i #H1 #H2 #H3 #H4
  60 whd in match (regular_trace ??????); whd in match (regular_i ????);
  61 whd in match (regular_i ?? rs2 ?); whd in match (regular_i ?? ls2 ?);
  62 whd in match (regular_i ?? (a2::rs2) ?); whd in match (trace ????);
  63 <trace_def whd in match (trace ??? (a2::rs2)); <trace_def
  64 <H1 <H2 <H3 @H4
  65 qed.
  66
  67 (******************************* move_to_blank_L ******************************)
  68 (* we compose machines together to reduce the number of output cases, and
  69    improve semantics *)
  70
  71 definition move_to_blank_L ≝ λsig,n,i.
  72   (move_until ? L (no_blank sig n i)) · extend ? (all_blank sig n).
  73
  74 (*
  75 definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
  76 (current ? t1 = None ? →
  77   t2 = midtape (multi_sig sig n) (left ? t1) (all_blank …) (right ? t1)) ∧
  78 ∀ls,a,rs.t1 = midtape ? ls a rs →
  79   ((no_blank sig n i a = false) ∧ t2 = t1) ∨
  80   (∃b,ls1,ls2.
  81     (no_blank sig n i b = false) ∧
  82     (∀j.j ≤n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j ls) ∧
  83     t2 = midtape ? ls2 b ((reverse ? (a::ls1))@rs)).
  84 *)
  85
  86 definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
  87 (current ? t1 = None ? →
  88   t2 = midtape (multi_sig sig n) (left ? t1) (all_blank …) (right ? t1)) ∧
  89 ∀ls,a,rs.
  90   t1 = midtape (multi_sig sig n) ls a rs →
  91   regular_i sig n (a::ls) i →
  92   (∀j. j ≠ i → regular_trace … a ls rs j) →
  93   (∃b,ls1,ls2.
  94     (regular_i sig n (ls1@b::ls2) i) ∧
  95     (∀j. j ≠ i → regular_trace …
  96       (hd ? (ls1@b::ls2) (all_blank …)) (tail ? (ls1@b::ls2)) rs j) ∧
  97     (no_blank sig n i b = false) ∧
  98     (hd (multi_sig sig n) (ls1@[b]) (all_blank …) = a) ∧ (* not implied by the next fact *)
  99     (∀j.j ≤n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j (a::ls)) ∧
 100     t2 = midtape ? ls2 b ((reverse ? ls1)@rs)).
 101
 102 theorem sem_move_to_blank_L: ∀sig,n,i.
 103   move_to_blank_L sig n i  ⊨ R_move_to_blank_L sig n i.
 104 #sig #n #i
 105 @(sem_seq_app ??????
 106   (ssem_move_until_L ? (no_blank sig n i)) (sem_extend ? (all_blank sig n)))
 107 #tin #tout * #t1 * * #Ht1a #Ht1b * #Ht2a #Ht2b %
 108   [#Hcur >(Ht1a Hcur) in Ht2a; /2 by /
 109   |#ls #a #rs #Htin #Hreg #Hreg2 -Ht1a cases (Ht1b … Htin)
 110     [* #Hnb #Ht1 -Ht1b -Ht2a >Ht1 in Ht2b; >Htin #H
 111      %{a} %{[ ]} %{ls}
 112      %[%[%[%[%[@Hreg|@Hreg2]|@Hnb]|//]|//]|@H normalize % #H1 destruct (H1)]
 113     |*
 114     [(* we find the blank *)
 115      * #ls1 * #b * #ls2 * * * #H1 #H2 #H3 #Ht1
 116      >Ht1 in Ht2b; #Hout -Ht1b
 117      %{b} %{(a::ls1)} %{ls2}
 118      %[%[%[%[%[>H1 in Hreg; #H @H
 119               |#j #jneqi whd in match (hd ???); whd in match (tail ??);
 120                <H1 @(Hreg2 j jneqi)]|@H2] |//]|>H1 //]
 121       |@Hout normalize % normalize #H destruct (H)
 122       ]
 123     |* #b * #lss * * #H1 #H2 #Ht1 -Ht1b >Ht1 in Ht2a;
 124      whd in match (left ??); whd in match (right ??); #Hout
 125      %{(all_blank …)} %{(lss@[b])} %{[]}
 126      %[%[%[%[%[<H2 @regular_extend //
 127               |<H2 #j #jneqi whd in match (hd ???); whd in match (tail ??);
 128                @regular_trace_extl @Hreg2 //]
 129             |whd in match (no_blank ????); >blank_all_blank //]
 130           |<H2 //]
 131         |#j #lejn <H2 @sym_eq @to_blank_i_ext]
 132       |>reverse_append >reverse_single @Hout normalize //
 133       ]
 134     ]
 135   ]
 136 qed.
 137
 138 (******************************************************************************)
 139
 140 definition shift_i_L ≝ λsig,n,i.
 141    ncombf_r (multi_sig …) (shift_i sig n i) (all_blank sig n) ·
 142    mti sig n i ·
 143    extend ? (all_blank sig n).
 144
 145 definition R_shift_i_L ≝ λsig,n,i,t1,t2.
 146     (∀a,ls,rs.
 147       t1 = midtape ? ls a rs  →
 148       ((∃rs1,b,rs2,a1,rss.
 149         rs = rs1@b::rs2 ∧
 150         nth i ? (vec … b) (blank ?) = (blank ?) ∧
 151         (∀x. mem ? x rs1 → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 152         shift_l sig n i (a::rs1) (a1::rss) ∧
 153         t2 = midtape (multi_sig sig n) ((reverse ? (a1::rss))@ls) b rs2) ∨
 154       (∃b,rss.
 155         (∀x. mem ? x rs → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 156         shift_l sig n i (a::rs) (rss@[b]) ∧
 157         t2 = midtape (multi_sig sig n)
 158           ((reverse ? (rss@[b]))@ls) (all_blank sig n) [ ]))).
 159
 160 definition R_shift_i_L_new ≝ λsig,n,i,t1,t2.
 161   (∀a,ls,rs.
 162    t1 = midtape ? ls a rs  →
 163    ∃rs1,b,rs2,rss.
 164       b = hd ? rs2 (all_blank sig n) ∧
 165       nth i ? (vec … b) (blank ?) = (blank ?) ∧
 166       rs = rs1@rs2 ∧
 167       (∀x. mem ? x rs1 → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 168       shift_l sig n i (a::rs1) rss ∧
 169       t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b (tail ? rs2)).
 170
 171 theorem sem_shift_i_L: ∀sig,n,i. shift_i_L sig n i  ⊨ R_shift_i_L sig n i.
 172 #sig #n #i
 173 @(sem_seq_app ??????
 174   (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
 175    (sem_seq ????? (ssem_mti sig n i)
 176     (sem_extend ? (all_blank sig n))))
 177 #tin #tout * #t1 * * #Ht1a #Ht1b * #t2 * * #Ht2a #Ht2b * #Htout1 #Htout2
 178 #a #ls #rs cases rs
 179   [#Htin %2 %{(shift_i sig n i a (all_blank sig n))} %{[ ]}
 180    %[%[#x @False_ind | @daemon]
 181     |lapply (Ht1a … Htin) -Ht1a -Ht1b #Ht1
 182      lapply (Ht2a … Ht1) -Ht2a -Ht2b #Ht2 >Ht2 in Htout1;
 183      >Ht1 whd in match (left ??); whd in match (right ??); #Htout @Htout //
 184     ]
 185   |#a1 #rs1 #Htin
 186    lapply (Ht1b … Htin) -Ht1a -Ht1b #Ht1
 187    lapply (Ht2b … Ht1) -Ht2a -Ht2b *
 188     [(* a1 is blank *) * #H1 #H2 %1
 189      %{[ ]} %{a1} %{rs1} %{(shift_i sig n i a a1)} %{[ ]}
 190      %[%[%[%[// |//] |#x @False_ind] | @daemon]
 191       |>Htout2 [>H2 >reverse_single @Ht1 |>H2 >Ht1 normalize % #H destruct (H)]
 192       ]
 193     |*
 194     [* #rs10 * #b * #rs2 * #rss * * * * #H1 #H2 #H3 #H4
 195      #Ht2 %1
 196      %{(a1::rs10)} %{b} %{rs2} %{(shift_i sig n i a a1)} %{rss}
 197      %[%[%[%[>H1 //|//] |@H3] |@daemon ]
 198       |>reverse_cons >associative_append
 199        >H2 in Htout2; #Htout >Htout [@Ht2| >Ht2 normalize % #H destruct (H)]
 200       ]
 201     |* #b * #rss * * #H1 #H2
 202      #Ht2 %2
 203      %{(shift_i sig n i b (all_blank sig n))} %{(shift_i sig n i a a1::rss)}
 204      %[%[@H1 |@daemon ]
 205       |>Ht2 in Htout1; #Htout >Htout //
 206        whd in match (left ??); whd in match (right ??);
 207        >reverse_append >reverse_single >associative_append  >reverse_cons
 208        >associative_append //
 209        ]
 210      ]
 211    ]
 212  ]
 213 qed.
 214
 215 theorem sem_shift_i_L_new: ∀sig,n,i.
 216   shift_i_L sig n i  ⊨ R_shift_i_L_new sig n i.
 217 #sig #n #i
 218 @(Realize_to_Realize … (sem_shift_i_L sig n i))
 219 #t1 #t2 #H #a #ls #rs #Ht1 lapply (H a ls rs Ht1) *
 220   [* #rs1 * #b * #rs2 * #a1 * #rss * * * * #H1 #H2 #H3 #H4 #Ht2
 221    %{rs1} %{b} %{(b::rs2)} %{(a1::rss)}
 222    %[%[%[%[%[//|@H2]|@H1]|@H3]|@H4] | whd in match (tail ??); @Ht2]
 223   |* #b * #rss * * #H1 #H2 #Ht2
 224    %{rs} %{(all_blank sig n)} %{[]} %{(rss@[b])}
 225    %[%[%[%[%[//|@blank_all_blank]|//]|@H1]|@H2] | whd in match (tail ??); @Ht2]
 226   ]
 227 qed.
 228
 229
 230 (*******************************************************************************
 231 The following machine implements a full move of for a trace: we reach the left
 232 border, shift the i-th trace and come back to the head position. *)
 233
 234 (* this exclude the possibility that traces do not overlap: the head must
 235 remain inside all traces *)
 236
 237 definition mtiL ≝ λsig,n,i.
 238    move_to_blank_L sig n i ·
 239    shift_i_L sig n i ·
 240    move_until ? L (no_head sig n).
 241
 242 definition Rmtil ≝ λsig,n,i,t1,t2.
 243   ∀ls,a,rs.
 244    t1 = midtape (multi_sig sig n) ls a rs →
 245    nth n ? (vec … a) (blank ?) = head ? →
 246    (∀i.regular_trace sig n a ls rs i) →
 247    (* next: we cannot be on rightof on trace i *)
 248    (nth i ? (vec … a) (blank ?) = (blank ?)
 249      → nth i ? (vec … (hd ? rs (all_blank …))) (blank ?) ≠ (blank ?)) →
 250    no_head_in … ls →
 251    no_head_in … rs  →
 252    (∃ls1,a1,rs1.
 253      t2 = midtape (multi_sig …) ls1 a1 rs1 ∧
 254      (∀i.regular_trace … a1 ls1 rs1 i) ∧
 255      (∀j. j ≤ n → j ≠ i → to_blank_i ? n j (a1::ls1) = to_blank_i ? n j (a::ls)) ∧
 256      (∀j. j ≤ n → j ≠ i → to_blank_i ? n j rs1 = to_blank_i ? n j rs) ∧
 257      (to_blank_i ? n i ls1 = to_blank_i ? n i (a::ls)) ∧
 258      (to_blank_i ? n i (a1::rs1)) = to_blank_i ? n i rs).
 259
 260 theorem sem_Rmtil: ∀sig,n,i. i < n → mtiL sig n i  ⊨ Rmtil sig n i.
 261 #sig #n #i #lt_in
 262 @(sem_seq_app ??????
 263   (sem_move_to_blank_L … )
 264    (sem_seq ????? (sem_shift_i_L_new …)
 265     (ssem_move_until_L ? (no_head sig n))))
 266 #tin #tout * #t1 * * #_ #Ht1 * #t2 * #Ht2 * #_ #Htout
 267 (* we start looking into Rmitl *)
 268 #ls #a #rs #Htin (* tin is a midtape *)
 269 #Hhead #Hreg #no_rightof #Hnohead_ls #Hnohead_rs
 270 cut (regular_i sig n (a::ls) i)
 271   [cases (Hreg i) * //
 272    cases (true_or_false (nth i ? (vec … a) (blank ?) == (blank ?))) #Htest
 273     [#_ @daemon (* absurd, since hd rs non e' blank *)
 274     |#H #_ @daemon]] #Hreg1
 275 lapply (Ht1 … Htin Hreg1 ?) [#j #_ @Hreg] -Ht1 -Htin
 276 * #b * #ls1 * #ls2 * * * * * #reg_ls1_i #reg_ls1_j #Hno_blankb #Hhead #Hls1 #Ht1
 277 lapply (Ht2 … Ht1) -Ht2 -Ht1
 278 * #rs1 * #b0 * #rs2 * #rss * * * * * #Hb0 #Hb0blank #Hrs1 #Hrs1b #Hrss #Ht2
 279 (* we need to recover the position of the head of the emulated machine
 280    that is the head of ls1. This is somewhere inside rs1 *)
 281 cut (∃rs11. rs1 = (reverse ? ls1)@rs11)
 282   [cut (ls1 = [ ] ∨ ∃aa,tlls1. ls1 = aa::tlls1)
 283     [cases ls1 [%1 // | #aa #tlls1 %2 %{aa} %{tlls1} //]] *
 284       [#H1ls1 %{rs1} >H1ls1 //
 285       |* #aa * #tlls1 #H1ls1 >H1ls1 in Hrs1;
 286        cut (aa = a) [>H1ls1 in Hls1; #H @(to_blank_hd … H)] #eqaa >eqaa
 287        #Hrs1_aux cases (compare_append … (sym_eq … Hrs1_aux)) #l *
 288         [* #H1 #H2 %{l} @H1
 289         |(* this is absurd : if l is empty, the case is as before.
 290            if l is not empty then it must start with a blank, since it is the
 291            first character in rs2. But in this case we would have a blank
 292            inside ls1=a::tls1 that is absurd *)
 293           @daemon
 294         ]]]
 295    * #rs11 #H1
 296 cut (rs = rs11@rs2)
 297   [@(injective_append_l … (reverse … ls1)) >Hrs1 <associative_append <H1 //] #H2
 298 lapply (Htout … Ht2) -Htout -Ht2 *
 299   [(* the current character on trace i holds the head-mark.
 300       The case is absurd, since b0 is the head of rs2, that is a sublist of rs,
 301       and the head-mark is not in rs *)
 302    * #H3 @False_ind @(absurd (nth n ? (vec … b0) (blank sig) = head ?))
 303      [@(\P ?) @injective_notb @H3 ]
 304    @Hnohead_rs >H2 >trace_append @mem_append_l2
 305    lapply Hb0 cases rs2
 306     [whd in match (hd ???); #H >H in H3; whd in match (no_head ???);
 307      >all_blank_n normalize -H #H destruct (H); @False_ind
 308     |#c #r #H4 %1 >H4 //
 309     ]
 310   |*
 311   [(* we reach the head position *)
 312    (* cut (trace sig n j (a1::ls20)=trace sig n j (ls1@b::ls2)) *)
 313    * #ls10 * #a1 * #ls20 * * * #Hls20 #Ha1 #Hnh #Htout
 314    cut (∀j.j ≠ i →
 315       trace sig n j (reverse (multi_sig sig n) rs1@b::ls2) =
 316       trace sig n j (ls10@a1::ls20))
 317     [#j #ineqj >append_cons <reverse_cons >trace_def <map_append <reverse_map
 318      lapply (trace_shift_neq …lt_in ? (sym_not_eq … ineqj) … Hrss) [//] #Htr
 319      <(trace_def …  (b::rs1)) <Htr >reverse_map >map_append @eq_f @Hls20 ]
 320    #Htracej
 321    cut (trace sig n i (reverse (multi_sig sig n) (rs1@[b0])@ls2) =
 322         trace sig n i (ls10@a1::ls20))
 323     [>trace_def <map_append <reverse_map <map_append <(trace_def … [b0])
 324      cut (trace sig n i [b0] = [blank ?]) [@daemon] #Hcut >Hcut
 325      lapply (trace_shift … lt_in … Hrss) [//] whd in match (tail ??); #Htr <Htr
 326      >reverse_map >map_append <trace_def <Hls20 %
 327     ]
 328    #Htracei
 329    cut (∀j. j ≠ i →
 330       (trace sig n j (reverse (multi_sig sig n) rs11) = trace sig n j ls10) ∧
 331       (trace sig n j (ls1@b::ls2) = trace sig n j (a1::ls20)))
 332    [@daemon (* si fa
 333      #j #ineqj @(first_P_to_eq ? (λx. x ≠ head ?))
 334       [lapply (Htracej … ineqj) >trace_def in ⊢ (%→?); <map_append
 335        >trace_def in ⊢ (%→?); <map_append #H @H
 336       | *) ] #H2
 337   cut ((trace sig n i (b0::reverse ? rs11) = trace sig n i (ls10@[a1])) ∧
 338       (trace sig n i (ls1@ls2) = trace sig n i ls20))
 339    [>H1 in Htracei; >reverse_append >reverse_single >reverse_append
 340      >reverse_reverse >associative_append >associative_append
 341      @daemon
 342     ] #H3
 343   cut (∀j. j ≠ i →
 344     trace sig n j (reverse (multi_sig sig n) ls10@rs2) = trace sig n j rs)
 345     [#j #jneqi @(injective_append_l … (trace sig n j (reverse ? ls1)))
 346      >map_append >map_append >Hrs1 >H1 >associative_append
 347      <map_append <map_append in ⊢ (???%); @eq_f
 348      <map_append <map_append @eq_f2 // @sym_eq
 349      <(reverse_reverse … rs11) <reverse_map <reverse_map in ⊢ (???%);
 350      @eq_f @(proj1 … (H2 j jneqi))] #Hrs_j
 351    %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail (multi_sig sig n) rs2)}
 352    %[%[%[%[%[@Htout
 353     |#j cases (decidable_eq_nat j i)
 354       [#eqji >eqji (* by cases wether a1 is blank *)
 355        @daemon
 356       |#jneqi lapply (reg_ls1_j … jneqi) #H4
 357        >reverse_cons >associative_append >Hb0 @regular_cons_hd_rs
 358        @(eq_trace_to_regular … H4)
 359         [<hd_trace >(proj2 … (H2 … jneqi)) >hd_trace %
 360         |<tail_trace >(proj2 … (H2 … jneqi)) >tail_trace %
 361         |@sym_eq @Hrs_j //
 362         ]
 363       ]]
 364     |#j #lejn #jneqi <(Hls1 … lejn)
 365      >to_blank_i_def >to_blank_i_def @eq_f @sym_eq @(proj2 … (H2 j jneqi))]
 366     |#j #lejn #jneqi >reverse_cons >associative_append >Hb0
 367      <to_blank_hd_cons >to_blank_i_def >to_blank_i_def @eq_f @Hrs_j //]
 368     |<(Hls1 i) [2:@lt_to_le //]
 369      lapply (all_blank_after_blank … reg_ls1_i)
 370        [@(\P ?) @daemon] #allb_ls2
 371      whd in match (to_blank_i ????); <(proj2 … H3)
 372      @daemon ]
 373     |>reverse_cons >associative_append
 374      cut (to_blank_i sig n i rs = to_blank_i sig n i (rs11@[b0])) [@daemon]
 375      #Hcut >Hcut >(to_blank_i_chop  … b0 (a1::reverse …ls10)) [2: @Hb0blank]
 376      >to_blank_i_def >to_blank_i_def @eq_f
 377      >trace_def >trace_def @injective_reverse >reverse_map >reverse_cons
 378      >reverse_reverse >reverse_map >reverse_append >reverse_single @sym_eq
 379      @(proj1 … H3)
 380     ]
 381   |(*we do not find the head: this is absurd *)
 382    * #b1 * #lss * * #H2 @False_ind
 383    cut (∀x0. mem ? x0 (trace sig n n (b0::reverse ? rss@ls2)) → x0 ≠ head ?)
 384      [@daemon] -H2 #H2
 385    lapply (trace_shift_neq sig n i n … lt_in … Hrss)
 386      [@lt_to_not_eq @lt_in | // ]
 387    #H3 @(absurd
 388         (nth n ? (vec … (hd ? (ls1@[b]) (all_blank sig n))) (blank ?) = head ?))
 389      [>Hhead //
 390      |@H2 >trace_def %2 <map_append @mem_append_l1 <reverse_map <trace_def
 391       >H3 >H1 >trace_def >reverse_map >reverse_cons >reverse_append
 392       >reverse_reverse >associative_append <map_append @mem_append_l2
 393       cases ls1 [%1 % |#x #ll %1 %]
 394      ]
 395    ]
 396  ]
 397 qed.