Proofgold Address

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