Step * 1 1 1 1 of Lemma prior-interface-induction

.....wf..... 
1. Info Type
2. Type
3. es EO+(Info)@i'
4. EClass(T)@i'
5. E(X) ─→ ℙ
6. ∀e:E(X). (P[e] supposing ¬↑e ∈b prior(X) ∧ P[prior(X)(e)]  P[e] supposing ↑e ∈b prior(X))@i
7. E@i
8. ∀e1:E. ((e1 < e)  (↑e1 ∈b X)  P[e1])
9. ↑e ∈b X@i
10. P[e] supposing ¬↑e ∈b prior(X)
11. ↑e ∈b prior(X)
12. P[prior(X)(e)]  P[e]
⊢ prior(X)(e) ∈ E
BY
(GenConclAtAddr [2;2] THEN Auto) }


Latex:



Latex:
.....wf..... 
1.  Info  :  Type
2.  T  :  Type
3.  es  :  EO+(Info)@i'
4.  X  :  EClass(T)@i'
5.  P  :  E(X)  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}e:E(X).  (P[e]  supposing  \mneg{}\muparrow{}e  \mmember{}\msubb{}  prior(X)  \mwedge{}  P[prior(X)(e)]  {}\mRightarrow{}  P[e]  supposing  \muparrow{}e  \mmember{}\msubb{}  prior(X))@i
7.  e  :  E@i
8.  \mforall{}e1:E.  ((e1  <  e)  {}\mRightarrow{}  (\muparrow{}e1  \mmember{}\msubb{}  X)  {}\mRightarrow{}  P[e1])
9.  \muparrow{}e  \mmember{}\msubb{}  X@i
10.  P[e]  supposing  \mneg{}\muparrow{}e  \mmember{}\msubb{}  prior(X)
11.  \muparrow{}e  \mmember{}\msubb{}  prior(X)
12.  P[prior(X)(e)]  {}\mRightarrow{}  P[e]
\mvdash{}  prior(X)(e)  \mmember{}  E


By


Latex:
(GenConclAtAddr  [2;2]  THEN  Auto)




Home Index