Search for blocks/addresses/...

Proofgold Address

address
PUPXDb7BqYSSwGqPwS1z32JaH8FMqjckyBj
total
0
mg
-
conjpub
-
current assets
fb350../d7729.. bday: 4945 doc published by Pr6Pc..
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition bijbij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)) (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Theorem bijIbijI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3x0x2 x3x1)(∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)(∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)bij x0 x1 x2 (proof)
Theorem bijEbijE : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2∀ x3 : ο . ((∀ x4 . x4x0x2 x4x1)(∀ x4 . x4x0∀ x5 . x5x0x2 x4 = x2 x5x4 = x5)(∀ x4 . x4x1∀ x5 : ο . (∀ x6 . and (x6x0) (x2 x6 = x4)x5)x5)x3)x3 (proof)
Definition equipequip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3x2)x2
Known bij_idbij_id : ∀ x0 . bij x0 x0 (λ x1 . x1)
Theorem equip_refequip_ref : ∀ x0 . equip x0 x0 (proof)
Param invinv : ι(ιι) → ιι
Known bij_invbij_inv : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2bij x1 x0 (inv x0 x2)
Theorem equip_symequip_sym : ∀ x0 x1 . equip x0 x1equip x1 x0 (proof)
Known bij_compbij_comp : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . bij x0 x1 x3bij x1 x2 x4bij x0 x2 (λ x5 . x4 (x3 x5))
Theorem equip_traequip_tra : ∀ x0 x1 x2 . equip x0 x1equip x1 x2equip x0 x2 (proof)

previous assets