---

Step * of Lemma max-fst-property

∀[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
{ Assert ⌜∀[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))))))))})⌝⋅ }

1
.....assertion..... 
∀[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
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 ℤ

---

Latex:

---

Latex:
\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:
Assert  \mkleeneopen{}\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))))))))\})\mkleeneclose{}\mcdot{}

---

Home Index