---

Step * 1 of Lemma ppcc-test3


1. [T] : Type
2. f : T ⟶ T
3. [Q] : T ⟶ T ⟶ ℙ
4. [P] : T ⟶ T ⟶ ℙ
5. ∀a,b:T.  (Q[f[a];b] ⇐⇒ P[a;f[b]])
6. Trans(T;a,b.P[a;b])
7. a : T
8. b : T
9. c : T
10. d : T
11. e : T
12. x : T
13. c = x ∈ T
14. f[x] = d ∈ T
15. f[b] = e ∈ T
16. P[a;c]
17. Q[d;b]
⊢ P[a;e]
BY
{ Auto }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  [Q]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
4.  [P]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}a,b:T.    (Q[f[a];b]  \mLeftarrow{}{}\mRightarrow{}  P[a;f[b]])
6.  Trans(T;a,b.P[a;b])
7.  a  :  T
8.  b  :  T
9.  c  :  T
10.  d  :  T
11.  e  :  T
12.  x  :  T
13.  c  =  x
14.  f[x]  =  d
15.  f[b]  =  e
16.  P[a;c]
17.  Q[d;b]
\mvdash{}  P[a;e]


By

---

Latex:
Auto

---

Home Index