---

Step * of Lemma mk-prec_wf

∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[i:P]. ∀[labl:{lbl:Atom| 0 < ||a[lbl;i]||} ].
∀[x:tuple-type(prec-arg-types(lbl,p.a[lbl;p];i;labl))].
  (mk-prec(labl;x) ∈ prec(lbl,p.a[lbl;p];i))
BY
{ (InstLemma `prec-ext` []
   THEN RepeatFor 3 (ParallelLast')
   THEN Intros
   THEN Unfold `prec-arg-types` -1
   THEN (SubsumeC ⌜labl:{lbl:Atom| 0 < ||a[lbl;i]||}  × tuple-type(map(λx.case x
                                                                     of inl(y) =>
                                                                     case y
                                                                      of inl(p) =>
                                                                      prec(lbl,p.a[lbl;p];p)
                                                                      | inr(p) =>
                                                                      prec(lbl,p.a[lbl;p];p) List
                                                                     | inr(E) =>
                                                                     E;a[labl;i]))⌝⋅
         THENL [ProveWfLemma; Auto]
   )) }

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[a:Atom  {}\mrightarrow{}  P  {}\mrightarrow{}  ((P  +  P  +  Type)  List)].  \mforall{}[i:P].  \mforall{}[labl:\{lbl:Atom|  0  <  ||a[lbl;i]||\}  ].
\mforall{}[x:tuple-type(prec-arg-types(lbl,p.a[lbl;p];i;labl))].
    (mk-prec(labl;x)  \mmember{}  prec(lbl,p.a[lbl;p];i))


By

---

Latex:
(InstLemma  `prec-ext`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Intros
  THEN  Unfold  `prec-arg-types`  -1
  THEN  (SubsumeC  \mkleeneopen{}labl:\{lbl:Atom|  0  <  ||a[lbl;i]||\}    \mtimes{}  tuple-type(map(\mlambda{}x.case  x
                                                                                                                                      of  inl(y)  =>
                                                                                                                                      case  y
                                                                                                                                        of  inl(p)  =>
                                                                                                                                        prec(lbl,p.a[lbl;p];p)
                                                                                                                                        |  inr(p)  =>
                                                                                                                                        prec(lbl,p.a[lbl;p];p)  List
                                                                                                                                      |  inr(E)  =>
                                                                                                                                      E;a[labl;i]))\mkleeneclose{}\mcdot{}
              THENL  [ProveWfLemma;  Auto]
  ))

---

Home Index