---

Step * 1 of Lemma prec-induction

.....wf..... 
1. P : Type
2. a : Atom ⟶ P ⟶ ((P + P + Type) List)
3. Q : i:P ⟶ prec(lbl,p.a[lbl;p];i) ⟶ TYPE
4. ∀i:P. ∀x:prec(lbl,p.a[lbl;p];i).  ((∀j:P. ∀z:{z:prec(lbl,p.a[lbl;p];j)| prec_sub+(P;lbl,p.a[lbl;p]) <j, z> <i, x>} . \000C Q[j;z]) ⇒ Q[i;x])
5. i : P
6. x : prec(lbl,p.a[lbl;p];i)
7. ∀j:P. ∀z:{z:prec(lbl,p.a[lbl;p];j)| ||j;z|| < ||i;x||} .  Q[j;z]
8. j : P
9. ∀z:{z:prec(lbl,p.a[lbl;p];j)| ||j;z|| < ||i;x||} . Q[j;z]
10. z : {z:prec(lbl,p.a[lbl;p];j)| prec_sub+(P;lbl,p.a[lbl;p]) <j, z> <i, x>} 
⊢ z ∈ {z:prec(lbl,p.a[lbl;p];j)| ||j;z|| < ||i;x||} 
BY
{ ((D -1 THEN MemTypeCD) THEN Auto THEN FLemma `prec-sub+-size` [-1] THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  P  :  Type
2.  a  :  Atom  {}\mrightarrow{}  P  {}\mrightarrow{}  ((P  +  P  +  Type)  List)
3.  Q  :  i:P  {}\mrightarrow{}  prec(lbl,p.a[lbl;p];i)  {}\mrightarrow{}  TYPE
4.  \mforall{}i:P.  \mforall{}x:prec(lbl,p.a[lbl;p];i).
          ((\mforall{}j:P.  \mforall{}z:\{z:prec(lbl,p.a[lbl;p];j)|  prec\_sub+(P;lbl,p.a[lbl;p])  <j,  z>  <i,  x>\}  .    Q[j;z])  {}\mRightarrow{}  \000CQ[i;x])
5.  i  :  P
6.  x  :  prec(lbl,p.a[lbl;p];i)
7.  \mforall{}j:P.  \mforall{}z:\{z:prec(lbl,p.a[lbl;p];j)|  ||j;z||  <  ||i;x||\}  .    Q[j;z]
8.  j  :  P
9.  \mforall{}z:\{z:prec(lbl,p.a[lbl;p];j)|  ||j;z||  <  ||i;x||\}  .  Q[j;z]
10.  z  :  \{z:prec(lbl,p.a[lbl;p];j)|  prec\_sub+(P;lbl,p.a[lbl;p])  <j,  z>  <i,  x>\} 
\mvdash{}  z  \mmember{}  \{z:prec(lbl,p.a[lbl;p];j)|  ||j;z||  <  ||i;x||\} 


By

---

Latex:
((D  -1  THEN  MemTypeCD)  THEN  Auto  THEN  FLemma  `prec-sub+-size`  [-1]  THEN  Auto)

---

Home Index