Step
*
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. Z : {x:ℤ × A + Top| ↑isl(x)} @i
⊢ 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(Z)) <z n then inl <n, g u1> else inl <fst(outl(Z)), g (snd(outl(Z)))> 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 Z of inl(p) => if fst(p) <z n then inl <n, u1> else Z 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 Z of inl(p) => if fst(p) <z n then inl <n, u1> else Z fi | inr(q) => inl <n, u1>))))
>
∈ (i:ℤ × T)
BY
{ TACTIC:(D -1 THEN D -2 THEN Reduce (-1) THEN Auto) }
1
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)
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. Z : \{x:\mBbbZ{} \mtimes{} A + Top| \muparrow{}isl(x)\} @i
\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(Z)) <z n then inl <n, g u1> else inl <fst(outl(Z)), g (snd(outl(Z)))> 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 Z of inl(p) => if fst(p) <z n then inl <n, u1> else Z fi | inr(q) => inl <n, u1>)\000C))
, 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 Z of inl(p) => if fst(p) <z n then inl <n, u1> else Z fi | inr(q) => inl <n, u1\000C>))))
>
By
Latex:
TACTIC:(D -1 THEN D -2 THEN Reduce (-1) THEN Auto)
Home
Index