---

Step * 2 2 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||) ~ ff 0 THENA Auto) THEN (Subst' (||l1|| + 1 =z ||l2|| + 1) ~ ff 0 THENA Auto))
   THEN Reduce 0
   THEN Auto) }

1
1. l1 : ℤ List
2. l2 : ℤ List
3. x : ℤ
4. y : ℤ
5. ¬||l1|| < ||l2||
6. ¬(||l1|| = ||l2|| ∈ ℤ)
7. (x < y ∧ (||l1|| = ||l2|| ∈ ℤ)) ∨ ((x = y ∈ ℤ) ∧ False)
⊢ False

---

Latex:

---

Latex:

1.  l1  :  \mBbbZ{}  List
2.  l2  :  \mBbbZ{}  List
3.  x  :  \mBbbZ{}
4.  y  :  \mBbbZ{}
5.  \mneg{}||l1||  <  ||l2||
6.  \mneg{}(||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{}  ff  0  THENA  Auto)
    THEN  (Subst'  (||l1||  +  1  =\msubz{}  ||l2||  +  1)  \msim{}  ff  0  THENA  Auto)
    )
  THEN  Reduce  0
  THEN  Auto)

---

Home Index