Step
*
2
2
2
1
2
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. labl : {lbl:Atom| 0 < ||a[lbl;i]||}
7. u : P + P + Type
8. v : (P + P + Type) List
9. null(v) = ff
10. x2 : 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
11. x3 : 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))
12. (1 + add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x3))↓
13. m : ℕ
14. add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x3) = m ∈ ℕ
⊢ (1
+ case u
of inl(z) =>
case z of inl(p) => pcorec-size(lbl,p.a[lbl;p]) p x2 | inr(p) => l_sum(map(pcorec-size(lbl,p.a[lbl;p]) p;x2))
| inr(E) =>
0
+ m)↓
BY
{ ((DVar `u' THEN Try (DVar `x')) THEN All Reduce) }
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. labl : {lbl:Atom| 0 < ||a[lbl;i]||}
7. x4 : P
8. v : (P + P + Type) List
9. null(v) = ff
10. x2 : prec(lbl,p.a[lbl;p];x4)
11. x3 : 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))
12. (1 + add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x3))↓
13. m : ℕ
14. add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x3) = m ∈ ℕ
⊢ (1 + (pcorec-size(lbl,p.a[lbl;p]) x4 x2) + m)↓
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. labl : {lbl:Atom| 0 < ||a[lbl;i]||}
7. y : P
8. v : (P + P + Type) List
9. null(v) = ff
10. x2 : prec(lbl,p.a[lbl;p];y) List
11. x3 : 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))
12. (1 + add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x3))↓
13. m : ℕ
14. add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x3) = m ∈ ℕ
⊢ (1 + l_sum(map(pcorec-size(lbl,p.a[lbl;p]) y;x2)) + m)↓
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. labl : {lbl:Atom| 0 < ||a[lbl;i]||}
7. y : Type
8. v : (P + P + Type) List
9. null(v) = ff
10. x2 : y
11. x3 : 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))
12. (1 + add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x3))↓
13. m : ℕ
14. add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x3) = m ∈ ℕ
⊢ (1 + 0 + m)↓
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. labl : \{lbl:Atom| 0 < ||a[lbl;i]||\}
7. u : P + P + Type
8. v : (P + P + Type) List
9. null(v) = ff
10. x2 : 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
11. x3 : 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))
12. (1 + add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x3))\mdownarrow{}
13. m : \mBbbN{}
14. add-sz(pcorec-size(lbl,p.a[lbl;p]);v;x3) = m
\mvdash{} (1
+ case u
of inl(z) =>
case z
of inl(p) =>
pcorec-size(lbl,p.a[lbl;p]) p x2
| inr(p) =>
l\_sum(map(pcorec-size(lbl,p.a[lbl;p]) p;x2))
| inr(E) =>
0
+ m)\mdownarrow{}
By
Latex:
((DVar `u' THEN Try (DVar `x')) THEN All Reduce)
Home
Index