Step
*
2
1
of Lemma
intlex-cons
1. l1 : ℤ List
2. l2 : ℤ List
3. x : ℤ
4. y : ℤ
5. ¬||l1|| < ||l2||
6. ||l1|| = ||l2|| ∈ ℤ
⊢ uiff(↑((||l1|| + 1 =z ||l2|| + 1) ∧b intlex-aux([x / l1];[y / l2]));||l1|| < ||l2||
∨ (x < y ∧ (||l1|| = ||l2|| ∈ ℤ))
∨ ((x = y ∈ ℤ) ∧ (↑((||l1|| =z ||l2||) ∧b intlex-aux(l1;l2)))))
BY
{ (((Subst' (||l1|| =z ||l2||) ~ tt 0 THENA Auto) THEN (Subst' (||l1|| + 1 =z ||l2|| + 1) ~ tt 0 THENA Auto))
THEN Reduce 0
) }
1
1. l1 : ℤ List
2. l2 : ℤ List
3. x : ℤ
4. y : ℤ
5. ¬||l1|| < ||l2||
6. ||l1|| = ||l2|| ∈ ℤ
⊢ uiff(↑intlex-aux([x / l1];[y / l2]);||l1|| < ||l2||
∨ (x < y ∧ (||l1|| = ||l2|| ∈ ℤ))
∨ ((x = y ∈ ℤ) ∧ (↑intlex-aux(l1;l2))))
Latex:
Latex:
1. l1 : \mBbbZ{} List
2. l2 : \mBbbZ{} List
3. x : \mBbbZ{}
4. y : \mBbbZ{}
5. \mneg{}||l1|| < ||l2||
6. ||l1|| = ||l2||
\mvdash{} uiff(\muparrow{}((||l1|| + 1 =\msubz{} ||l2|| + 1) \mwedge{}\msubb{} intlex-aux([x / l1];[y / l2]));||l1|| < ||l2||
\mvee{} (x < y \mwedge{} (||l1|| = ||l2||))
\mvee{} ((x = y) \mwedge{} (\muparrow{}((||l1|| =\msubz{} ||l2||) \mwedge{}\msubb{} intlex-aux(l1;l2)))))
By
Latex:
(((Subst' (||l1|| =\msubz{} ||l2||) \msim{} tt 0 THENA Auto)
THEN (Subst' (||l1|| + 1 =\msubz{} ||l2|| + 1) \msim{} tt 0 THENA Auto)
)
THEN Reduce 0
)
Home
Index