---

Step * 2 of Lemma prec-sub+-size


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>
8. x1 : i:P × prec(lbl,p.a[lbl;p];i)
9. y1 : i:P × prec(lbl,p.a[lbl;p];i)
10. x1 prec_sub(P;lbl,p.a[lbl;p]) y1
⊢ x1 (λu,v. let j,x = u in let i,y = v in ||j;x|| < ||i;y||) y1
BY
{ (D -3 THEN D -2 THEN RepUR ``prec_sub`` -1 THEN Reduce 0 THEN EAuto 1) }

---

Latex:

---

Latex:

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>
8.  x1  :  i:P  \mtimes{}  prec(lbl,p.a[lbl;p];i)
9.  y1  :  i:P  \mtimes{}  prec(lbl,p.a[lbl;p];i)
10.  x1  prec\_sub(P;lbl,p.a[lbl;p])  y1
\mvdash{}  x1  (\mlambda{}u,v.  let  j,x  =  u  in  let  i,y  =  v  in  ||j;x||  <  ||i;y||)  y1


By

---

Latex:
(D  -3  THEN  D  -2  THEN  RepUR  ``prec\_sub``  -1  THEN  Reduce  0  THEN  EAuto  1)

---

Home Index