---

Step * 1 of Lemma ppcc-test2


1. [T] : Type
2. f : T ⟶ T
3. [Q] : T ⟶ ℙ
4. [P] : T ⟶ T ⟶ ℙ
5. ∀z:T. (Q[z] ⇒ P[z;f[z]])
6. x : T
7. y : T
8. y = f[x] ∈ T
9. Q[x]
⊢ P[x;y]
BY
{ Auto }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  [Q]  :  T  {}\mrightarrow{}  \mBbbP{}
4.  [P]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}z:T.  (Q[z]  {}\mRightarrow{}  P[z;f[z]])
6.  x  :  T
7.  y  :  T
8.  y  =  f[x]
9.  Q[x]
\mvdash{}  P[x;y]


By

---

Latex:
Auto

---

Home Index