---

Step * of Lemma ml_merge_int-sq

∀[bs,as:ℤ List].  (ml_merge_int(as;bs) ~ merge-int(as;bs))
BY
{ (((Assert ℤ BY (UseWitness ⌜0⌝⋅ THEN Auto)) THEN Auto)
   THEN RepUR ``ml_merge_int merge-int ml_apply`` 0
   THEN (CallByValueReduceOn ⌜bs⌝ 0⋅ THENA Auto)
   THEN (CallByValueReduceOn ⌜as⌝ 0⋅ THENA Auto)
   THEN Reduce 0
   THEN UseWitness ⌜Ax⌝⋅
   THEN MemCD
   THEN Fold `ml_apply` 0) }

1
1. ℤ
2. bs : ℤ List
3. as : ℤ List
⊢ ml-reduce(fix((λinsert_int,x,l. if null(l)
                                 then [x]
                                 else let a.as = l 
                                      in if x <z a + 1 then [x / l] else [a / insert_int(x)(as)] fi 
                                 fi ));as;bs)
= reduce(λb,l. insert-int(b;l);as;bs)
∈ (ℤ List)

---

Latex:

---

Latex:
\mforall{}[bs,as:\mBbbZ{}  List].    (ml\_merge\_int(as;bs)  \msim{}  merge-int(as;bs))


By

---

Latex:
(((Assert  \mBbbZ{}  BY  (UseWitness  \mkleeneopen{}0\mkleeneclose{}\mcdot{}  THEN  Auto))  THEN  Auto)
  THEN  RepUR  ``ml\_merge\_int  merge-int  ml\_apply``  0
  THEN  (CallByValueReduceOn  \mkleeneopen{}bs\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}as\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  MemCD
  THEN  Fold  `ml\_apply`  0)

---

Home Index