Step
*
1
1
2
1
1
1
3
1
1
of Lemma
prec-ext
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. lbl : Atom
7. u : P + P + Type
8. v : (P + P + Type) List
9. ∀x: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;v))
((add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x) ∈ ℕ)
⇒ (x ∈ 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;v))))
10. null(v) = tt
⊢ ∀x@0:case u
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
((add-sz(pcorec-size(lbl,p.a[lbl;p]);[u / v];x@0) ∈ ℕ)
⇒ (x@0 ∈ case u
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))
BY
{ (Unfold `add-sz` 0
THEN DVar `u'
THEN Try (DVar `x')
THEN Reduce 0
THEN Unfold `tuple-sum` 0
THEN Reduce 0
THEN HypSubst' 10 0
THEN Reduce 0) }
1
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. lbl : Atom
7. x1 : P
8. v : (P + P + Type) List
9. ∀x: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;v))
((add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x) ∈ ℕ)
⇒ (x ∈ 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;v))))
10. null(v) = tt
⊢ ∀x@0:pcorec(lbl,p.a[lbl;p]) x1. ((pcorec-size(lbl,p.a[lbl;p]) x1 x@0 ∈ ℕ) ⇒ (x@0 ∈ prec(lbl,p.a[lbl;p];x1)))
2
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. lbl : Atom
7. y : P
8. v : (P + P + Type) List
9. ∀x: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;v))
((add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x) ∈ ℕ)
⇒ (x ∈ 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;v))))
10. null(v) = tt
⊢ ∀x@0:(pcorec(lbl,p.a[lbl;p]) y) List
((l_sum(map(pcorec-size(lbl,p.a[lbl;p]) y;x@0)) ∈ ℕ) ⇒ (x@0 ∈ prec(lbl,p.a[lbl;p];y) List))
3
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. lbl : Atom
7. y : Type
8. v : (P + P + Type) List
9. ∀x: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;v))
((add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x) ∈ ℕ)
⇒ (x ∈ 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;v))))
10. null(v) = tt
⊢ ∀x@0:y. ((0 ∈ ℕ) ⇒ (x@0 ∈ y))
Latex:
Latex:
1. P : Type
2. a : Atom {}\mrightarrow{} P {}\mrightarrow{} ((P + P + Type) List)
3. pcorec(lbl,p.a[lbl;p]) \mequiv{} ptuple(lbl,p.a[lbl;p];pcorec(lbl,p.a[lbl;p]))
4. i : P
5. pcorec(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) =>
pcorec(lbl,p.a[lbl;p]) p
| inr(p) =>
(pcorec(lbl,p.a[lbl;p]) p) List
| inr(E) =>
E;a[labl;i]))
6. lbl : Atom
7. u : P + P + Type
8. v : (P + P + Type) List
9. \mforall{}x:tuple-type(map(\mlambda{}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;v))
((add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x) \mmember{} \mBbbN{})
{}\mRightarrow{} (x \mmember{} 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;v))))
10. null(v) = tt
\mvdash{} \mforall{}x@0:case u
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
((add-sz(pcorec-size(lbl,p.a[lbl;p]);[u / v];x@0) \mmember{} \mBbbN{})
{}\mRightarrow{} (x@0 \mmember{} case u
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))
By
Latex:
(Unfold `add-sz` 0
THEN DVar `u'
THEN Try (DVar `x')
THEN Reduce 0
THEN Unfold `tuple-sum` 0
THEN Reduce 0
THEN HypSubst' 10 0
THEN Reduce 0)
Home
Index