Step
*
2
1
of Lemma
max-fst-property
1. ∀[Info,A:Type].
∀es:EO+(Info). ∀X:EClass(ℤ × A). ∀e:E.
((↑e ∈b MaxFst(X))
⇒ {(fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e))))
∧ (∃mxe:E(X)
(mxe ≤loc e
∧ (MaxFst(X)(e) = X(mxe) ∈ (ℤ × A))
∧ (∀e':E(X). (e' ≤loc e ⇒ ((fst(X(e'))) ≤ (fst(X(mxe))))))))})
2. Info : Type
3. ∀[A:Type]
∀es:EO+(Info). ∀X:EClass(ℤ × A). ∀e:E.
((↑e ∈b MaxFst(X))
⇒ {(fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e))))
∧ (∃mxe:E(X)
(mxe ≤loc e
∧ (MaxFst(X)(e) = X(mxe) ∈ (ℤ × A))
∧ (∀e':E(X). (e' ≤loc e ⇒ ((fst(X(e'))) ≤ (fst(X(mxe))))))))})
4. A : Type
5. ∀es:EO+(Info). ∀X:EClass(ℤ × A). ∀e:E.
((↑e ∈b MaxFst(X))
⇒ {(fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e))))
∧ (∃mxe:E(X)
(mxe ≤loc e
∧ (MaxFst(X)(e) = X(mxe) ∈ (ℤ × A))
∧ (∀e':E(X). (e' ≤loc e ⇒ ((fst(X(e'))) ≤ (fst(X(mxe))))))))})
6. T : Type
7. T ⊆r ℤ
8. es : EO+(Info)@i'
9. ∀X:EClass(ℤ × A). ∀e:E.
((↑e ∈b MaxFst(X))
⇒ {(fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e))))
∧ (∃mxe:E(X)
(mxe ≤loc e
∧ (MaxFst(X)(e) = X(mxe) ∈ (ℤ × A))
∧ (∀e':E(X). (e' ≤loc e ⇒ ((fst(X(e'))) ≤ (fst(X(mxe))))))))})
10. X : EClass(T × A)@i'
11. ∀e:E
((↑e ∈b MaxFst(X))
⇒ {(fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e))))
∧ (∃mxe:E(X)
(mxe ≤loc e
∧ (MaxFst(X)(e) = X(mxe) ∈ (ℤ × A))
∧ (∀e':E(X). (e' ≤loc e ⇒ ((fst(X(e'))) ≤ (fst(X(mxe))))))))})
12. e : E@i
13. ↑e ∈b MaxFst(X)
14. fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e)))
15. mxe : E(X)
16. mxe ≤loc e
17. MaxFst(X)(e) = X(mxe) ∈ (ℤ × A)
18. ∀e':E(X). (e' ≤loc e ⇒ ((fst(X(e'))) ≤ (fst(X(mxe)))))
19. mxe ≤loc e
⊢ MaxFst(X)(e) = X(mxe) ∈ (T × A)
BY
{ (MoveToConcl (-3) THEN (GenConclAtAddr [1;2] THENA Auto) THEN (GenConclAtAddr [1;3] THENA Auto)) }
1
1. ∀[Info,A:Type].
∀es:EO+(Info). ∀X:EClass(ℤ × A). ∀e:E.
((↑e ∈b MaxFst(X))
⇒ {(fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e))))
∧ (∃mxe:E(X)
(mxe ≤loc e
∧ (MaxFst(X)(e) = X(mxe) ∈ (ℤ × A))
∧ (∀e':E(X). (e' ≤loc e ⇒ ((fst(X(e'))) ≤ (fst(X(mxe))))))))})
2. Info : Type
3. ∀[A:Type]
∀es:EO+(Info). ∀X:EClass(ℤ × A). ∀e:E.
((↑e ∈b MaxFst(X))
⇒ {(fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e))))
∧ (∃mxe:E(X)
(mxe ≤loc e
∧ (MaxFst(X)(e) = X(mxe) ∈ (ℤ × A))
∧ (∀e':E(X). (e' ≤loc e ⇒ ((fst(X(e'))) ≤ (fst(X(mxe))))))))})
4. A : Type
5. ∀es:EO+(Info). ∀X:EClass(ℤ × A). ∀e:E.
((↑e ∈b MaxFst(X))
⇒ {(fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e))))
∧ (∃mxe:E(X)
(mxe ≤loc e
∧ (MaxFst(X)(e) = X(mxe) ∈ (ℤ × A))
∧ (∀e':E(X). (e' ≤loc e ⇒ ((fst(X(e'))) ≤ (fst(X(mxe))))))))})
6. T : Type
7. T ⊆r ℤ
8. es : EO+(Info)@i'
9. ∀X:EClass(ℤ × A). ∀e:E.
((↑e ∈b MaxFst(X))
⇒ {(fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e))))
∧ (∃mxe:E(X)
(mxe ≤loc e
∧ (MaxFst(X)(e) = X(mxe) ∈ (ℤ × A))
∧ (∀e':E(X). (e' ≤loc e ⇒ ((fst(X(e'))) ≤ (fst(X(mxe))))))))})
10. X : EClass(T × A)@i'
11. ∀e:E
((↑e ∈b MaxFst(X))
⇒ {(fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e))))
∧ (∃mxe:E(X)
(mxe ≤loc e
∧ (MaxFst(X)(e) = X(mxe) ∈ (ℤ × A))
∧ (∀e':E(X). (e' ≤loc e ⇒ ((fst(X(e'))) ≤ (fst(X(mxe))))))))})
12. e : E@i
13. ↑e ∈b MaxFst(X)
14. fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e)))
15. mxe : E(X)
16. mxe ≤loc e
17. ∀e':E(X). (e' ≤loc e ⇒ ((fst(X(e'))) ≤ (fst(X(mxe)))))
18. mxe ≤loc e
19. v : T × A@i
20. MaxFst(X)(e) = v ∈ (T × A)@i
21. v1 : T × A@i
22. X(mxe) = v1 ∈ (T × A)@i
⊢ (v = v1 ∈ (ℤ × A)) ⇒ (v = v1 ∈ (T × A))
Latex:
Latex:
1. \mforall{}[Info,A:Type].
\mforall{}es:EO+(Info). \mforall{}X:EClass(\mBbbZ{} \mtimes{} A). \mforall{}e:E.
((\muparrow{}e \mmember{}\msubb{} MaxFst(X))
{}\mRightarrow{} \{(fst(MaxFst(X)(e)) \msim{} imax-list(map(\mlambda{}e.(fst(X(e)));\mleq{}(X)(e))))
\mwedge{} (\mexists{}mxe:E(X)
(mxe \mleq{}loc e
\mwedge{} (MaxFst(X)(e) = X(mxe))
\mwedge{} (\mforall{}e':E(X). (e' \mleq{}loc e {}\mRightarrow{} ((fst(X(e'))) \mleq{} (fst(X(mxe))))))))\})
2. Info : Type
3. \mforall{}[A:Type]
\mforall{}es:EO+(Info). \mforall{}X:EClass(\mBbbZ{} \mtimes{} A). \mforall{}e:E.
((\muparrow{}e \mmember{}\msubb{} MaxFst(X))
{}\mRightarrow{} \{(fst(MaxFst(X)(e)) \msim{} imax-list(map(\mlambda{}e.(fst(X(e)));\mleq{}(X)(e))))
\mwedge{} (\mexists{}mxe:E(X)
(mxe \mleq{}loc e
\mwedge{} (MaxFst(X)(e) = X(mxe))
\mwedge{} (\mforall{}e':E(X). (e' \mleq{}loc e {}\mRightarrow{} ((fst(X(e'))) \mleq{} (fst(X(mxe))))))))\})
4. A : Type
5. \mforall{}es:EO+(Info). \mforall{}X:EClass(\mBbbZ{} \mtimes{} A). \mforall{}e:E.
((\muparrow{}e \mmember{}\msubb{} MaxFst(X))
{}\mRightarrow{} \{(fst(MaxFst(X)(e)) \msim{} imax-list(map(\mlambda{}e.(fst(X(e)));\mleq{}(X)(e))))
\mwedge{} (\mexists{}mxe:E(X)
(mxe \mleq{}loc e
\mwedge{} (MaxFst(X)(e) = X(mxe))
\mwedge{} (\mforall{}e':E(X). (e' \mleq{}loc e {}\mRightarrow{} ((fst(X(e'))) \mleq{} (fst(X(mxe))))))))\})
6. T : Type
7. T \msubseteq{}r \mBbbZ{}
8. es : EO+(Info)@i'
9. \mforall{}X:EClass(\mBbbZ{} \mtimes{} A). \mforall{}e:E.
((\muparrow{}e \mmember{}\msubb{} MaxFst(X))
{}\mRightarrow{} \{(fst(MaxFst(X)(e)) \msim{} imax-list(map(\mlambda{}e.(fst(X(e)));\mleq{}(X)(e))))
\mwedge{} (\mexists{}mxe:E(X)
(mxe \mleq{}loc e
\mwedge{} (MaxFst(X)(e) = X(mxe))
\mwedge{} (\mforall{}e':E(X). (e' \mleq{}loc e {}\mRightarrow{} ((fst(X(e'))) \mleq{} (fst(X(mxe))))))))\})
10. X : EClass(T \mtimes{} A)@i'
11. \mforall{}e:E
((\muparrow{}e \mmember{}\msubb{} MaxFst(X))
{}\mRightarrow{} \{(fst(MaxFst(X)(e)) \msim{} imax-list(map(\mlambda{}e.(fst(X(e)));\mleq{}(X)(e))))
\mwedge{} (\mexists{}mxe:E(X)
(mxe \mleq{}loc e
\mwedge{} (MaxFst(X)(e) = X(mxe))
\mwedge{} (\mforall{}e':E(X). (e' \mleq{}loc e {}\mRightarrow{} ((fst(X(e'))) \mleq{} (fst(X(mxe))))))))\})
12. e : E@i
13. \muparrow{}e \mmember{}\msubb{} MaxFst(X)
14. fst(MaxFst(X)(e)) \msim{} imax-list(map(\mlambda{}e.(fst(X(e)));\mleq{}(X)(e)))
15. mxe : E(X)
16. mxe \mleq{}loc e
17. MaxFst(X)(e) = X(mxe)
18. \mforall{}e':E(X). (e' \mleq{}loc e {}\mRightarrow{} ((fst(X(e'))) \mleq{} (fst(X(mxe)))))
19. mxe \mleq{}loc e
\mvdash{} MaxFst(X)(e) = X(mxe)
By
Latex:
(MoveToConcl (-3) THEN (GenConclAtAddr [1;2] THENA Auto) THEN (GenConclAtAddr [1;3] THENA Auto))
Home
Index