---

Step * 1 of Lemma prec-sub+-size

.....antecedent..... 
1. P : Type
2. a : Atom ⟶ P ⟶ ((P + P + Type) List)
3. j : P
4. x : prec(lbl,p.a[lbl;p];j)
5. i : P
6. y : prec(lbl,p.a[lbl;p];i)
7. prec_sub+(P;lbl,p.a[lbl;p]) <j, x> <i, y>
⊢ Trans(i:P × prec(lbl,p.a[lbl;p];i))(λu,v. let j,x = u in let i,y = v in ||j;x|| < ||i;y||[_1;_2])
BY
{ (RepeatFor 3 (((D 0 THENW Auto) THEN D -1)) THEN RepUR ``so_apply`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  P  :  Type
2.  a  :  Atom  {}\mrightarrow{}  P  {}\mrightarrow{}  ((P  +  P  +  Type)  List)
3.  j  :  P
4.  x  :  prec(lbl,p.a[lbl;p];j)
5.  i  :  P
6.  y  :  prec(lbl,p.a[lbl;p];i)
7.  prec\_sub+(P;lbl,p.a[lbl;p])  <j,  x>  <i,  y>
\mvdash{}  Trans(i:P  \mtimes{}  prec(lbl,p.a[lbl;p];i))(\mlambda{}u,v.  let  j,x  =  u  in  let  i,y  =  v  in  ||j;x||  <  ||i;y||[$\mbackslash{}ff\000C5f{1}$;$_{2}$])


By

---

Latex:
(RepeatFor  3  (((D  0  THENW  Auto)  THEN  D  -1))  THEN  RepUR  ``so\_apply``  0  THEN  Auto)

---

Home Index