Step
*
1
2
2
of Lemma
insert-int-comm
.....subterm..... T:t
2:n
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. ¬u < a
6. b : ℤ
7. ¬b < a
8. ¬a < b
9. ¬u < b
⊢ [a; [u / v]] = [b; [u / v]] ∈ (ℤ List)
BY
{ (EqCDA THEN Auto) }
Latex:
Latex:
.....subterm..... T:t
2:n
1. u : \mBbbZ{}
2. v : \mBbbZ{} List
3. \mforall{}a,b:\mBbbZ{}. (insert-int(b;insert-int(a;v)) = insert-int(a;insert-int(b;v)))
4. a : \mBbbZ{}
5. \mneg{}u < a
6. b : \mBbbZ{}
7. \mneg{}b < a
8. \mneg{}a < b
9. \mneg{}u < b
\mvdash{} [a; [u / v]] = [b; [u / v]]
By
Latex:
(EqCDA THEN Auto)
Home
Index