---

Step * 1 1 of Lemma insert-int-comm


1. a : ℤ
2. b : ℤ
⊢ if a <z b then [a / insert-int(b;[])] else [b; a] fi 
= if b <z a then [b / insert-int(a;[])] else [a; b] fi 
∈ (ℤ List)
BY
{ (Reduce 0 THEN RepeatFor 2 (AutoSplit)) }

1
1. a : ℤ
2. b : ℤ
3. ¬b < a
4. ¬a < b
⊢ [b; a] = [a; b] ∈ (ℤ List)

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
\mvdash{}  if  a  <z  b  then  [a  /  insert-int(b;[])]  else  [b;  a]  fi 
=  if  b  <z  a  then  [b  /  insert-int(a;[])]  else  [a;  b]  fi 


By

---

Latex:
(Reduce  0  THEN  RepeatFor  2  (AutoSplit))

---

Home Index