Proofgold Address

Definition canonical_elt := λ x0 : ι → ι → ο . λ x1 . prim0 (x0 x1)
Known Eps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (prim0 x0)
Theorem canonical_elt_rel : ∀ x0 : ι → ι → ο . ∀ x1 . x0 x1 x1 ⟶ x0 x1 (canonical_elt x0 x1) (proof)
Param per : (ι → ι → ο) → ο
Known pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1
Known per_stra1 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 x3 . x0 x2 x1 ⟶ x0 x2 x3 ⟶ x0 x1 x3
Definition transitive := λ x0 : ι → ι → ο . ∀ x1 x2 x3 . x0 x1 x2 ⟶ x0 x2 x3 ⟶ x0 x1 x3
Known per_tra : ∀ x0 : ι → ι → ο . per x0 ⟶ transitive x0
Theorem canonical_elt_eq : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 . x0 x1 x2 ⟶ canonical_elt x0 x1 = canonical_elt x0 x2 (proof)
Theorem canonical_elt_idem : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 . x0 x1 x1 ⟶ canonical_elt x0 x1 = canonical_elt x0 (canonical_elt x0 x1) (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition quotient := λ x0 : ι → ι → ο . λ x1 . and (x0 x1 x1) (x1 = canonical_elt x0 x1)
Known andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Theorem quotient_prop1 : ∀ x0 : ι → ι → ο . ∀ x1 . quotient x0 x1 ⟶ x0 x1 x1 (proof)
Known andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Theorem quotient_prop2 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 . quotient x0 x1 ⟶ quotient x0 x2 ⟶ x0 x1 x2 ⟶ x1 = x2 (proof)
Param If_i : ο → ι → ι → ι
Definition canonical_elt_def := λ x0 : ι → ι → ο . λ x1 : ι → ι . λ x2 . If_i (x0 x2 (x1 x2)) (x1 x2) (canonical_elt x0 x2)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Known If_i_correct : ∀ x0 : ο . ∀ x1 x2 . or (and x0 (If_i x0 x1 x2 = x1)) (and (not x0) (If_i x0 x1 x2 = x2))
Theorem canonical_elt_def_rel : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . ∀ x2 . x0 x2 x2 ⟶ x0 x2 (canonical_elt_def x0 x1 x2) (proof)
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Theorem canonical_elt_def_eq : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 : ι → ι . (∀ x2 x3 . x0 x2 x3 ⟶ x1 x2 = x1 x3) ⟶ ∀ x2 x3 . x0 x2 x3 ⟶ canonical_elt_def x0 x1 x2 = canonical_elt_def x0 x1 x3 (proof)
Theorem canonical_elt_def_idem : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 : ι → ι . (∀ x2 x3 . x0 x2 x3 ⟶ x1 x2 = x1 x3) ⟶ ∀ x2 . x0 x2 x2 ⟶ canonical_elt_def x0 x1 x2 = canonical_elt_def x0 x1 (canonical_elt_def x0 x1 x2) (proof)
Definition quotient_def := λ x0 : ι → ι → ο . λ x1 : ι → ι . λ x2 . and (x0 x2 x2) (x2 = canonical_elt_def x0 x1 x2)
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known per_ref1 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 . x0 x1 x2 ⟶ x0 x1 x1
Theorem quotient_def_prop0 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 : ι → ι . ∀ x2 . x0 x2 (x1 x2) ⟶ x2 = x1 x2 ⟶ quotient_def x0 x1 x2 (proof)
Theorem quotient_def_prop1 : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . ∀ x2 . quotient_def x0 x1 x2 ⟶ x0 x2 x2 (proof)
Theorem quotient_def_prop2 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 : ι → ι . (∀ x2 x3 . x0 x2 x3 ⟶ x1 x2 = x1 x3) ⟶ ∀ x2 x3 . quotient_def x0 x1 x2 ⟶ quotient_def x0 x1 x3 ⟶ x0 x2 x3 ⟶ x2 = x3 (proof)