---

Step * of Lemma ml-insert-int-sq

∀[l:ℤ List]. ∀[x:ℤ].  (ml-insert-int(x;l) ~ insert-int(x;l))
BY
{ (InductionOnList
   THEN Intro
   THEN All (RepUR ``ml-insert-int spreadcons ml_apply let``)
   THEN RW (AddrC [1] (SweepUpC UnrollRecursionC)) 0
   THEN Reduce 0
   THEN (CallByValueReduceOn ⌜x⌝ 0⋅ THENA Auto)
   THEN Reduce 0
   THEN (Trivial
   ORELSE ((CallByValueReduce 0⋅ THENA Auto)
           THEN Reduce 0
           THEN ((InstHyp [⌜x⌝] 3⋅ THENA Auto) THEN (CallByValueReduceOn ⌜x⌝ (-1)⋅ THENA Auto))
           THEN HypSubst' (-1) 0)
   )) }

1
1. u : ℤ
2. v : ℤ List
3. ∀[x:ℤ]
     (let y ⟵ v
      in let y ⟵ x
         in 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 / let y ⟵ as in let y ⟵ x in insert_int y y]
                                         fi 
                                 fi )) 
            y 
         y ~ insert-int(x;v))
4. [x] : ℤ
5. let y ⟵ v
   in 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 / let y ⟵ as in let y ⟵ x in insert_int y y] fi 
                           fi )) 
      x 
      y ~ insert-int(x;v)
⊢ if x <z u + 1 then [x; [u / v]] else [u / insert-int(x;v)] fi  ~ insert-int(x;[u / v])

---

Latex:

---

Latex:
\mforall{}[l:\mBbbZ{}  List].  \mforall{}[x:\mBbbZ{}].    (ml-insert-int(x;l)  \msim{}  insert-int(x;l))


By

---

Latex:
(InductionOnList
  THEN  Intro
  THEN  All  (RepUR  ``ml-insert-int  spreadcons  ml\_apply  let``)
  THEN  RW  (AddrC  [1]  (SweepUpC  UnrollRecursionC))  0
  THEN  Reduce  0
  THEN  (CallByValueReduceOn  \mkleeneopen{}x\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  (Trivial
  ORELSE  ((CallByValueReduce  0\mcdot{}  THENA  Auto)
                  THEN  Reduce  0
                  THEN  ((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  3\mcdot{}  THENA  Auto)  THEN  (CallByValueReduceOn  \mkleeneopen{}x\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto))
                  THEN  HypSubst'  (-1)  0)
  ))

---

Home Index