Search for blocks/addresses/...

Proofgold Asset

asset id
cd427e3e2051ff0c43e44cb749918761c2ccb34829f4f2f548973befec3e6c92
asset hash
8f355f0f83f346d521fd72e829df4900c6079d741adb7f42b7ab89a51d95e5a0
bday / block
4892
tx
d4a74..
preasset
doc published by Pr6Pc..
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Theorem exandE_iexandE_i : ∀ x0 x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x0 x3) (x1 x3)x2)x2)∀ x2 : ο . (∀ x3 . x0 x3x1 x3x2)x2 (proof)
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition If_Vo4If_Vo4 := λ x0 : ο . λ x1 x2 : (((ι → ο) → ο) → ο) → ο . λ x3 : ((ι → ο) → ο) → ο . and (x0x1 x3) (not x0x2 x3)
Known prop_ext_2prop_ext_2 : ∀ x0 x1 : ο . (x0x1)(x1x0)x0 = x1
Known andELandEL : ∀ x0 x1 : ο . and x0 x1x0
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known FalseEFalseE : False∀ x0 : ο . x0
Known notEnotE : ∀ x0 : ο . not x0x0False
Theorem If_Vo4_1If_Vo4_1 : ∀ x0 : ο . ∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . x0If_Vo4 x0 x1 x2 = x1 (proof)
Known andERandER : ∀ x0 x1 : ο . and x0 x1x1
Theorem If_Vo4_0If_Vo4_0 : ∀ x0 : ο . ∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . not x0If_Vo4 x0 x1 x2 = x2 (proof)
Definition Descr_Vo4Descr_Vo4 := λ x0 : ((((ι → ο) → ο) → ο) → ο) → ο . λ x1 : ((ι → ο) → ο) → ο . ∀ x2 : (((ι → ο) → ο) → ο) → ο . x0 x2x2 x1
Theorem Descr_Vo4_propDescr_Vo4_prop : ∀ x0 : ((((ι → ο) → ο) → ο) → ο) → ο . (∀ x1 : ο . (∀ x2 : (((ι → ο) → ο) → ο) → ο . x0 x2x1)x1)(∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . x0 x1x0 x2x1 = x2)x0 (Descr_Vo4 x0) (proof)
Definition 461b4.. := λ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο)(((ι → ο) → ο) → ο) → ο . λ x1 . λ x2 : (((ι → ο) → ο) → ο) → ο . ∀ x3 : ι → ((((ι → ο) → ο) → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x6 . x6x4x3 x6 (x5 x6))x3 x4 (x0 x4 x5))x3 x1 x2
Definition In_rec_Vo4In_rec_Vo4 := λ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο)(((ι → ο) → ο) → ο) → ο . λ x1 . Descr_Vo4 (461b4.. x0 x1)
Theorem 23e18.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο)(((ι → ο) → ο) → ο) → ο . ∀ x1 . ∀ x2 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x3 . x3x1461b4.. x0 x3 (x2 x3))461b4.. x0 x1 (x0 x1 x2) (proof)
Theorem 45e15.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο)(((ι → ο) → ο) → ο) → ο . ∀ x1 . ∀ x2 : (((ι → ο) → ο) → ο) → ο . 461b4.. x0 x1 x2∀ x3 : ο . (∀ x4 : ι → (((ι → ο) → ο) → ο) → ο . and (∀ x5 . x5x1461b4.. x0 x5 (x4 x5)) (x2 = x0 x1 x4)x3)x3 (proof)
Known In_indIn_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . x0 x1
Theorem 87941.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο)(((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . ∀ x2 x3 : (((ι → ο) → ο) → ο) → ο . 461b4.. x0 x1 x2461b4.. x0 x1 x3x2 = x3 (proof)
Theorem 6dcc7.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο)(((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . 461b4.. x0 x1 (In_rec_Vo4 x0 x1) (proof)
Theorem 05f75.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο)(((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . 461b4.. x0 x1 (x0 x1 (In_rec_Vo4 x0)) (proof)
Theorem In_rec_Vo4_eqIn_rec_Vo4_eq : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο)(((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_Vo4 x0 x1 = x0 x1 (In_rec_Vo4 x0) (proof)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known not_and_or_demorgannot_and_or_demorgan : ∀ x0 x1 : ο . not (and x0 x1)or (not x0) (not x1)
Theorem eq_imp_oreq_imp_or : (λ x1 x2 : ο . x1x2) = λ x1 : ο . or (not x1) (proof)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Definition nInnIn := λ x0 x1 . not (x0x1)
Known Subq_contraSubq_contra : ∀ x0 x1 x2 . x0x1nIn x2 x1nIn x2 x0
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known Subq_EmptySubq_Empty : ∀ x0 . 0x0
Known Empty_Subq_eqEmpty_Subq_eq : ∀ x0 . x00x0 = 0
Known Empty_eqEmpty_eq : ∀ x0 . (∀ x1 . nIn x1 x0)x0 = 0
Known UnionEUnionE : ∀ x0 x1 . x1prim3 x0∀ x2 : ο . (∀ x3 . and (x1x3) (x3x0)x2)x2
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Known Union_EmptyUnion_Empty : prim3 0 = 0
Known PowerEPowerE : ∀ x0 x1 . x1prim4 x0x1x0
Known Union_Power_SubqUnion_Power_Subq : ∀ x0 . prim3 (prim4 x0)x0
Known ReplE_impredReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . x4x0x2 = x1 x4x3)x3
Known Repl_EmptyRepl_Empty : ∀ x0 : ι → ι . prim5 0 x0 = 0
Known ReplIReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0x1 x2prim5 x0 x1
Known ReplEq_ext_subReplEq_ext_sub : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)prim5 x0 x1prim5 x0 x2
Known ReplEq_extReplEq_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)prim5 x0 x1 = prim5 x0 x2
Param UPairUPair : ιιι
Known UPairEUPairE : ∀ x0 x1 x2 . x0UPair x1 x2or (x0 = x1) (x0 = x2)
Known UPairI2UPairI2 : ∀ x0 x1 . x1UPair x0 x1
Known UPairI1UPairI1 : ∀ x0 x1 . x0UPair x0 x1
Known 93b47.. : ∀ x0 x1 . UPair x0 x1UPair x1 x0
Known UPair_comUPair_com : ∀ x0 x1 . UPair x0 x1 = UPair x1 x0
Param binunionbinunion : ιιι
Param SingSing : ιι
Definition SetAdjoinSetAdjoin := λ x0 x1 . binunion x0 (Sing x1)
Known SingISingI : ∀ x0 . x0Sing x0
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known Empty_In_PowerEmpty_In_Power : ∀ x0 . 0prim4 x0
Known Power_0_Sing_0Power_0_Sing_0 : prim4 0 = Sing 0
Known Repl_UPairRepl_UPair : ∀ x0 : ι → ι . ∀ x1 x2 . prim5 (UPair x1 x2) x0 = UPair (x0 x1) (x0 x2)
Known Repl_SingRepl_Sing : ∀ x0 : ι → ι . ∀ x1 . prim5 (Sing x1) x0 = Sing (x0 x1)
Known ReplEReplE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . and (x4x0) (x2 = x1 x4)x3)x3
Known ReplEq_ext_subReplEq_ext_sub : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)prim5 x0 x1prim5 x0 x2
Known ReplEq_extReplEq_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)prim5 x0 x1 = prim5 x0 x2
Definition famunionfamunion := λ x0 . λ x1 : ι → ι . prim3 (prim5 x0 x1)
Known UnionIUnionI : ∀ x0 x1 x2 . x1x2x2x0x1prim3 x0
Known famunionIfamunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2x0x3x1 x2x3famunion x0 x1
Known UnionE_impredUnionE_impred : ∀ x0 x1 . x1prim3 x0∀ x2 : ο . (∀ x3 . x1x3x3x0x2)x2
Known famunionEfamunionE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2famunion x0 x1∀ x3 : ο . (∀ x4 . and (x4x0) (x2x1 x4)x3)x3
Known famunionE_impredfamunionE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2famunion x0 x1∀ x3 : ο . (∀ x4 . x4x0x2x1 x4x3)x3
Known UnionEq_famunionIdUnionEq_famunionId : ∀ x0 . prim3 x0 = famunion x0 (λ x2 . x2)
Known ReplEq_famunion_SingReplEq_famunion_Sing : ∀ x0 . ∀ x1 : ι → ι . prim5 x0 x1 = famunion x0 (λ x3 . Sing (x1 x3))
Theorem Empty_or_exEmpty_or_ex : ∀ x0 . or (x0 = 0) (∀ x1 : ο . (∀ x2 . x2x0x1)x1) (proof)