Step
*
1
1
2
of Lemma
intlex-aux-antisym
1. u : ℤ
2. v : ℤ List
3. ∀[l2:{as:ℤ List| ||as|| = ||v|| ∈ ℤ} ]
(v = l2 ∈ (ℤ List)) supposing (intlex-aux(l2;v) = tt and intlex-aux(v;l2) = tt)
4. u1 : ℤ
5. v1 : ℤ List
6. (||v1|| + 1) = (||v|| + 1) ∈ ℤ
7. if u=u1 then intlex-aux(v;v1) else (inr Ax ) = tt
8. inl Ax = tt
9. 0 ≤ ||v||
10. ¬u < u1
11. u1 < u
⊢ [u / v] = [u1 / v1] ∈ (ℤ List)
BY
{ ((Assert ¬(u = u1 ∈ ℤ) BY Auto) THEN All Reduce THEN Auto) }
Latex:
Latex:
1. u : \mBbbZ{}
2. v : \mBbbZ{} List
3. \mforall{}[l2:\{as:\mBbbZ{} List| ||as|| = ||v||\} ]
(v = l2) supposing (intlex-aux(l2;v) = tt and intlex-aux(v;l2) = tt)
4. u1 : \mBbbZ{}
5. v1 : \mBbbZ{} List
6. (||v1|| + 1) = (||v|| + 1)
7. if u=u1 then intlex-aux(v;v1) else (inr Ax ) = tt
8. inl Ax = tt
9. 0 \mleq{} ||v||
10. \mneg{}u < u1
11. u1 < u
\mvdash{} [u / v] = [u1 / v1]
By
Latex:
((Assert \mneg{}(u = u1) BY Auto) THEN All Reduce THEN Auto)
Home
Index