Step
*
of Lemma
antecedent-surjection_functionality_wrt_iff
∀es:EO
  ∀[P1,P2,Q1,Q2:E ─→ ℙ].
    ∀f:{e:E| P1 e}  ─→ {e:E| Q1 e} 
      ((∀e:E. (P1 e 
⇐⇒ P2 e)) 
⇒ (∀e:E. (Q1 e 
⇐⇒ Q2 e)) 
⇒ (Q1 ←←─ f── P1 
⇐⇒ Q2 ←←─ f── P2))
BY
{ (Auto
   THEN Try (Complete (Auto))
   THEN Try ((RepeatFor 3 (ParallelLast)
              THEN Try (RepeatFor 3 (ParallelLast))
              THEN skip{(Auto THEN ParallelLast THEN Auto)}))) }
1
1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [P2] : E ─→ ℙ
4. [Q1] : E ─→ ℙ
5. [Q2] : E ─→ ℙ
6. f : {e:E| P1 e}  ─→ {e:E| Q1 e} @i
7. ∀e:E. (P1 e 
⇐⇒ P2 e)@i
8. ∀e:E. (Q1 e 
⇐⇒ Q2 e)@i
9. ∀e:{e:E| Q1 e} . ∃e':{e:E| P1 e} . ((f e') = e ∈ E)@i
10. ∀e:{e:E| P1 e} . ((f e < e) ∧ (Q1 (f e)))@i
⊢ ∀e:{e:E| P2 e} . ((f e < e) ∧ (Q2 (f e)))
2
1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [P2] : E ─→ ℙ
4. [Q1] : E ─→ ℙ
5. [Q2] : E ─→ ℙ
6. f : {e:E| P1 e}  ─→ {e:E| Q1 e} @i
7. ∀e:E. (P1 e 
⇐⇒ P2 e)@i
8. ∀e:E. (Q1 e 
⇐⇒ Q2 e)@i
9. ∀e:{e:E| Q2 e} . ∃e':{e:E| P2 e} . ((f e') = e ∈ E)@i
10. ∀e:{e:E| P2 e} . ((f e < e) ∧ (Q2 (f e)))@i
⊢ ∀e:{e:E| P1 e} . ((f e < e) ∧ (Q1 (f e)))
Latex:
\mforall{}es:EO
    \mforall{}[P1,P2,Q1,Q2:E  {}\mrightarrow{}  \mBbbP{}].
        \mforall{}f:\{e:E|  P1  e\}    {}\mrightarrow{}  \{e:E|  Q1  e\} 
            ((\mforall{}e:E.  (P1  e  \mLeftarrow{}{}\mRightarrow{}  P2  e))  {}\mRightarrow{}  (\mforall{}e:E.  (Q1  e  \mLeftarrow{}{}\mRightarrow{}  Q2  e))  {}\mRightarrow{}  (Q1  \mleftarrow{}\mleftarrow{}{}  f{}{}  P1  \mLeftarrow{}{}\mRightarrow{}  Q2  \mleftarrow{}\mleftarrow{}{}  f{}{}  P2))
By
(Auto
  THEN  Try  (Complete  (Auto))
  THEN  Try  ((RepeatFor  3  (ParallelLast)
                        THEN  Try  (RepeatFor  3  (ParallelLast))
                        THEN  skip\{(Auto  THEN  ParallelLast  THEN  Auto)\})))
Home
Index