Step
*
1
of Lemma
prec-sub-size
.....assertion.....
1. P : Type
2. a : Atom ⟶ P ⟶ ((P + P + Type) List)
3. j : P
4. x : prec(lbl,p.a[lbl;p];j)
5. i : P
6. labl : {lbl:Atom| 0 < ||a[lbl;i]||}
7. y1 : 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]))
8. prec-sub(P;lbl,p.a[lbl;p];j;x;i;<labl, y1>)
⊢ ||j;x|| ≤ tuple-sum(λc,x. case c
of inl(p) =>
case p of inl(j) => ||j;x|| | inr(j) => l_sum(map(λz.||j;z||;x))
| inr(_) =>
0;a[labl;i];y1)
BY
{ (RepUR ``prec-sub let`` -1
THEN ExRepD
THEN (InstLemma `le-tuple-sum` [⌜parm{i'}⌝;⌜P + P + Type⌝;⌜a[labl;i]⌝;⌜λ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⌝;⌜y1⌝;⌜λc,x. case c
of inl(p) =>
case p
of inl(j) =>
||j;x||
| inr(j) =>
l_sum(map(λz.||j;z||;x))
| inr(_) =>
0⌝;⌜k⌝]⋅
THENA Auto
)
THEN Reduce -1) }
1
1. P : Type
2. a : Atom ⟶ P ⟶ ((P + P + Type) List)
3. j : P
4. x : prec(lbl,p.a[lbl;p];j)
5. i : P
6. labl : {lbl:Atom| 0 < ||a[lbl;i]||}
7. y1 : 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]))
8. k : ℕ||a[labl;i]||
9. ↑isl(a[labl;i][k])
10. ((outl(a[labl;i][k]) = (inl j) ∈ (P + P)) ∧ (x = y1.k ∈ prec(lbl,i.a[lbl;i];j)))
∨ ((outl(a[labl;i][k]) = (inr j ) ∈ (P + P)) ∧ (x ∈ y1.k))
11. y : P
12. x1 : prec(lbl,p.a[lbl;p];y) List
⊢ l_sum(map(λz.||y;z||;x1)) ∈ ℕ
2
1. P : Type
2. a : Atom ⟶ P ⟶ ((P + P + Type) List)
3. j : P
4. x : prec(lbl,p.a[lbl;p];j)
5. i : P
6. labl : {lbl:Atom| 0 < ||a[lbl;i]||}
7. y1 : 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]))
8. k : ℕ||a[labl;i]||
9. ↑isl(a[labl;i][k])
10. ((outl(a[labl;i][k]) = (inl j) ∈ (P + P)) ∧ (x = y1.k ∈ prec(lbl,i.a[lbl;i];j)))
∨ ((outl(a[labl;i][k]) = (inr j ) ∈ (P + P)) ∧ (x ∈ y1.k))
11. case a[labl;i][k] of inl(p) => case p of inl(j) => ||j;y1.k|| | inr(j) => l_sum(map(λz.||j;z||;y1.k)) | inr(_) => 0
≤ tuple-sum(λc,x. case c
of inl(p) =>
case p of inl(j) => ||j;x|| | inr(j) => l_sum(map(λz.||j;z||;x))
| inr(_) =>
0;a[labl;i];y1)
⊢ ||j;x|| ≤ tuple-sum(λc,x. case c
of inl(p) =>
case p of inl(j) => ||j;x|| | inr(j) => l_sum(map(λz.||j;z||;x))
| inr(_) =>
0;a[labl;i];y1)
Latex:
Latex:
.....assertion.....
1. P : Type
2. a : Atom {}\mrightarrow{} P {}\mrightarrow{} ((P + P + Type) List)
3. j : P
4. x : prec(lbl,p.a[lbl;p];j)
5. i : P
6. labl : \{lbl:Atom| 0 < ||a[lbl;i]||\}
7. y1 : 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]))
8. prec-sub(P;lbl,p.a[lbl;p];j;x;i;<labl, y1>)
\mvdash{} ||j;x|| \mleq{} tuple-sum(\mlambda{}c,x. case c
of inl(p) =>
case p of inl(j) => ||j;x|| | inr(j) => l\_sum(map(\mlambda{}z.||j;z||;x))
| inr($_{}$) =>
0;a[labl;i];y1)
By
Latex:
(RepUR ``prec-sub let`` -1
THEN ExRepD
THEN (InstLemma `le-tuple-sum` [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}P + P + Type\mkleeneclose{};\mkleeneopen{}a[labl;i]\mkleeneclose{};
\mkleeneopen{}\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\mkleeneclose{};\mkleeneopen{}y1\mkleeneclose{};\mkleeneopen{}\mlambda{}c,x. case c
of inl(p) =>
case p of inl(j) => ||j;x|| | inr(j) => l\_sum(map(\mlambda{}z.||j;z||;x))
| inr($_{}$) =>
0\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}
THENA Auto
)
THEN Reduce -1)
Home
Index