Step
*
1
1
1
of Lemma
list-max-map
1. T : Type
2. A : Type
3. g : A ⟶ T
4. f : T ⟶ ℤ
5. u : A
6. u1 : A
7. v : A List
8. ∀Z:{x:ℤ × A + Top| ↑isl(x)}
(outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, g x> else a fi | inr(q) => inl <n, g x>
over list:
v
with starting value:
(λp.(inl <fst(outl(p)), g (snd(outl(p)))>)) Z))
= <fst(outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, x> else a fi | inr(q) => inl <n, x>
over list:
v
with starting value:
Z)))
, g
(snd(outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, x> else a fi | inr(q) => inl <n, x>
over list:
v
with starting value:
Z))))
>
∈ (i:ℤ × T))
9. x : ℤ × A@i
10. True
⊢ outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, g x> else a fi | inr(q) => inl <n, g x>
over list:
v
with starting value:
eval n = f[g u1] in
if fst(outl(inl x)) <z n then inl <n, g u1> else inl <fst(outl(inl x)), g (snd(outl(inl x)))> fi ))
= <fst(outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, x> else a fi | inr(q) => inl <n, x>
over list:
v
with starting value:
eval n = f[g u1] in
case inl x of inl(p) => if fst(p) <z n then inl <n, u1> else inl x fi | inr(q) => inl <n, u1>)))
, g
(snd(outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, x> else a fi | inr(q) => inl <n, x>
over list:
v
with starting value:
eval n = f[g u1] in
case inl x of inl(p) => if fst(p) <z n then inl <n, u1> else inl x fi | inr(q) => inl <n, u1>))))
>
∈ (i:ℤ × T)
BY
{ ((InstHyp [⌜eval n = f[g u1] in
case inl x of inl(p) => if fst(p) <z n then inl <n, u1> else inl x fi | inr(q) => inl <n, u1>⌝] 8⋅
THENA ((CallByValueReduce 0 THEN Auto) THEN Reduce 0 THEN AutoSplit)
)
THEN Thin 8
THEN (NthHypEq (-1) THEN Thin (-1))
THEN EqCD
THEN Auto) }
1
.....subterm..... T:t
2:n
1. T : Type
2. A : Type
3. g : A ⟶ T
4. f : T ⟶ ℤ
5. u : A
6. u1 : A
7. v : A List
8. x : ℤ × A@i
9. True
⊢ outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, g x> else a fi | inr(q) => inl <n, g x>
over list:
v
with starting value:
eval n = f[g u1] in
if fst(outl(inl x)) <z n then inl <n, g u1> else inl <fst(outl(inl x)), g (snd(outl(inl x)))> fi ))
= outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, g x> else a fi | inr(q) => inl <n, g x>
over list:
v
with starting value:
(λp.(inl <fst(outl(p)), g (snd(outl(p)))>))
eval n = f[g u1] in
case inl x of inl(p) => if fst(p) <z n then inl <n, u1> else inl x fi | inr(q) => inl <n, u1>))
∈ (i:ℤ × T)
2
1. T : Type
2. A : Type
3. g : A ⟶ T
4. f : T ⟶ ℤ
5. u : A
6. u1 : A
7. v : A List
8. x : ℤ × A@i
9. True
⊢ fst(outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, x> else a fi | inr(q) => inl <n, x>
over list:
v
with starting value:
eval n = f[g u1] in
case inl x of inl(p) => if fst(p) <z n then inl <n, u1> else inl x fi | inr(q) => inl <n, u1>))) ∈ ℤ
3
1. T : Type
2. A : Type
3. g : A ⟶ T
4. f : T ⟶ ℤ
5. u : A
6. u1 : A
7. v : A List
8. x : ℤ × A@i
9. True
⊢ snd(outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, x> else a fi | inr(q) => inl <n, x>
over list:
v
with starting value:
eval n = f[g u1] in
case inl x of inl(p) => if fst(p) <z n then inl <n, u1> else inl x fi | inr(q) => inl <n, u1>))) ∈ A
Latex:
Latex:
1. T : Type
2. A : Type
3. g : A {}\mrightarrow{} T
4. f : T {}\mrightarrow{} \mBbbZ{}
5. u : A
6. u1 : A
7. v : A List
8. \mforall{}Z:\{x:\mBbbZ{} \mtimes{} A + Top| \muparrow{}isl(x)\}
(outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, g x> else a fi | inr(q) => inl <n, g x>
over list:
v
with starting value:
(\mlambda{}p.(inl <fst(outl(p)), g (snd(outl(p)))>)) Z))
= <fst(outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, x> else a fi | inr(q) => inl <n, \000Cx>
over list:
v
with starting value:
Z)))
, g
(snd(outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, x> else a fi | inr(q) => inl <n\000C, x>
over list:
v
with starting value:
Z))))
>)
9. x : \mBbbZ{} \mtimes{} A@i
10. True
\mvdash{} outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, g x> else a fi | inr(q) => inl <n, g x>
over list:
v
with starting value:
eval n = f[g u1] in
if fst(outl(inl x)) <z n then inl <n, g u1> else inl <fst(outl(inl x)), g (snd(outl(inl x)))\000C> fi ))
= <fst(outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, x> else a fi | inr(q) => inl <n, x>
over list:
v
with starting value:
eval n = f[g u1] in
case inl x
of inl(p) =>
if fst(p) <z n then inl <n, u1> else inl x fi
| inr(q) =>
inl <n, u1>)))
, g
(snd(outl(accumulate (with value a and list item x):
eval n = f[g x] in
case a of inl(p) => if fst(p) <z n then inl <n, x> else a fi | inr(q) => inl <n, x>
over list:
v
with starting value:
eval n = f[g u1] in
case inl x
of inl(p) =>
if fst(p) <z n then inl <n, u1> else inl x fi
| inr(q) =>
inl <n, u1>))))
>
By
Latex:
((InstHyp [\mkleeneopen{}eval n = f[g u1] in
case inl x
of inl(p) =>
if fst(p) <z n then inl <n, u1> else inl x fi
| inr(q) =>
inl <n, u1>\mkleeneclose{}] 8\mcdot{}
THENA ((CallByValueReduce 0 THEN Auto) THEN Reduce 0 THEN AutoSplit)
)
THEN Thin 8
THEN (NthHypEq (-1) THEN Thin (-1))
THEN EqCD
THEN Auto)
Home
Index