Step * of Lemma stable__implies

[P,Q:ℙ].  (Stable{P}  Stable{Q  P})
BY
(Auto THEN RepeatFor ((D THENA Auto))) }

1
1. [P] : ℙ
2. [Q] : ℙ
3. Stable{P}
4. ¬¬(Q  P)
5. Q
⊢ P


Latex:


Latex:
\mforall{}[P,Q:\mBbbP{}].    (Stable\{P\}  {}\mRightarrow{}  Stable\{Q  {}\mRightarrow{}  P\})


By


Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THENA  Auto)))




Home Index