---

Step * of Lemma prec-ext

∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[i:P].
  prec(lbl,p.a[lbl;p];i) ≡ 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]))
BY
{ (InstLemma `pcorec-ext` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN DupHyp (-2)
   THEN (D -1 With ⌜i⌝  THENA Auto)
   THEN RepUR ``ptuple`` -1
   THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
.....subterm..... T:t
1:n
1. P : Type
2. a : Atom ⟶ P ⟶ ((P + P + Type) List)
3. pcorec(lbl,p.a[lbl;p]) ≡ ptuple(lbl,p.a[lbl;p];pcorec(lbl,p.a[lbl;p]))
4. i : P
5. pcorec(lbl,p.a[lbl;p]) i ≡ labl:{lbl:Atom| 0 < ||a[lbl;i]||}  × tuple-type(map(λx.case x
                                                     of inl(y) =>
                                                     case y
                                                      of inl(p) =>
                                                      pcorec(lbl,p.a[lbl;p]) p
                                                      | inr(p) =>
                                                      (pcorec(lbl,p.a[lbl;p]) p) List
                                                     | inr(E) =>
                                                     E;a[labl;i]))
6. x : prec(lbl,p.a[lbl;p];i)
⊢ x ∈ 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]))

2
.....subterm..... T:t
1:n
1. P : Type
2. a : Atom ⟶ P ⟶ ((P + P + Type) List)
3. pcorec(lbl,p.a[lbl;p]) ≡ ptuple(lbl,p.a[lbl;p];pcorec(lbl,p.a[lbl;p]))
4. i : P
5. pcorec(lbl,p.a[lbl;p]) i ≡ labl:{lbl:Atom| 0 < ||a[lbl;i]||}  × tuple-type(map(λx.case x
                                                     of inl(y) =>
                                                     case y
                                                      of inl(p) =>
                                                      pcorec(lbl,p.a[lbl;p]) p
                                                      | inr(p) =>
                                                      (pcorec(lbl,p.a[lbl;p]) p) List
                                                     | inr(E) =>
                                                     E;a[labl;i]))
6. x : 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]))
⊢ x ∈ prec(lbl,p.a[lbl;p];i)

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[a:Atom  {}\mrightarrow{}  P  {}\mrightarrow{}  ((P  +  P  +  Type)  List)].  \mforall{}[i:P].
    prec(lbl,p.a[lbl;p];i)  \mequiv{}  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]))


By

---

Latex:
(InstLemma  `pcorec-ext`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  DupHyp  (-2)
  THEN  (D  -1  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  RepUR  ``ptuple``  -1
  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index