---

Step * 1 of Lemma insert-int-comm

.....assertion..... 
∀L:ℤ List. ∀a,b:ℤ.  (insert-int(b;insert-int(a;L)) = insert-int(a;insert-int(b;L)) ∈ (ℤ List))
BY
{ (InductionOnList THEN Auto THEN Reduce 0 THEN (RWO "insert-int-cons" 0 THENA Auto)) }

1
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)

2
1. u : ℤ
2. v : ℤ List
3. ∀a,b:ℤ.  (insert-int(b;insert-int(a;v)) = insert-int(a;insert-int(b;v)) ∈ (ℤ List))
4. a : ℤ
5. b : ℤ
⊢ insert-int(b;if u <z a then [u / insert-int(a;v)] else [a; [u / v]] fi )
= insert-int(a;if u <z b then [u / insert-int(b;v)] else [b; [u / v]] fi )
∈ (ℤ List)

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}L:\mBbbZ{}  List.  \mforall{}a,b:\mBbbZ{}.    (insert-int(b;insert-int(a;L))  =  insert-int(a;insert-int(b;L)))


By

---

Latex:
(InductionOnList  THEN  Auto  THEN  Reduce  0  THEN  (RWO  "insert-int-cons"  0  THENA  Auto))

---

Home Index