---

Step * 2 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))))))))})
⊢ ∀[Info,A,T:Type].
    ∀es:EO+(Info). ∀X:EClass(T × A). ∀e:E.
      {(fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e))))
      ∧ (∃mxe:E(X)
          (mxe ≤loc e 
          ∧ (MaxFst(X)(e) = X(mxe) ∈ (T × A))
          ∧ (∀e':E(X). (e' ≤loc e  ⇒ ((fst(X(e'))) ≤ (fst(X(mxe))))))))} 
      supposing ↑e ∈b MaxFst(X) 
    supposing T ⊆r ℤ
BY
{ (RepeatFor 2 (ParallelLast)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN ParallelOp -3
   THEN RepeatFor 2 ((ParallelLast THENA Auto))
   THEN (D 0 THENA Auto)
   THEN ThinTrivial
   THEN (RepeatFor 3 ((ParallelLast THENA Auto)) THEN 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. 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)

---

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))))))))\})
\mvdash{}  \mforall{}[Info,A,T:Type].
        \mforall{}es:EO+(Info).  \mforall{}X:EClass(T  \mtimes{}  A).  \mforall{}e:E.
            \{(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))))))))\} 
            supposing  \muparrow{}e  \mmember{}\msubb{}  MaxFst(X) 
        supposing  T  \msubseteq{}r  \mBbbZ{}


By

---

Latex:
(RepeatFor  2  (ParallelLast)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  ParallelOp  -3
  THEN  RepeatFor  2  ((ParallelLast  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  ThinTrivial
  THEN  (RepeatFor  3  ((ParallelLast  THENA  Auto))  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index