Step
*
1
of Lemma
prec-ext
.....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]))
BY
{ (D -1
THEN (Assert x ∈ 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])) BY
(D -3 THEN Auto))
THEN (Assert x ~ <fst(x), snd(x)> BY
(GenConclTerm ⌜x⌝⋅ THEN Auto THEN D -2 THEN Reduce 0 THEN Auto))
THEN HypSubst' (-1) (-3)
THEN (Assert ⌜<fst(x), snd(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]))⌝⋅
THENM (RevHypSubst' (-2) (-1) THEN Trivial)
)
THEN (MemHD (-2) THENA Auto)
THEN (MemCD THENA Auto)
THEN Try (Trivial)) }
1
.....subterm..... T:t
2: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 : 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)>
⊢ snd(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;a[fst(x);i]))
Latex:
Latex:
.....subterm..... T:t
1:n
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 : prec(lbl,p.a[lbl;p];i)
\mvdash{} x \mmember{} 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:
(D -1
THEN (Assert x \mmember{} 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])) BY
(D -3 THEN Auto))
THEN (Assert x \msim{} <fst(x), snd(x)> BY
(GenConclTerm \mkleeneopen{}x\mkleeneclose{}\mcdot{} THEN Auto THEN D -2 THEN Reduce 0 THEN Auto))
THEN HypSubst' (-1) (-3)
THEN (Assert \mkleeneopen{}<fst(x), snd(x)> \mmember{} 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]))\mkleeneclose{}\mcdot{}
THENM (RevHypSubst' (-2) (-1) THEN Trivial)
)
THEN (MemHD (-2) THENA Auto)
THEN (MemCD THENA Auto)
THEN Try (Trivial))
Home
Index