Search for blocks/addresses/...

Proofgold Address

address
PUbKmca8iRFNEBwDLYXXnp9RECgxvTDJry3
total
0
mg
-
conjpub
-
current assets
cffce../64e55.. bday: 11610 doc published by PrGxv..
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param setsumsetsum : ιιι
Definition tuple_ptuple_p := λ x0 x1 . ∀ x2 . x2x1∀ x3 : ο . (∀ x4 . and (x4x0) (∀ x5 : ο . (∀ x6 . x2 = setsum x4 x6x5)x5)x3)x3
Param lamSigma : ι(ιι) → ι
Param apap : ιιι
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known lamIlamI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0∀ x3 . x3x1 x2setsum x2 x3lam x0 x1
Known apIapI : ∀ x0 x1 x2 . setsum x1 x2x0x2ap x0 x1
Known lamElamE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1∀ x3 : ο . (∀ x4 . and (x4x0) (∀ x5 : ο . (∀ x6 . and (x6x1 x4) (x2 = setsum x4 x6)x5)x5)x3)x3
Known apEapE : ∀ x0 x1 x2 . x2ap x0 x1setsum x1 x2x0
Theorem 47a16.. : ∀ x0 x1 . tuple_p x0 x1x1 = lam x0 (ap x1) (proof)
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem 55df5.. : ∀ x0 . ∀ x1 : ι → ι . tuple_p x0 (lam x0 x1) (proof)
Param ordsuccordsucc : ιι
Param If_iIf_i : οιιι
Definition 59caa.. := λ x0 . λ x1 : ι → ι . λ x2 . ∀ x3 : ι → ο . (∀ x4 . x4x0∀ x5 . tuple_p (x1 x4) x5(∀ x6 . x6x1 x4x3 (ap x5 x6))x3 (lam 2 (λ x6 . If_i (x6 = 0) x4 x5)))x3 x2
Theorem 83bd8.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0∀ x3 . tuple_p (x1 x2) x3(∀ x4 . x4x1 x259caa.. x0 x1 (ap x3 x4))59caa.. x0 x1 (lam 2 (λ x4 . If_i (x4 = 0) x2 x3)) (proof)
Theorem 32b0a.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . (∀ x3 . x3x0∀ x4 . tuple_p (x1 x3) x4(∀ x5 . x5x1 x359caa.. x0 x1 (ap x4 x5))(∀ x5 . x5x1 x3x2 (ap x4 x5))x2 (lam 2 (λ x5 . If_i (x5 = 0) x3 x4)))∀ x3 . 59caa.. x0 x1 x3x2 x3 (proof)
Param ZF_closedZF_closed : ιο
Param nat_pnat_p : ιο
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known ZF_ordsucc_closedZF_ordsucc_closed : ∀ x0 . ZF_closed x0∀ x1 . x1x0ordsucc x1x0
Theorem ebd65.. : ∀ x0 . ZF_closed x00x0∀ x1 . nat_p x1x1x0 (proof)
Definition TransSetTransSet := λ x0 . ∀ x1 . x1x0x1x0
Known c59b3..ZF_Sigma_closed : ∀ x0 . TransSet x0ZF_closed x0∀ x1 . x1x0∀ x2 : ι → ι . (∀ x3 . x3x1x2 x3x0)lam x1 x2x0
Theorem b6a89.. : ∀ x0 . TransSet x0ZF_closed x0∀ x1 . x1x0∀ x2 . tuple_p x1 x2(∀ x3 . x3x1ap x2 x3x0)x2x0 (proof)
Known nat_2nat_2 : nat_p 2
Known tuple_p_2_tupletuple_p_2_tuple : ∀ x0 x1 . tuple_p 2 (lam 2 (λ x2 . If_i (x2 = 0) x0 x1))
Known cases_2cases_2 : ∀ x0 . x02∀ x1 : ι → ο . x1 0x1 1x1 x0
Known tuple_2_0_eqtuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known tuple_2_1_eqtuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Theorem 9f645.. : ∀ x0 . TransSet x0ZF_closed x00x0∀ x1 . x1x0∀ x2 : ι → ι . (∀ x3 . x3x1x2 x3x0)∀ x3 . 59caa.. x1 x2 x3x3x0 (proof)
Param SepSep : ι(ιο) → ι
Param UPairUPair : ιιι
Param famunionfamunion : ι(ιι) → ι
Param SingSing : ιι
Definition c8f46.. := λ x0 . λ x1 : ι → ι . Sep (prim6 (UPair x0 (famunion x0 (λ x2 . Sing (x1 x2))))) (59caa.. x0 x1)
Known SepE2SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x1 x2
Theorem 0bd77.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2c8f46.. x0 x159caa.. x0 x1 x2 (proof)
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Known UnivOf_TransSetUnivOf_TransSet : ∀ x0 . TransSet (prim6 x0)
Known UnivOf_ZF_closedUnivOf_ZF_closed : ∀ x0 . ZF_closed (prim6 x0)
Known 6aa34..UnivOf_Subq_closed : ∀ x0 x1 . x1prim6 x0∀ x2 . x2x1x2prim6 x0
Known UnivOf_InUnivOf_In : ∀ x0 . x0prim6 x0
Known Subq_EmptySubq_Empty : ∀ x0 . 0x0
Known famunionIfamunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2x0x3x1 x2x3famunion x0 x1
Known SingISingI : ∀ x0 . x0Sing x0
Known UPairI2UPairI2 : ∀ x0 x1 . x1UPair x0 x1
Known UPairI1UPairI1 : ∀ x0 x1 . x0UPair x0 x1
Theorem 2224e.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . 59caa.. x0 x1 x2x2c8f46.. x0 x1 (proof)
Theorem 4db94.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0∀ x3 . tuple_p (x1 x2) x3(∀ x4 . x4x1 x2ap x3 x4c8f46.. x0 x1)lam 2 (λ x4 . If_i (x4 = 0) x2 x3)c8f46.. x0 x1 (proof)
Theorem 34323.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . (∀ x3 . x3x0∀ x4 . tuple_p (x1 x3) x4(∀ x5 . x5x1 x3ap x4 x5c8f46.. x0 x1)(∀ x5 . x5x1 x3x2 (ap x4 x5))x2 (lam 2 (λ x5 . If_i (x5 = 0) x3 x4)))∀ x3 . x3c8f46.. x0 x1x2 x3 (proof)
Definition c40a3.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ι → ι . λ x3 x4 . ∀ x5 : ι → ι → ο . (∀ x6 . x6x0∀ x7 . tuple_p (x1 x6) x7∀ x8 : ι → ι . (∀ x9 . x9x1 x6x5 (ap x7 x9) (x8 x9))x5 (lam 2 (λ x9 . If_i (x9 = 0) x6 x7)) (x2 x6 x7 (lam (x1 x6) x8)))x5 x3 x4
Theorem d7522.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ι . ∀ x3 . x3x0∀ x4 . tuple_p (x1 x3) x4∀ x5 : ι → ι . (∀ x6 . x6x1 x3c40a3.. x0 x1 x2 (ap x4 x6) (x5 x6))c40a3.. x0 x1 x2 (lam 2 (λ x6 . If_i (x6 = 0) x3 x4)) (x2 x3 x4 (lam (x1 x3) x5)) (proof)
Theorem 0e173.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ι . ∀ x3 : ι → ι → ο . (∀ x4 . x4x0∀ x5 . tuple_p (x1 x4) x5∀ x6 : ι → ι . (∀ x7 . x7x1 x4c40a3.. x0 x1 x2 (ap x5 x7) (x6 x7))(∀ x7 . x7x1 x4x3 (ap x5 x7) (x6 x7))x3 (lam 2 (λ x7 . If_i (x7 = 0) x4 x5)) (x2 x4 x5 (lam (x1 x4) x6)))∀ x4 x5 . c40a3.. x0 x1 x2 x4 x5x3 x4 x5 (proof)
Known Eps_i_exEps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2x1)x1)x0 (prim0 x0)
Theorem 4d5b3.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ι . ∀ x3 . x3c8f46.. x0 x1∀ x4 : ο . (∀ x5 . c40a3.. x0 x1 x2 x3 x5x4)x4 (proof)
Definition e2778.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ι → ι . λ x3 . prim0 (c40a3.. x0 x1 x2 x3)
Theorem be97b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ι . ∀ x3 . x3c8f46.. x0 x1c40a3.. x0 x1 x2 x3 (e2778.. x0 x1 x2 x3) (proof)
Known tuple_2_injtuple_2_inj : ∀ x0 x1 x2 x3 . lam 2 (λ x5 . If_i (x5 = 0) x0 x1) = lam 2 (λ x5 . If_i (x5 = 0) x2 x3)and (x0 = x2) (x1 = x3)
Known encode_u_extencode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)lam x0 x1 = lam x0 x2
Theorem 9a9e0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ι . ∀ x3 . x3c8f46.. x0 x1∀ x4 . c40a3.. x0 x1 x2 x3 x4∀ x5 x6 . c40a3.. x0 x1 x2 x5 x6x3 = x5x4 = x6 (proof)
Theorem 2ca51.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ι . ∀ x3 . x3x0∀ x4 . tuple_p (x1 x3) x4(∀ x5 . x5x1 x3ap x4 x5c8f46.. x0 x1)e2778.. x0 x1 x2 (lam 2 (λ x6 . If_i (x6 = 0) x3 x4)) = x2 x3 x4 (lam (x1 x3) (λ x6 . e2778.. x0 x1 x2 (ap x4 x6))) (proof)

previous assets