Proofgold Address

Param lam^Sigma : ι → (ι → ι) → ι
Definition setprod^setprod := λ x0 x1 . lam x0 (λ x2 . x1)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known Empty_eq^Empty_eq : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 0
Param ap^ap : ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Known ap1_Sigma^ap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 1 ∈ x1 (ap x2 0)
Theorem a9232.. : ∀ x0 . setprod x0 0 = 0 (proof)
Param nat_p^nat_p : ι → ο
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition bij^bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Definition equip^equip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2
Param mul_nat^mul_nat : ι → ι → ι
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known mul_nat_0R^mul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Known c5737.. : ∀ x0 . equip 0 x0 ⟶ x0 = 0
Known equip_ref^equip_ref : ∀ x0 . equip x0 x0
Param add_nat^add_nat : ι → ι → ι
Known mul_nat_SR^mul_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Param setsum^setsum : ι → ι → ι
Param setminus^setminus : ι → ι → ι
Param Sing^Sing : ι → ι
Known equip_tra^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2
Known c88e0.. : ∀ x0 x1 x2 x3 . nat_p x0 ⟶ nat_p x1 ⟶ equip x0 x2 ⟶ equip x1 x3 ⟶ equip (add_nat x0 x1) (setsum x2 x3)
Known mul_nat_p^mul_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (mul_nat x0 x1)
Known bijI^bijI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ bij x0 x1 x2
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Param combine_funcs^{combine_funcs} : ι → ι → (ι → ι) → (ι → ι) → ι → ι
Param If_i^If_i : ο → ι → ι → ι
Param Inj0^Inj0 : ι → ι
Param Inj1^Inj1 : ι → ι
Known f4c7c.. : ∀ x0 x1 . ∀ x2 : ι → ο . (∀ x3 . x3 ∈ x0 ⟶ x2 (Inj0 x3)) ⟶ (∀ x3 . x3 ∈ x1 ⟶ x2 (Inj1 x3)) ⟶ ∀ x3 . x3 ∈ setsum x0 x1 ⟶ x2 x3
Known combine_funcs_eq1^{combine_funcs_eq1} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj0 x4) = x2 x4
Known tuple_2_setprod^{tuple_2_setprod} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ setprod x0 x1
Known combine_funcs_eq2^{combine_funcs_eq2} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj1 x4) = x3 x4
Known setprod_mon1^setprod_mon1 : ∀ x0 x1 x2 . x1 ⊆ x2 ⟶ setprod x0 x1 ⊆ setprod x0 x2
Known setminus_Subq^{setminus_Subq} : ∀ x0 x1 . setminus x0 x1 ⊆ x0
Known tuple_2_0_eq^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known setminusE2^setminusE2 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ nIn x2 x1
Known tuple_2_1_eq^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known Inj0_setsum^Inj0_setsum : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ Inj0 x2 ∈ setsum x0 x1
Known ap0_Sigma^ap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 0 ∈ x0
Known tuple_Sigma_eta^{tuple_Sigma_eta} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Known Inj1_setsum^Inj1_setsum : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ Inj1 x2 ∈ setsum x0 x1
Theorem 63881.. : ∀ x0 x1 x2 x3 . nat_p x0 ⟶ nat_p x1 ⟶ equip x0 x2 ⟶ equip x1 x3 ⟶ equip (mul_nat x0 x1) (setprod x2 x3) (proof)
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Definition u18 := ordsucc u17
Definition u19 := ordsucc u18
Definition u20 := ordsucc u19
Definition u21 := ordsucc u20
Definition u22 := ordsucc u21
Definition u23 := ordsucc u22
Definition u24 := ordsucc u23
Definition u25 := ordsucc u24
Definition u26 := ordsucc u25
Definition u27 := ordsucc u26
Definition u28 := ordsucc u27
Definition u29 := ordsucc u28
Definition u30 := ordsucc u29
Definition u31 := ordsucc u30
Definition u32 := ordsucc u31
Definition u33 := ordsucc u32
Definition u34 := ordsucc u33
Definition u35 := ordsucc u34
Definition u36 := ordsucc u35
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_5^nat_5 : nat_p 5
Known nat_4^nat_4 : nat_p 4
Known 2cf95.. : add_nat 6 4 = 10
Theorem f1303.. : add_nat u6 u6 = u12 (proof)
Known nat_1^nat_1 : nat_p 1
Known mul_nat_1R^mul_nat_1R : ∀ x0 . mul_nat x0 1 = x0
Theorem fbd5e.. : mul_nat u6 u2 = u12 (proof)
Known nat_11^nat_11 : nat_p 11
Known add_nat_com^add_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat x0 x1 = add_nat x1 x0
Known nat_6^nat_6 : nat_p 6
Known 91a85.. : add_nat 11 6 = 17
Theorem a2682.. : add_nat u6 u12 = u18 (proof)
Known nat_2^nat_2 : nat_p 2
Theorem 176e9.. : mul_nat u6 u3 = u18 (proof)
Known nat_17^nat_17 : nat_p 17
Known nat_16^nat_16 : nat_p 16
Known f5339.. : add_nat 16 6 = 22
Theorem 67f29.. : add_nat u6 u18 = u24 (proof)
Known nat_3^nat_3 : nat_p 3
Theorem 4603a.. : mul_nat u6 u4 = u24 (proof)
Known 2a2ab.. : add_nat 24 6 = 30
Theorem b6d70.. : mul_nat u6 u5 = u30 (proof)
Known 73189.. : nat_p u24
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Theorem d5180.. : nat_p u25 (proof)
Theorem 24234.. : nat_p u26 (proof)
Theorem e06fe.. : nat_p u27 (proof)
Theorem 5c78e.. : nat_p u28 (proof)
Theorem 7e1a8.. : nat_p u29 (proof)
Theorem a9ae2.. : nat_p u30 (proof)
Theorem 74918.. : nat_p u31 (proof)
Theorem 1f846.. : nat_p u32 (proof)
Theorem ffdd1.. : nat_p u33 (proof)
Theorem 183e4.. : nat_p u34 (proof)
Theorem 966a2.. : nat_p u35 (proof)
Theorem 4aca7.. : nat_p u36 (proof)
Known nat_0^nat_0 : nat_p 0
Known add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem ac6b6.. : add_nat u6 u30 = u36 (proof)
Theorem 66577.. : mul_nat u6 u6 = u36 (proof)
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Theorem 9bff1.. : equip (setprod u6 u6) u36 (proof)
Known setminusE1^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Theorem bc60b.. : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ ∀ x3 : ι → ι . bij x0 x1 x3 ⟶ bij (setminus x0 (Sing x2)) (setminus x1 (Sing (x3 x2))) x3 (proof)
Known 8ac0e.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ ordsucc x0 ⟶ equip x0 (setminus (ordsucc x0) (Sing x1))
Known In_5_6^In_5_6 : 5 ∈ 6
Theorem 903ea.. : equip (setminus (setprod u6 u6) (Sing (lam 2 (λ x0 . If_i (x0 = 0) u5 u5)))) u35 (proof)