Step
*
2
2
2
1
of Lemma
priority-select-property
1. [T] : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
((accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)
⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ¬↑(f u)
8. ¬↑(g u)
⊢ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v|| + 1. ((↑(f [u / v][i])) ∧ (∀j:ℕi. (¬↑(g [u / v][j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v|| + 1. ((↑(g [u / v][i])) ∧ (∀j:ℕi + 1. (¬↑(f [u / v][j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)
⇐⇒ ∀i:ℕ||v|| + 1. ((¬↑(f [u / v][i])) ∧ (¬↑(g [u / v][i]))))
BY
{ (((InstHyp [⌜f⌝; ⌜g⌝] (-5))⋅ THENA Auto)
THEN RepeatFor 2 (ParallelLast)
THEN Try ((ParallelIff (-1) THEN (Trivial ORELSE ExRepD)))
THEN ExRepD
THEN Auto) }
1
1. [T] : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
((accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)
⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ¬↑(f u)
8. ¬↑(g u)
9. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?))
⇒ (∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
10. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)) ⇐ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j]))))
11. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?))
⇒ (∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i]))))
12. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)) ⇐ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))
13. accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)
14. i : ℕ||v||
15. ↑(f v[i])
16. ∀j:ℕi. (¬↑(g v[j]))
⊢ ∃i:ℕ||v|| + 1. ((↑(f [u / v][i])) ∧ (∀j:ℕi. (¬↑(g [u / v][j]))))
2
1. T : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
((accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)
⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ¬↑(f u)
8. ¬↑(g u)
9. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?))
⇒ (∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
10. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)) ⇐ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j]))))
11. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?))
⇒ (∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i]))))
12. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)) ⇐ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))
13. i : ℕ||v|| + 1
14. ↑(f [u / v][i])
15. ∀j:ℕi. (¬↑(g [u / v][j]))
⊢ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j]))))
3
1. [T] : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
((accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)
⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ¬↑(f u)
8. ¬↑(g u)
9. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?))
⇒ (∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
10. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)) ⇐ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j]))))
11. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?))
⇒ (∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i]))))
12. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)) ⇐ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))
13. accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)
14. i : ℕ||v||
15. ↑(g v[i])
16. ∀j:ℕi + 1. (¬↑(f v[j]))
⊢ ∃i:ℕ||v|| + 1. ((↑(g [u / v][i])) ∧ (∀j:ℕi + 1. (¬↑(f [u / v][j]))))
4
1. T : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
((accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)
⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ¬↑(f u)
8. ¬↑(g u)
9. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?))
⇒ (∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
10. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)) ⇐ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j]))))
11. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?))
⇒ (∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i]))))
12. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)) ⇐ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))
13. i : ℕ||v|| + 1
14. ↑(g [u / v][i])
15. ∀j:ℕi + 1. (¬↑(f [u / v][j]))
⊢ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j]))))
5
1. T : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
((accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)
⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ¬↑(f u)
8. ¬↑(g u)
9. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?))
⇒ (∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
10. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)) ⇐ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j]))))
11. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?))
⇒ (∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
12. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)) ⇐ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j]))))
13. accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)
14. ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))
15. i : ℕ||v|| + 1
⊢ ¬↑(f [u / v][i])
6
1. T : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
((accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)
⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ¬↑(f u)
8. ¬↑(g u)
9. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?))
⇒ (∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
10. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)) ⇐ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j]))))
11. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?))
⇒ (∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
12. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)) ⇐ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j]))))
13. accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)
14. ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))
15. i : ℕ||v|| + 1
16. ¬↑(f [u / v][i])
⊢ ¬↑(g [u / v][i])
7
1. T : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
((accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)
⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ¬↑(f u)
8. ¬↑(g u)
9. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?))
⇒ (∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
10. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)) ⇐ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j]))))
11. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?))
⇒ (∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
12. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)) ⇐ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j]))))
13. ∀i:ℕ||v|| + 1. ((¬↑(f [u / v][i])) ∧ (¬↑(g [u / v][i])))
14. i : ℕ||v||
⊢ ¬↑(f v[i])
8
1. T : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
((accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)
⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
∧ (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)
⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ¬↑(f u)
8. ¬↑(g u)
9. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?))
⇒ (∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
10. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl tt)
∈ (𝔹?)) ⇐ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j]))))
11. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?))
⇒ (∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
12. (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr ⋅ )
= (inl ff)
∈ (𝔹?)) ⇐ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j]))))
13. ∀i:ℕ||v|| + 1. ((¬↑(f [u / v][i])) ∧ (¬↑(g [u / v][i])))
14. i : ℕ||v||
15. ¬↑(f v[i])
⊢ ¬↑(g v[i])
Latex:
Latex:
1. [T] : Type
2. u : T
3. v : T List
4. \mforall{}f,g:T {}\mrightarrow{} \mBbbB{}.
((accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr \mcdot{} )
= (inl tt)
\mLeftarrow{}{}\mRightarrow{} \mexists{}i:\mBbbN{}||v||. ((\muparrow{}(f v[i])) \mwedge{} (\mforall{}j:\mBbbN{}i. (\mneg{}\muparrow{}(g v[j])))))
\mwedge{} (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr \mcdot{} )
= (inl ff)
\mLeftarrow{}{}\mRightarrow{} \mexists{}i:\mBbbN{}||v||. ((\muparrow{}(g v[i])) \mwedge{} (\mforall{}j:\mBbbN{}i + 1. (\mneg{}\muparrow{}(f v[j])))))
\mwedge{} (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr \mcdot{} )
= (inr \mcdot{} )
\mLeftarrow{}{}\mRightarrow{} \mforall{}i:\mBbbN{}||v||. ((\mneg{}\muparrow{}(f v[i])) \mwedge{} (\mneg{}\muparrow{}(g v[i])))))
5. f : T {}\mrightarrow{} \mBbbB{}
6. g : T {}\mrightarrow{} \mBbbB{}
7. \mneg{}\muparrow{}(f u)
8. \mneg{}\muparrow{}(g u)
\mvdash{} (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr \mcdot{} )
= (inl tt)
\mLeftarrow{}{}\mRightarrow{} \mexists{}i:\mBbbN{}||v|| + 1. ((\muparrow{}(f [u / v][i])) \mwedge{} (\mforall{}j:\mBbbN{}i. (\mneg{}\muparrow{}(g [u / v][j])))))
\mwedge{} (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr \mcdot{} )
= (inl ff)
\mLeftarrow{}{}\mRightarrow{} \mexists{}i:\mBbbN{}||v|| + 1. ((\muparrow{}(g [u / v][i])) \mwedge{} (\mforall{}j:\mBbbN{}i + 1. (\mneg{}\muparrow{}(f [u / v][j])))))
\mwedge{} (accumulate (with value x and list item m):
if isl(x) then x
if f m then inl tt
if g m then inl ff
else x
fi
over list:
v
with starting value:
inr \mcdot{} )
= (inr \mcdot{} )
\mLeftarrow{}{}\mRightarrow{} \mforall{}i:\mBbbN{}||v|| + 1. ((\mneg{}\muparrow{}(f [u / v][i])) \mwedge{} (\mneg{}\muparrow{}(g [u / v][i]))))
By
Latex:
(((InstHyp [\mkleeneopen{}f\mkleeneclose{}; \mkleeneopen{}g\mkleeneclose{}] (-5))\mcdot{} THENA Auto)
THEN RepeatFor 2 (ParallelLast)
THEN Try ((ParallelIff (-1) THEN (Trivial ORELSE ExRepD)))
THEN ExRepD
THEN Auto)
Home
Index