Proofgold Asset

Known 30edc..^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2
Known 637fd..^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Theorem 86c40.. : ∀ x0 x1 x2 . equip x1 x0 ⟶ equip x2 x0 ⟶ equip x1 x2 (proof)
Known 82600.. : ∀ x0 . equip x0 0 ⟶ x0 = 0
Known d0de4..^Empty_eq : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 0
Known 9d2e6..^nIn_I2 : ∀ x0 x1 . (In x0 x1 ⟶ False) ⟶ nIn x0 x1
Known 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False
Known 681fa..^{proj0_setprod} : ∀ x0 x1 x2 . In x2 (setprod x0 x1) ⟶ In (proj0 x2) x0
Known 54d4b..^equip_ref : ∀ x0 . equip x0 x0
Theorem 12ef8.. : ∀ x0 x1 . equip x0 0 ⟶ equip (setprod x0 x1) 0 (proof)
Known 1cfb6..^{proj1_setprod} : ∀ x0 x1 x2 . In x2 (setprod x0 x1) ⟶ In (proj1 x2) x1
Theorem 9f38c.. : ∀ x0 x1 . equip x1 0 ⟶ equip (setprod x0 x1) 0 (proof)
Known c9b7c..^{equipE_impred} : ∀ x0 x1 . equip x0 x1 ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2
Known 80a11..^bijE_impred : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ ∀ x3 : ο . (inj x0 x1 x2 ⟶ (∀ x4 . In x4 x1 ⟶ ∀ x5 : ο . (∀ x6 . and (In x6 x0) (x2 x6 = x4) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known e6daf..^injE_impred : ∀ x0 x1 . ∀ x2 : ι → ι . inj x0 x1 x2 ⟶ ∀ x3 : ο . ((∀ x4 . In x4 x0 ⟶ In (x2 x4) x1) ⟶ (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ x2 x4 = x2 x5 ⟶ x4 = x5) ⟶ x3) ⟶ x3
Known f2c5c..^equipI : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ equip x0 x1
Known e5c63..^bijI : ∀ x0 x1 . ∀ x2 : ι → ι . inj x0 x1 x2 ⟶ (∀ x3 . In x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (In x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ bij x0 x1 x2
Known 1796e..^injI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ In (x2 x3) x1) ⟶ (∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ inj x0 x1 x2
Known c1504..^{tuple_setprod_eta} : ∀ x0 x1 x2 . In x2 (setprod x0 x1) ⟶ lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Known e51a8..^cases_1 : ∀ x0 . In x0 1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0
Known fe28a..^ap0_setprod : ∀ x0 x1 x2 . In x2 (setprod x0 x1) ⟶ In (ap x2 0) x0
Known 3342b..^proj1_ap_1 : ∀ x0 . proj1 x0 = ap x0 1
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 07808..^pair_setprod : ∀ x0 x1 x2 . In x2 x0 ⟶ ∀ x3 . In x3 x1 ⟶ In (setsum x2 x3) (setprod x0 x1)
Known 0978b..^In_0_1 : In 0 1
Known b8fac..^{proj1_pair_eq} : ∀ x0 x1 . proj1 (setsum x0 x1) = x1
Theorem fb646.. : ∀ x0 x1 . equip x0 x1 ⟶ equip (setprod 1 x0) x1 (proof)
Known 82f37..^proj0_ap_0 : ∀ x0 . proj0 x0 = ap x0 0
Known 6789e..^ap1_setprod : ∀ x0 x1 x2 . In x2 (setprod x0 x1) ⟶ In (ap x2 1) x1
Known d6e1a..^{proj0_pair_eq} : ∀ x0 x1 . proj0 (setsum x0 x1) = x0
Theorem 25080.. : ∀ x0 x1 . equip x0 x1 ⟶ equip (setprod x0 1) x1 (proof)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Param 69aae..^exp_nat : ι → ι → ι
Known 02169..^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Known 9e914.. : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc x1)))))))))))))))) = ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (add_nat x0 x1))))))))))))))))
Known 3fe1c..^add_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat x0 x1 = add_nat x1 x0
Known 53f67.. : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc x0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
Known 74cfe.. : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc x0))))))))))))))))))))))))))))))))
Known 5af12.. : ∀ x0 . add_nat x0 2 = ordsucc (ordsucc x0)
Known 2b177.. : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc x1)))))))) = ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (add_nat x0 x1))))))))
Known a2e43.. : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc x0))))))))))))))))
Known 7bb3f.. : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc (ordsucc (ordsucc (ordsucc x1)))) = ordsucc (ordsucc (ordsucc (ordsucc (add_nat x0 x1))))
Known 63495.. : ∀ x0 . add_nat x0 1 = ordsucc x0
Known 9b388..^mul_nat_1R : ∀ x0 . mul_nat x0 1 = x0
Known 0ac77.. : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc (ordsucc x1)) = ordsucc (ordsucc (add_nat x0 x1))
Known d6dd4.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 x3 . equip x2 x0 ⟶ equip x3 x1 ⟶ equip (binrep x2 x3) (add_nat x0 (69aae.. 2 x1))
Known a62e2.. : ∀ x0 . equip x0 4 ⟶ equip (Power x0) 16
Known 6d362.. : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc x0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
Known b2788.. : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc x0))))))))
Known c83a0.. : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc (ordsucc (ordsucc (ordsucc x0))))
Known a1573.. : ∀ x0 . equip x0 2 ⟶ equip (Power x0) 4
Known fddcf.. : 69aae.. 2 2 = 4
Known 2b6ba.. : nat_p 4
Known f4890..^exp_nat_S : ∀ x0 x1 . nat_p x1 ⟶ 69aae.. x0 (ordsucc x1) = mul_nat x0 (69aae.. x0 x1)
Known 37c59..^exp_nat_1 : ∀ x0 . 69aae.. x0 1 = x0
Known 02b3e.. : ∀ x0 . equip x0 3 ⟶ equip (Power x0) 8
Known c7c31..^nat_1 : nat_p 1
Known fad70..^mul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Known 94de7..^exp_nat_0 : ∀ x0 . 69aae.. x0 0 = 1
Known e6b7d.. : ∀ x0 . equip x0 1 ⟶ equip (Power x0) 2
Known 224e2.. : ∀ x0 . equip x0 0 ⟶ equip (Power x0) 1
Known 9814f.. : nat_p 3
Known 08405..^nat_0 : nat_p 0
Known 36841..^nat_2 : nat_p 2
Known 4c6ff.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 x3 . equip x2 x0 ⟶ equip x3 x1 ⟶ equip (setexp x2 x3) (69aae.. x0 x1)
Known 912b9..^{equip_setprod_mul_nat_2} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 x3 . equip x2 x0 ⟶ equip x3 x1 ⟶ equip (setprod x2 x3) (mul_nat x0 x1)
Known 56707..^{equip_setsum_add_nat_2} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 x3 . equip x2 x0 ⟶ equip x3 x1 ⟶ equip (setsum x2 x3) (add_nat x0 x1)
Theorem 22b42.. : (∀ x0 x1 x2 . equip (setsum (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (Power (Power 0))))) (setsum (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 x2))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setexp x0 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (setexp x0 (Power (Power 0))) (setexp x1 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setprod x1 x2))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) x1)) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) x2)) (setsum (setprod (Power (Power 0)) (setexp x0 (Power (Power 0)))) (setsum (setprod (Power (Power 0)) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (Power 0)) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (Power (Power (Power 0))) (setprod x0 (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod x0 (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod x0 (setprod (setexp x1 (Power (Power 0))) x2)) (setsum (setprod (Power (Power 0)) (setprod x0 (setexp x1 (Power (Power 0))))) (setsum (setprod x0 (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod x0 (setprod x1 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod x0 (setprod x1 x2))) (setsum (setprod (Power (Power 0)) (setprod x0 x1)) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod x0 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod x0 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod x0 x2)) (setsum (setprod (Power (Power 0)) x0) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0))))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setexp x1 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setprod (setexp x1 (Power (Power 0))) x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setexp x1 (Power (Power 0)))) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod x1 (setexp x2 (Power (Power 0)))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod x1 x2)) (setsum (setprod (binrep (Power (Power (Power 0))) 0) x1) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setexp x2 (binrep (Power (Power 0)) 0))) (setsum (setprod (Power (Power (Power 0))) (setexp x2 (Power (Power 0)))) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) x2) (Power 0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Power (Power (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 x2))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setexp x0 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x0 (Power (Power 0))) (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x0 (Power (Power 0))) x1)) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod (setexp x0 (Power (Power 0))) x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setexp x0 (Power (Power 0)))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod x0 (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod x0 (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod x0 (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod x0 (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x0 (setexp x1 (Power (Power 0))))) (setsum (setprod (Power (Power (Power 0))) (setprod x0 (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setprod x0 (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod x0 (setprod x1 x2))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod x0 x1)) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x0 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod x0 (setexp x2 (Power (Power 0)))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod x0 x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) x0) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setexp x1 (binrep (Power (Power 0)) 0))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x1 (Power (Power 0))) x2)) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setexp x1 (Power (Power 0)))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (Power (Power 0)) (setprod x1 x2)) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) x1) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (Power 0)) 0) (setexp x2 (Power (Power 0)))) (setprod (binrep (Power (Power (Power 0))) 0) x2)))))))))))))))))))))))))))))))))))))))))))))))))))))))) ⟶ False) ⟶ ∀ x0 : ο . x0 (proof)