---

Step * 1 of Lemma intlex-aux-transitive


1. u : ℤ
2. v : ℤ List
3. ∀[l2,l3:{as:ℤ List| ||as|| = ||v|| ∈ ℤ} ].
     (intlex-aux(v;l3) = tt) supposing (intlex-aux(l2;l3) = tt and intlex-aux(v;l2) = tt)
4. u1 : ℤ
5. v1 : ℤ List
6. (||v1|| + 1) = (||v|| + 1) ∈ ℤ
7. u2 : ℤ
8. v2 : ℤ List
9. (||v2|| + 1) = (||v|| + 1) ∈ ℤ
10. if (u) < (u1)  then inl Ax  else if u=u1 then intlex-aux(v;v1) else (inr Ax ) = tt
11. if (u1) < (u2)  then inl Ax  else if u1=u2 then intlex-aux(v1;v2) else (inr Ax ) = tt
12. 0 ≤ ||v||
⊢ if (u) < (u2)  then inl Ax  else if u=u2 then intlex-aux(v;v2) else (inr Ax ) = tt
BY
{ (((Decide ⌜u < u1⌝⋅ THENA Auto) THEN All Reduce) THEN (Decide ⌜u1 < u2⌝⋅ THENA Auto) THEN All Reduce) }

1
1. u : ℤ
2. v : ℤ List
3. ∀[l2,l3:{as:ℤ List| ||as|| = ||v|| ∈ ℤ} ].
     (intlex-aux(v;l3) = tt) supposing (intlex-aux(l2;l3) = tt and intlex-aux(v;l2) = tt)
4. u1 : ℤ
5. v1 : ℤ List
6. (||v1|| + 1) = (||v|| + 1) ∈ ℤ
7. u2 : ℤ
8. v2 : ℤ List
9. (||v2|| + 1) = (||v|| + 1) ∈ ℤ
10. inl Ax = tt
11. inl Ax = tt
12. 0 ≤ ||v||
13. u < u1
14. u1 < u2
⊢ if (u) < (u2)  then inl Ax  else if u=u2 then intlex-aux(v;v2) else (inr Ax ) = tt

2
1. u : ℤ
2. v : ℤ List
3. ∀[l2,l3:{as:ℤ List| ||as|| = ||v|| ∈ ℤ} ].
     (intlex-aux(v;l3) = tt) supposing (intlex-aux(l2;l3) = tt and intlex-aux(v;l2) = tt)
4. u1 : ℤ
5. v1 : ℤ List
6. (||v1|| + 1) = (||v|| + 1) ∈ ℤ
7. u2 : ℤ
8. v2 : ℤ List
9. (||v2|| + 1) = (||v|| + 1) ∈ ℤ
10. inl Ax = tt
11. if u1=u2 then intlex-aux(v1;v2) else (inr Ax ) = tt
12. 0 ≤ ||v||
13. u < u1
14. ¬u1 < u2
⊢ if (u) < (u2)  then inl Ax  else if u=u2 then intlex-aux(v;v2) else (inr Ax ) = tt

3
1. u : ℤ
2. v : ℤ List
3. ∀[l2,l3:{as:ℤ List| ||as|| = ||v|| ∈ ℤ} ].
     (intlex-aux(v;l3) = tt) supposing (intlex-aux(l2;l3) = tt and intlex-aux(v;l2) = tt)
4. u1 : ℤ
5. v1 : ℤ List
6. (||v1|| + 1) = (||v|| + 1) ∈ ℤ
7. u2 : ℤ
8. v2 : ℤ List
9. (||v2|| + 1) = (||v|| + 1) ∈ ℤ
10. if u=u1 then intlex-aux(v;v1) else (inr Ax ) = tt
11. inl Ax = tt
12. 0 ≤ ||v||
13. ¬u < u1
14. u1 < u2
⊢ if (u) < (u2)  then inl Ax  else if u=u2 then intlex-aux(v;v2) else (inr Ax ) = tt

4
1. u : ℤ
2. v : ℤ List
3. ∀[l2,l3:{as:ℤ List| ||as|| = ||v|| ∈ ℤ} ].
     (intlex-aux(v;l3) = tt) supposing (intlex-aux(l2;l3) = tt and intlex-aux(v;l2) = tt)
4. u1 : ℤ
5. v1 : ℤ List
6. (||v1|| + 1) = (||v|| + 1) ∈ ℤ
7. u2 : ℤ
8. v2 : ℤ List
9. (||v2|| + 1) = (||v|| + 1) ∈ ℤ
10. if u=u1 then intlex-aux(v;v1) else (inr Ax ) = tt
11. if u1=u2 then intlex-aux(v1;v2) else (inr Ax ) = tt
12. 0 ≤ ||v||
13. ¬u < u1
14. ¬u1 < u2
⊢ if (u) < (u2)  then inl Ax  else if u=u2 then intlex-aux(v;v2) else (inr Ax ) = tt

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}[l2,l3:\{as:\mBbbZ{}  List|  ||as||  =  ||v||\}  ].
          (intlex-aux(v;l3)  =  tt)  supposing  (intlex-aux(l2;l3)  =  tt  and  intlex-aux(v;l2)  =  tt)
4.  u1  :  \mBbbZ{}
5.  v1  :  \mBbbZ{}  List
6.  (||v1||  +  1)  =  (||v||  +  1)
7.  u2  :  \mBbbZ{}
8.  v2  :  \mBbbZ{}  List
9.  (||v2||  +  1)  =  (||v||  +  1)
10.  if  (u)  <  (u1)    then  inl  Ax    else  if  u=u1  then  intlex-aux(v;v1)  else  (inr  Ax  )  =  tt
11.  if  (u1)  <  (u2)    then  inl  Ax    else  if  u1=u2  then  intlex-aux(v1;v2)  else  (inr  Ax  )  =  tt
12.  0  \mleq{}  ||v||
\mvdash{}  if  (u)  <  (u2)    then  inl  Ax    else  if  u=u2  then  intlex-aux(v;v2)  else  (inr  Ax  )  =  tt


By

---

Latex:
(((Decide  \mkleeneopen{}u  <  u1\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Reduce)
  THEN  (Decide  \mkleeneopen{}u1  <  u2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Reduce)

---

Home Index