---

Step * of Lemma prec-sub_wf

∀[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)].
  (prec-sub(P;lbl,p.a[lbl;p];j;x;i;y) ∈ ℙ)
BY
{ (Auto
   THEN Unfold `prec-sub` 0
   THEN (GenConclTerm ⌜dest-prec(y)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN D -2
   THEN Reduce 0
   THEN RepUR ``let`` 0
   THEN RepUR ``prec-arg-types`` -1
   THEN (MemCD
         THENL [Auto
               ; ((InstLemma `select-tuple_wf` [⌜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[lbl;i])⌝;⌜k⌝;⌜||a[lbl;i]||⌝;⌜v1⌝]⋅
                   THENA Auto
                   )
                  THEN (RWO  "select-map" (-1) THENA Auto)
                  THEN Reduce -1)]
   )
   THEN Auto
   THEN InferEqualType
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (GenConclTerm ⌜a[lbl;i][k]⌝⋅ THENA Auto)
   THEN DProdsAndUnions
   THEN Reduce 0
   THEN Auto
   THEN HypSubst' (-1) 0
   THEN Auto) }

---

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)].
    (prec-sub(P;lbl,p.a[lbl;p];j;x;i;y)  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto
  THEN  Unfold  `prec-sub`  0
  THEN  (GenConclTerm  \mkleeneopen{}dest-prec(y)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  D  -2
  THEN  Reduce  0
  THEN  RepUR  ``let``  0
  THEN  RepUR  ``prec-arg-types``  -1
  THEN  (MemCD
              THENL  [Auto
                          ;  ((InstLemma  `select-tuple\_wf`  [\mkleeneopen{}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[lbl;i])\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}||a[lbl;i]||\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{}]\mcdot{}
                                  THENA  Auto
                                  )
                                THEN  (RWO    "select-map"  (-1)  THENA  Auto)
                                THEN  Reduce  -1)]
  )
  THEN  Auto
  THEN  InferEqualType
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConclTerm  \mkleeneopen{}a[lbl;i][k]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  DProdsAndUnions
  THEN  Reduce  0
  THEN  Auto
  THEN  HypSubst'  (-1)  0
  THEN  Auto)

---

Home Index