---

Step * of Lemma prec-sub+-size

∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[j:P]. ∀[x:prec(lbl,p.a[lbl;p];j)]. ∀[i:P].
∀[y:prec(lbl,p.a[lbl;p];i)].
  ||j;x|| < ||i;y|| supposing prec_sub+(P;lbl,p.a[lbl;p]) <j, x> <i, y>
BY
{ (Auto
   THEN ((InstLemma `rel_plus_closure` [⌜i:P × prec(lbl,p.a[lbl;p];i)⌝;⌜prec_sub(P;lbl,p.a[lbl;p])⌝;
          ⌜λu,v. let j,x = u in let i,y = v in ||j;x|| < ||i;y||⌝]⋅
         THENM (InstHyp [⌜<j, x>⌝;⌜<i, y>⌝] (-1)⋅ THEN Auto)
         )
         THENA Auto
         )
   ) }

1
.....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])

2
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

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[a:Atom  {}\mrightarrow{}  P  {}\mrightarrow{}  ((P  +  P  +  Type)  List)].  \mforall{}[j:P].  \mforall{}[x:prec(lbl,p.a[lbl;p];j)].  \mforall{}[i:P].
\mforall{}[y:prec(lbl,p.a[lbl;p];i)].
    ||j;x||  <  ||i;y||  supposing  prec\_sub+(P;lbl,p.a[lbl;p])  <j,  x>  <i,  y>


By

---

Latex:
(Auto
  THEN  ((InstLemma  `rel\_plus\_closure`  [\mkleeneopen{}i:P  \mtimes{}  prec(lbl,p.a[lbl;p];i)\mkleeneclose{};\mkleeneopen{}prec\_sub(P;lbl,p.a[lbl;p])\mkleeneclose{};
                \mkleeneopen{}\mlambda{}u,v.  let  j,x  =  u  in  let  i,y  =  v  in  ||j;x||  <  ||i;y||\mkleeneclose{}]\mcdot{}
              THENM  (InstHyp  [\mkleeneopen{}<j,  x>\mkleeneclose{};\mkleeneopen{}<i,  y>\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
              )
              THENA  Auto
              )
  )

---

Home Index