Step
*
1
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. x : pcorec(lbl,p.a[lbl;p]) i
7. (pcorec-size(lbl,p.a[lbl;p]) i <fst(x), snd(x)>)↓
8. (fst(x)) = (fst(x)) ∈ {lbl:Atom| 0 < ||a[lbl;i]||}
9. snd(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;a[fst(x);i]))
10. x ~ <fst(x), snd(x)>
11. (snd(x))
= (snd(x))
∈ {z: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[fst(x);i]))|
(pcorec-size(lbl,p.a[lbl;p]) i <fst(x), z>)↓}
⊢ {z: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[fst(x);i]))|
(pcorec-size(lbl,p.a[lbl;p]) i <fst(x), z>)↓} ⊆r 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[fst(x);i]))
BY
{ ((GenConcl ⌜(fst(x)) = lbl ∈ Atom⌝⋅ THENA Auto)
THEN (RWO "unroll-pcorec-size" 0 THENA Auto)
THEN Reduce 0
THEN (GenConclTerm ⌜a[lbl;i]⌝⋅ THENA Auto)
THEN Thin (-1)
THEN RenameVar `L' (-1)
THEN ThinVar `x') }
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. L : (P + P + Type) List
⊢ {z: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;L))|
(1 + add-sz(pcorec-size(lbl,p.a[lbl;p]);L;z))↓} ⊆r 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;L))
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. x : pcorec(lbl,p.a[lbl;p]) i
7. (pcorec-size(lbl,p.a[lbl;p]) i <fst(x), snd(x)>)\mdownarrow{}
8. (fst(x)) = (fst(x))
9. snd(x) \mmember{} 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[fst(x);i]))
10. x \msim{} <fst(x), snd(x)>
11. (snd(x)) = (snd(x))
\mvdash{} \{z: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[fst(x);i]))|
(pcorec-size(lbl,p.a[lbl;p]) i <fst(x), z>)\mdownarrow{}\} \msubseteq{}r 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[fst(x);i]))
By
Latex:
((GenConcl \mkleeneopen{}(fst(x)) = lbl\mkleeneclose{}\mcdot{} THENA Auto)
THEN (RWO "unroll-pcorec-size" 0 THENA Auto)
THEN Reduce 0
THEN (GenConclTerm \mkleeneopen{}a[lbl;i]\mkleeneclose{}\mcdot{} THENA Auto)
THEN Thin (-1)
THEN RenameVar `L' (-1)
THEN ThinVar `x')
Home
Index