---

Step * 1 of Lemma intlex-transitive


1. l1 : ℤ List
2. l2 : ℤ List
3. l3 : ℤ List
4. ||l1|| <z ||l2|| ∨b((||l1|| =z ||l2||) ∧b intlex-aux(l1;l2)) = tt
5. ||l2|| <z ||l3|| ∨b((||l2|| =z ||l3||) ∧b intlex-aux(l2;l3)) = tt
⊢ ||l1|| <z ||l3|| ∨b((||l1|| =z ||l3||) ∧b intlex-aux(l1;l3)) = tt
BY
{ ((Assert ||l1|| ≤ ||l2|| BY
          (MoveToConcl (-2) THEN AutoBoolCase ⌜||l1|| <z ||l2||⌝⋅ THEN AutoBoolCase ⌜(||l1|| =z ||l2||)⌝⋅))
   THEN (Assert ||l2|| ≤ ||l3|| BY
               (MoveToConcl (-2) THEN AutoBoolCase ⌜||l2|| <z ||l3||⌝⋅ THEN AutoBoolCase ⌜(||l2|| =z ||l3||)⌝⋅))
   ) }

1
1. l1 : ℤ List
2. l2 : ℤ List
3. l3 : ℤ List
4. ||l1|| <z ||l2|| ∨b((||l1|| =z ||l2||) ∧b intlex-aux(l1;l2)) = tt
5. ||l2|| <z ||l3|| ∨b((||l2|| =z ||l3||) ∧b intlex-aux(l2;l3)) = tt
6. ||l1|| ≤ ||l2||
7. ||l2|| ≤ ||l3||
⊢ ||l1|| <z ||l3|| ∨b((||l1|| =z ||l3||) ∧b intlex-aux(l1;l3)) = tt

---

Latex:

---

Latex:

1.  l1  :  \mBbbZ{}  List
2.  l2  :  \mBbbZ{}  List
3.  l3  :  \mBbbZ{}  List
4.  ||l1||  <z  ||l2||  \mvee{}\msubb{}((||l1||  =\msubz{}  ||l2||)  \mwedge{}\msubb{}  intlex-aux(l1;l2))  =  tt
5.  ||l2||  <z  ||l3||  \mvee{}\msubb{}((||l2||  =\msubz{}  ||l3||)  \mwedge{}\msubb{}  intlex-aux(l2;l3))  =  tt
\mvdash{}  ||l1||  <z  ||l3||  \mvee{}\msubb{}((||l1||  =\msubz{}  ||l3||)  \mwedge{}\msubb{}  intlex-aux(l1;l3))  =  tt


By

---

Latex:
((Assert  ||l1||  \mleq{}  ||l2||  BY
                (MoveToConcl  (-2)
                  THEN  AutoBoolCase  \mkleeneopen{}||l1||  <z  ||l2||\mkleeneclose{}\mcdot{}
                  THEN  AutoBoolCase  \mkleeneopen{}(||l1||  =\msubz{}  ||l2||)\mkleeneclose{}\mcdot{}))
  THEN  (Assert  ||l2||  \mleq{}  ||l3||  BY
                          (MoveToConcl  (-2)
                            THEN  AutoBoolCase  \mkleeneopen{}||l2||  <z  ||l3||\mkleeneclose{}\mcdot{}
                            THEN  AutoBoolCase  \mkleeneopen{}(||l2||  =\msubz{}  ||l3||)\mkleeneclose{}\mcdot{}))
  )

---

Home Index