Proofgold Address

Theorem neq_i_sym : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2 (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition explicit_Group := λ x0 . λ x1 : ι → ι → ι . and (and (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)) (∀ x2 : ο . (∀ x3 . and (prim1 x3 x0) (and (∀ x4 . prim1 x4 x0 ⟶ and (x1 x3 x4 = x4) (x1 x4 x3 = x4)) (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (and (x1 x4 x6 = x3) (x1 x6 x4 = x3)) ⟶ x5) ⟶ x5)) ⟶ x2) ⟶ x2)
Theorem explicit_Group_identity_unique : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ (∀ x4 . prim1 x4 x0 ⟶ x1 x2 x4 = x4) ⟶ (∀ x4 . prim1 x4 x0 ⟶ x1 x4 x3 = x4) ⟶ x2 = x3 (proof)
Definition explicit_Group_identity := λ x0 . λ x1 : ι → ι → ι . prim0 (λ x2 . and (prim1 x2 x0) (and (∀ x3 . prim1 x3 x0 ⟶ and (x1 x2 x3 = x3) (x1 x3 x2 = x3)) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (and (x1 x3 x5 = x2) (x1 x5 x3 = x2)) ⟶ x4) ⟶ x4)))
Definition explicit_Group_inverse := λ x0 . λ x1 : ι → ι → ι . λ x2 . prim0 (λ x3 . and (prim1 x3 x0) (and (x1 x2 x3 = explicit_Group_identity x0 x1) (x1 x3 x2 = explicit_Group_identity x0 x1)))
Known Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem explicit_Group_identity_prop : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ and (prim1 (explicit_Group_identity x0 x1) x0) (and (∀ x2 . prim1 x2 x0 ⟶ and (x1 (explicit_Group_identity x0 x1) x2 = x2) (x1 x2 (explicit_Group_identity x0 x1) = x2)) (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (and (x1 x2 x4 = explicit_Group_identity x0 x1) (x1 x4 x2 = explicit_Group_identity x0 x1)) ⟶ x3) ⟶ x3)) (proof)
Theorem explicit_Group_identity_in : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ prim1 (explicit_Group_identity x0 x1) x0 (proof)
Theorem explicit_Group_identity_lid : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ x1 (explicit_Group_identity x0 x1) x2 = x2 (proof)
Theorem explicit_Group_identity_rid : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ x1 x2 (explicit_Group_identity x0 x1) = x2 (proof)
Theorem explicit_Group_identity_invex : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (and (x1 x2 x4 = explicit_Group_identity x0 x1) (x1 x4 x2 = explicit_Group_identity x0 x1)) ⟶ x3) ⟶ x3 (proof)
Theorem explicit_Group_inverse_prop : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ and (prim1 (explicit_Group_inverse x0 x1 x2) x0) (and (x1 x2 (explicit_Group_inverse x0 x1 x2) = explicit_Group_identity x0 x1) (x1 (explicit_Group_inverse x0 x1 x2) x2 = explicit_Group_identity x0 x1)) (proof)
Theorem explicit_Group_inverse_in : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ prim1 (explicit_Group_inverse x0 x1 x2) x0 (proof)
Theorem explicit_Group_inverse_rinv : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ x1 x2 (explicit_Group_inverse x0 x1 x2) = explicit_Group_identity x0 x1 (proof)
Theorem explicit_Group_inverse_linv : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ x1 (explicit_Group_inverse x0 x1 x2) x2 = explicit_Group_identity x0 x1 (proof)
Theorem explicit_Group_lcancel : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x2 x3 = x1 x2 x4 ⟶ x3 = x4 (proof)
Theorem explicit_Group_rcancel : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x2 x4 = x1 x3 x4 ⟶ x2 = x3 (proof)
Theorem explicit_Group_rinv_rev : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 x3 = explicit_Group_identity x0 x1 ⟶ x3 = explicit_Group_inverse x0 x1 x2 (proof)
Theorem explicit_Group_inv_com : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 x3 = explicit_Group_identity x0 x1 ⟶ x1 x3 x2 = explicit_Group_identity x0 x1 (proof)
Theorem explicit_Group_inv_rev2 : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 (x1 x2 x3) (x1 x2 x3) = explicit_Group_identity x0 x1 ⟶ x1 (x1 x3 x2) (x1 x3 x2) = explicit_Group_identity x0 x1 (proof)
Definition explicit_abelian := λ x0 . λ x1 : ι → ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 x3 = x1 x3 x2
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem explicit_Group_repindep_imp : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ explicit_Group x0 x1 ⟶ explicit_Group x0 x2 (proof)
Theorem explicit_Group_identity_repindep : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ explicit_Group x0 x1 ⟶ explicit_Group_identity x0 x1 = explicit_Group_identity x0 x2 (proof)
Theorem explicit_Group_inverse_repindep : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ explicit_Group x0 x1 ⟶ ∀ x3 . prim1 x3 x0 ⟶ explicit_Group_inverse x0 x1 x3 = explicit_Group_inverse x0 x2 x3 (proof)
Theorem explicit_abelian_repindep_imp : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ explicit_abelian x0 x1 ⟶ explicit_abelian x0 x2 (proof)
Param iff : ο → ο → ο
Known iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem explicit_Group_repindep : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ iff (explicit_Group x0 x1) (explicit_Group x0 x2) (proof)
Theorem explicit_abelian_repindep : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ iff (explicit_abelian x0 x1) (explicit_abelian x0 x2) (proof)
Param 987b2.. : ι → CT2 ι
Definition 30750.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ x1 (987b2.. x2 x3)) ⟶ x1 x0
Param 93c99.. : ι → (ι → (ι → ι → ι) → ο) → ο
Definition 4f2b4.. := λ x0 . and (30750.. x0) (93c99.. x0 explicit_Group)
Definition eb6e9.. := λ x0 . and (4f2b4.. x0) (93c99.. x0 explicit_abelian)
Known 7dd3b.. : ∀ x0 : ι → (ι → ι → ι) → ο . ∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 93c99.. (987b2.. x1 x2) x0 = x0 x1 x2
Known prop_ext : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 = x1
Theorem 8a6de.. : ∀ x0 . ∀ x1 : ι → ι → ι . 93c99.. (987b2.. x0 x1) explicit_Group = explicit_Group x0 x1 (proof)
Known b6770.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ 30750.. (987b2.. x0 x1)
Theorem bd486.. : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ 4f2b4.. (987b2.. x0 x1) (proof)
Theorem f2790.. : ∀ x0 . ∀ x1 : ι → ι → ι . 4f2b4.. (987b2.. x0 x1) ⟶ explicit_Group x0 x1 (proof)
Theorem 09c6f.. : ∀ x0 . ∀ x1 : ι → ι → ι . 93c99.. (987b2.. x0 x1) explicit_abelian = explicit_abelian x0 x1 (proof)
Theorem aa75a.. : ∀ x0 . ∀ x1 : ι → ι → ι . eb6e9.. (987b2.. x0 x1) ⟶ and (4f2b4.. (987b2.. x0 x1)) (explicit_abelian x0 x1) (proof)
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition 7fe8f.. := λ x0 . λ x1 : ι → ι → ι . λ x2 . and (4f2b4.. (987b2.. x2 x1)) (Subq x2 x0)
Param 94f9e.. : ι → (ι → ι) → ι
Definition a0fbb.. := λ x0 . λ x1 : ι → ι → ι . λ x2 . ∀ x3 . prim1 x3 x0 ⟶ Subq (94f9e.. x2 (λ x4 . x1 x3 (x1 x4 (explicit_Group_inverse x0 x1 x3)))) x2
Theorem 5e4ec.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . 4f2b4.. (987b2.. x0 x1) ⟶ Subq x2 x0 ⟶ prim1 (explicit_Group_identity x0 x1) x2 ⟶ (∀ x3 . prim1 x3 x2 ⟶ prim1 (explicit_Group_inverse x0 x1 x3) x2) ⟶ (∀ x3 . prim1 x3 x2 ⟶ ∀ x4 . prim1 x4 x2 ⟶ prim1 (x1 x3 x4) x2) ⟶ 7fe8f.. x0 x1 x2 (proof)
Theorem 7bf3c.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . 4f2b4.. (987b2.. x0 x1) ⟶ 7fe8f.. x0 x1 x2 ⟶ explicit_Group_identity x0 x1 = explicit_Group_identity x2 x1 (proof)
Theorem e2bca.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . 4f2b4.. (987b2.. x0 x1) ⟶ 7fe8f.. x0 x1 x2 ⟶ ∀ x3 . prim1 x3 x2 ⟶ explicit_Group_inverse x0 x1 x3 = explicit_Group_inverse x2 x1 x3 (proof)
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem 7ffca.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . 4f2b4.. (987b2.. x0 x1) ⟶ 7fe8f.. x0 x1 x2 ⟶ explicit_abelian x0 x1 ⟶ a0fbb.. x0 x1 x2 (proof)
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1)
Theorem 62d26.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . explicit_Group x1 x2 ⟶ Subq x0 x1 ⟶ (∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ a0fbb.. x1 x2 x0 ⟶ a0fbb.. x1 x3 x0 (proof)
Definition 69b7e.. := λ x0 x1 . and (and (30750.. x1) (30750.. x0)) (93c99.. x1 (λ x2 . λ x3 : ι → ι → ι . 93c99.. x0 (λ x4 . λ x5 : ι → ι → ι . and (and (x0 = 987b2.. x4 x3) (4f2b4.. (987b2.. x4 x3))) (Subq x4 x2))))
Param 19c2c.. : ι → (ι → CT2 ι) → ι
Param 1216a.. : ι → (ι → ο) → ι
Param 48ef8.. : ι
Param 3097a.. : ι → (ι → ι) → ι
Definition b5c9f.. := λ x0 x1 . 3097a.. x1 (λ x2 . x0)
Param 4ae4a.. : ι → ι
Param f482f.. : ι → ι → ι
Param 4a7ef.. : ι
Definition 95464.. := λ x0 x1 . 19c2c.. x1 (λ x2 . λ x3 : ι → ι → ι . 1216a.. 48ef8.. (λ x4 . ∀ x5 : ο . (∀ x6 . and (prim1 x6 (b5c9f.. x2 (4ae4a.. x4))) (∀ x7 . prim1 x7 (4ae4a.. x4) ⟶ ∀ x8 . prim1 x8 (4ae4a.. x4) ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ ∀ x9 . prim1 x9 (f482f.. x0 4a7ef..) ⟶ ∀ x10 . prim1 x10 (f482f.. x0 4a7ef..) ⟶ x3 (f482f.. x6 x7) x9 = x3 (f482f.. x6 x8) x10 ⟶ ∀ x11 : ο . x11) ⟶ x5) ⟶ x5))
Definition 21582.. := λ x0 x1 . and (69b7e.. x0 x1) (93c99.. x1 (λ x2 . λ x3 : ι → ι → ι . 93c99.. x0 (λ x4 . λ x5 : ι → ι → ι . a0fbb.. x2 x3 x4)))
Theorem a2263.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . 93c99.. (987b2.. x0 x2) (λ x5 . λ x6 : ι → ι → ι . and (and (987b2.. x0 x2 = 987b2.. x5 x3) (4f2b4.. (987b2.. x5 x3))) (Subq x5 x1)) = and (and (987b2.. x0 x2 = 987b2.. x0 x3) (4f2b4.. (987b2.. x0 x3))) (Subq x0 x1) (proof)
Known prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Known a90ae.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ 987b2.. x0 x1 = 987b2.. x0 x2
Theorem d0eb4.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . 93c99.. (987b2.. x1 x3) (λ x5 . λ x6 : ι → ι → ι . 93c99.. (987b2.. x0 x2) (λ x7 . λ x8 : ι → ι → ι . and (and (987b2.. x0 x2 = 987b2.. x7 x6) (4f2b4.. (987b2.. x7 x6))) (Subq x7 x5))) = and (and (987b2.. x0 x2 = 987b2.. x0 x3) (4f2b4.. (987b2.. x0 x3))) (Subq x0 x1) (proof)
Theorem 6754f.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . 69b7e.. (987b2.. x0 x2) (987b2.. x1 x3) ⟶ and (987b2.. x0 x2 = 987b2.. x0 x3) (7fe8f.. x1 x3 x0) (proof)
Theorem 8f922.. : ∀ x0 x1 . 69b7e.. x0 x1 ⟶ ∀ x2 : ι → ι → ο . (∀ x3 x4 . ∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x4 ⟶ ∀ x7 . prim1 x7 x4 ⟶ prim1 (x5 x6 x7) x4) ⟶ 4f2b4.. (987b2.. x3 x5) ⟶ Subq x3 x4 ⟶ x2 (987b2.. x3 x5) (987b2.. x4 x5)) ⟶ x2 x0 x1 (proof)
Theorem 41c9a.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . explicit_Group x1 x2 ⟶ Subq x0 x1 ⟶ (∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ a0fbb.. x1 x2 x0 = a0fbb.. x1 x3 x0 (proof)
Theorem c57da.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . 93c99.. (987b2.. x0 x2) (λ x5 . λ x6 : ι → ι → ι . a0fbb.. x1 x3 x5) = a0fbb.. x1 x3 x0 (proof)
Theorem c2f47.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . 4f2b4.. (987b2.. x1 x3) ⟶ Subq x0 x1 ⟶ 93c99.. (987b2.. x1 x3) (λ x5 . λ x6 : ι → ι → ι . 93c99.. (987b2.. x0 x2) (λ x7 . λ x8 : ι → ι → ι . a0fbb.. x5 x6 x7)) = a0fbb.. x1 x3 x0 (proof)
Theorem e478d.. : ∀ x0 . eb6e9.. x0 ⟶ ∀ x1 . 69b7e.. x1 x0 ⟶ 21582.. x1 x0 (proof)
Known 31c9d.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . 987b2.. x0 x2 = 987b2.. x1 x3 ⟶ and (x0 = x1) (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = x3 x4 x5)
Theorem 4970d.. : ∀ x0 x1 x2 . 69b7e.. x0 x1 ⟶ 69b7e.. x1 x2 ⟶ 69b7e.. x0 x2 (proof)
Definition bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Param 0fc90.. : ι → (ι → ι) → ι
Known 6982e.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ and (prim1 x2 x0) (x1 x2)
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ prim1 x2 (1216a.. x0 x1)
Known 27474.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) (x1 x3)) ⟶ prim1 (0fc90.. x0 x2) (3097a.. x0 x1)
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Known d8d74.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 x2 (3097a.. x0 x1) ⟶ prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3)
Theorem f37b7.. : ∀ x0 x1 . prim1 x1 (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (f482f.. x2))) ⟶ ∀ x2 . prim1 x2 (1216a.. (b5c9f.. x0 x0) (λ x3 . bij x0 x0 (f482f.. x3))) ⟶ prim1 (0fc90.. x0 (λ x3 . f482f.. x2 (f482f.. x1 x3))) (1216a.. (b5c9f.. x0 x0) (λ x3 . bij x0 x0 (f482f.. x3))) (proof)
Theorem 89f56.. : ∀ x0 . prim1 (0fc90.. x0 (λ x1 . x1)) (1216a.. (b5c9f.. x0 x0) (λ x1 . bij x0 x0 (f482f.. x1))) (proof)
Param inv : ι → (ι → ι) → ι → ι
Known 4402a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 0fc90.. x0 x1 = 0fc90.. x0 x2
Known f775d.. : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ ∀ x3 . prim1 x3 x0 ⟶ inv x0 x2 (x2 x3) = x3
Known surj_rinv : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ ∀ x3 . prim1 x3 x1 ⟶ and (prim1 (inv x0 x2 x3) x0) (x2 (inv x0 x2 x3) = x3)
Theorem 4d3ca.. : ∀ x0 x1 . prim1 x1 (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (f482f.. x2))) ⟶ and (and (prim1 (0fc90.. x0 (inv x0 (f482f.. x1))) (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (f482f.. x2)))) (0fc90.. x0 (λ x3 . f482f.. (0fc90.. x0 (inv x0 (f482f.. x1))) (f482f.. x1 x3)) = 0fc90.. x0 (λ x3 . x3))) (0fc90.. x0 (λ x3 . f482f.. x1 (f482f.. (0fc90.. x0 (inv x0 (f482f.. x1))) x3)) = 0fc90.. x0 (λ x3 . x3)) (proof)
Known 6e275.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (3097a.. x0 x1) ⟶ ∀ x3 . prim1 x3 (3097a.. x0 x1) ⟶ (∀ x4 . prim1 x4 x0 ⟶ f482f.. x2 x4 = f482f.. x3 x4) ⟶ x2 = x3
Theorem e418d.. : ∀ x0 . explicit_Group (1216a.. (b5c9f.. x0 x0) (λ x1 . bij x0 x0 (f482f.. x1))) (λ x1 x2 . 0fc90.. x0 (λ x3 . f482f.. x2 (f482f.. x1 x3))) (proof)
Theorem 0e0f6.. : ∀ x0 . explicit_Group_identity (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (f482f.. x2))) (λ x2 x3 . 0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4))) = 0fc90.. x0 (λ x2 . x2) (proof)
Theorem 1845b.. : ∀ x0 x1 . prim1 x1 (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (f482f.. x2))) ⟶ explicit_Group_inverse (1216a.. (b5c9f.. x0 x0) (λ x3 . bij x0 x0 (f482f.. x3))) (λ x3 x4 . 0fc90.. x0 (λ x5 . f482f.. x4 (f482f.. x3 x5))) x1 = 0fc90.. x0 (inv x0 (f482f.. x1)) (proof)
Theorem d3010.. : ∀ x0 x1 . Subq x1 x0 ⟶ ∀ x2 . prim1 x2 (1216a.. (b5c9f.. x0 x0) (λ x3 . and (bij x0 x0 (f482f.. x3)) (∀ x4 . prim1 x4 x1 ⟶ f482f.. x3 x4 = x4))) ⟶ ∀ x3 . prim1 x3 (1216a.. (b5c9f.. x0 x0) (λ x4 . and (bij x0 x0 (f482f.. x4)) (∀ x5 . prim1 x5 x1 ⟶ f482f.. x4 x5 = x5))) ⟶ prim1 (0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4))) (1216a.. (b5c9f.. x0 x0) (λ x4 . and (bij x0 x0 (f482f.. x4)) (∀ x5 . prim1 x5 x1 ⟶ f482f.. x4 x5 = x5))) (proof)
Theorem 5f4b1.. : ∀ x0 x1 . Subq x1 x0 ⟶ 7fe8f.. (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (f482f.. x2))) (λ x2 x3 . 0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4))) (1216a.. (b5c9f.. x0 x0) (λ x2 . and (bij x0 x0 (f482f.. x2)) (∀ x3 . prim1 x3 x1 ⟶ f482f.. x2 x3 = x3))) (proof)
Definition c7794.. := λ x0 . 987b2.. (1216a.. (b5c9f.. x0 x0) (λ x1 . bij x0 x0 (f482f.. x1))) (λ x1 x2 . 0fc90.. x0 (λ x3 . f482f.. x2 (f482f.. x1 x3)))
Definition dae85.. := λ x0 x1 . 987b2.. (1216a.. (b5c9f.. x0 x0) (λ x2 . and (bij x0 x0 (f482f.. x2)) (∀ x3 . prim1 x3 x1 ⟶ f482f.. x2 x3 = x3))) (λ x2 x3 . 0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4)))
Theorem 8fe16.. : ∀ x0 . 4f2b4.. (c7794.. x0) (proof)
Theorem b4446.. : ∀ x0 x1 . Subq x1 x0 ⟶ 4f2b4.. (dae85.. x0 x1) (proof)
Theorem 1a2be.. : ∀ x0 x1 . Subq x1 x0 ⟶ 69b7e.. (dae85.. x0 x1) (c7794.. x0) (proof)
Theorem 03e07.. : ∀ x0 x1 x2 . Subq x2 x1 ⟶ Subq x1 x0 ⟶ 69b7e.. (dae85.. x0 x1) (dae85.. x0 x2) (proof)
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Param If_i : ο → ι → ι → ι
Known ac5c1.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ x1 x2
Known 3a2b6.. : 4ae4a.. (4ae4a.. 4a7ef..) = 4a7ef.. ⟶ ∀ x0 : ο . x0
Known 52da6.. : ∀ x0 x1 x2 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) 4a7ef.. = x0
Known 2eaee.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))
Known 11d6d.. : ∀ x0 x1 x2 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2
Known 72f77.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))
Known f1083.. : prim1 4a7ef.. (4ae4a.. 4a7ef..)
Known 29def.. : ∀ x0 x1 x2 x3 . prim1 x0 x3 ⟶ prim1 x1 x3 ⟶ prim1 x2 x3 ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) (b5c9f.. x3 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Known c60fe.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))
Known 530f4.. : ∀ x0 x1 x2 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ prim1 x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ prim1 x2 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ bij (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x3 . If_i (x3 = 4a7ef..) x0 (If_i (x3 = 4ae4a.. 4a7ef..) x1 x2))))
Known 3bafe.. : 4a7ef.. = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0
Known c8c18.. : 4a7ef.. = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Known f9d2f.. : 4ae4a.. (4ae4a.. 4a7ef..) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Known 2911f.. : ∀ x0 . prim1 x0 (4ae4a.. 4a7ef..) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 x0
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known 958ef.. : ∀ x0 x1 . prim1 x1 (4ae4a.. x0) ⟶ or (prim1 x1 x0) (x1 = x0)
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem 6c4b8.. : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 . and (and (4f2b4.. x3) (69b7e.. x1 x3)) (not (21582.. x1 x3)) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition 7a200.. := λ x0 x1 x2 x3 . 93c99.. x0 (λ x4 . λ x5 : ι → ι → ι . and (and (prim1 x2 x4) (prim1 x3 x4)) (prim1 (x5 x2 (explicit_Group_inverse x4 x5 x3)) (f482f.. x1 4a7ef..)))
Param quotient : (ι → ι → ο) → ι → ο
Param canonical_elt : (ι → ι → ο) → ι → ι
Definition df26d.. := λ x0 x1 . 19c2c.. x0 (λ x2 . λ x3 : ι → ι → ι . 987b2.. (1216a.. x2 (quotient (7a200.. x0 x1))) (λ x4 x5 . canonical_elt (7a200.. x0 x1) (x3 x4 x5)))
Definition 70df3.. := λ x0 . and (4f2b4.. x0) (∀ x1 . prim1 x1 (f482f.. x0 4a7ef..) ⟶ ∀ x2 . prim1 x2 (f482f.. x0 4a7ef..) ⟶ x1 = x2)
Definition 173cc.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (prim1 x2 48ef8..) (∀ x3 : ο . (∀ x4 . and (and (and (and (∀ x5 . prim1 x5 (4ae4a.. x2) ⟶ 4f2b4.. (f482f.. x4 x5)) (∀ x5 . prim1 x5 x2 ⟶ 21582.. (f482f.. x4 x5) (f482f.. x4 (4ae4a.. x5)))) (∀ x5 . prim1 x5 x2 ⟶ eb6e9.. (df26d.. (f482f.. x4 (4ae4a.. x5)) (f482f.. x4 x5)))) (x0 = f482f.. x4 x2)) (70df3.. (f482f.. x4 4a7ef..)) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1