---

Step * 1 of Lemma ml_merge_int-sq


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)
BY
{ ((Assert ⌜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 ))
            = (λb,l. insert-int(b;l))
            ∈ (ℤ ⟶ (ℤ List) ⟶ (ℤ List))⌝⋅
   THENM (RWO "-1" 0 THEN Auto)
   )
   THEN RepeatFor 2 (((FunExt THENA Auto) THEN Reduce 0))
   THEN Fold `ml_insert_int` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  \mBbbZ{}
2.  bs  :  \mBbbZ{}  List
3.  as  :  \mBbbZ{}  List
\mvdash{}  ml-reduce(fix((\mlambda{}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$_{in\000Ct}$(x)(as)]  fi 
                                                                fi  ));as;bs)
=  reduce(\mlambda{}b,l.  insert-int(b;l);as;bs)


By

---

Latex:
((Assert  \mkleeneopen{}fix((\mlambda{}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\mbackslash{}\000Cff7d$(x)(as)]  fi 
                                                            fi  ))
                    =  (\mlambda{}b,l.  insert-int(b;l))\mkleeneclose{}\mcdot{}
  THENM  (RWO  "-1"  0  THEN  Auto)
  )
  THEN  RepeatFor  2  (((FunExt  THENA  Auto)  THEN  Reduce  0))
  THEN  Fold  `ml\_insert\_int`  0
  THEN  Auto)

---

Home Index