Parents |
pcf-defs |
Constants |
$∈c
|
PC → PC → BOOL |
Fixity |
Right Infix 300: |
∈c |
Axioms |
pc_ext
|
⊢ ∀ c1 c2• c1 = c2 ⇔ (∀ f• f ∈f c1 ⇔ f ∈f c2) |
pf_ext
|
⊢ ∀ f1 f2 ![]() ![]() ![]() ![]() |
associative_axiom
|
⊢ ∀ f g h
![]() ![]() |
identity_axiom
|
⊢ ∀ c f
![]() ![]() |
pc_closure_axiom
|
⊢ ∀ c f g
![]() ![]() ![]() ![]() ![]() |
pf_induction
|
⊢ ∀ p ![]() ![]() ![]() ![]() |
Definitions |
∈c
|
⊢ ∀ c d• c ∈c d ⇔ idf c ∈f d |