Step * 1 4 of Lemma intlex-aux-transitive


1. : ℤ
2. : ℤ 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
BY
(((Decide ⌜u1 u2 ∈ ℤ⌝⋅ THENA Auto) THEN (Decide ⌜u1 ∈ ℤ⌝⋅ THENA Auto)) THEN All Reduce THEN Auto) }


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  intlex-aux(v;v1)  else  (inr  Ax  )  =  tt
11.  if  u1=u2  then  intlex-aux(v1;v2)  else  (inr  Ax  )  =  tt
12.  0  \mleq{}  ||v||
13.  \mneg{}u  <  u1
14.  \mneg{}u1  <  u2
\mvdash{}  if  (u)  <  (u2)    then  inl  Ax    else  if  u=u2  then  intlex-aux(v;v2)  else  (inr  Ax  )  =  tt


By


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




Home Index