Search for blocks/addresses/...

Proofgold Address

address
PUVC91u6nXd1RkYDeaCNbxY1RZPHSJAr9SP
total
0
mg
-
conjpub
-
current assets
4bb26../080a7.. bday: 4672 doc published by PrGxv..
Definition a813b.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . λ x4 : ι → ι → ι . λ x5 x6 . ∀ x7 : ι → ι → ο . x7 x1 x3(∀ x8 . prim1 x8 x0∀ x9 . x7 x8 x9x7 (x2 x8) (x4 x8 x9))x7 x5 x6
Param explicit_Nats : ιι(ιι) → ο
Known explicit_Nats_ind : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 : ι → ο . x3 x1(∀ x4 . prim1 x4 x0x3 x4x3 (x2 x4))∀ x4 . prim1 x4 x0x3 x4
Theorem 89666.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2∀ x5 . prim1 x5 x0∀ x6 : ο . (∀ x7 . a813b.. x0 x1 x2 x3 x4 x5 x7x6)x6 (proof)
Known explicit_Nats_E : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ο . (explicit_Nats x0 x1 x2prim1 x1 x0(∀ x4 . prim1 x4 x0prim1 (x2 x4) x0)(∀ x4 . prim1 x4 x0x2 x4 = x1∀ x5 : ο . x5)(∀ x4 . prim1 x4 x0∀ x5 . prim1 x5 x0x2 x4 = x2 x5x4 = x5)(∀ x4 : ι → ο . x4 x1(∀ x5 . x4 x5x4 (x2 x5))∀ x5 . prim1 x5 x0x4 x5)x3)explicit_Nats x0 x1 x2x3
Definition False := ∀ x0 : ο . x0
Known FalseE : False∀ x0 : ο . x0
Theorem 45784.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2∀ x5 . a813b.. x0 x1 x2 x3 x4 x1 x5x5 = x3 (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known andI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem 0bfdd.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2∀ x5 . prim1 x5 x0∀ x6 . a813b.. x0 x1 x2 x3 x4 (x2 x5) x6∀ x7 : ο . (∀ x8 . and (x6 = x4 x5 x8) (a813b.. x0 x1 x2 x3 x4 x5 x8)x7)x7 (proof)
Theorem f1675.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2∀ x5 . prim1 x5 x0∀ x6 x7 . a813b.. x0 x1 x2 x3 x4 x5 x6a813b.. x0 x1 x2 x3 x4 x5 x7x6 = x7 (proof)
Definition explicit_Nats_primrec := λ x0 x1 . λ x2 : ι → ι . λ x3 . λ x4 : ι → ι → ι . λ x5 . prim0 (a813b.. x0 x1 x2 x3 x4 x5)
Theorem 89666.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2∀ x5 . prim1 x5 x0∀ x6 : ο . (∀ x7 . a813b.. x0 x1 x2 x3 x4 x5 x7x6)x6 (proof)
Known Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2x1)x1)x0 (prim0 x0)
Theorem 1347b.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2∀ x5 . prim1 x5 x0a813b.. x0 x1 x2 x3 x4 x5 (explicit_Nats_primrec x0 x1 x2 x3 x4 x5) (proof)
Theorem explicit_Nats_primrec_base : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2explicit_Nats_primrec x0 x1 x2 x3 x4 x1 = x3 (proof)
Theorem explicit_Nats_primrec_S : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2∀ x5 . prim1 x5 x0explicit_Nats_primrec x0 x1 x2 x3 x4 (x2 x5) = x4 x5 (explicit_Nats_primrec x0 x1 x2 x3 x4 x5) (proof)
Definition explicit_Nats_zero_plus := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . explicit_Nats_primrec x0 x1 x2 x4 (λ x5 . x2) x3
Definition explicit_Nats_zero_mult := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . explicit_Nats_primrec x0 x1 x2 x1 (λ x5 . explicit_Nats_zero_plus x0 x1 x2 x4) x3
Theorem explicit_Nats_zero_plus_0L : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . prim1 x3 x0explicit_Nats_zero_plus x0 x1 x2 x1 x3 = x3 (proof)
Theorem explicit_Nats_zero_plus_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . prim1 x3 x0∀ x4 . prim1 x4 x0explicit_Nats_zero_plus x0 x1 x2 (x2 x3) x4 = x2 (explicit_Nats_zero_plus x0 x1 x2 x3 x4) (proof)
Theorem explicit_Nats_zero_mult_0L : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . prim1 x3 x0explicit_Nats_zero_mult x0 x1 x2 x1 x3 = x1 (proof)
Theorem explicit_Nats_zero_mult_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . prim1 x3 x0∀ x4 . prim1 x4 x0explicit_Nats_zero_mult x0 x1 x2 (x2 x3) x4 = explicit_Nats_zero_plus x0 x1 x2 x4 (explicit_Nats_zero_mult x0 x1 x2 x3 x4) (proof)
Definition explicit_Nats_one_plus := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . explicit_Nats_primrec x0 x1 x2 (x2 x4) (λ x5 . x2) x3
Definition explicit_Nats_one_mult := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . explicit_Nats_primrec x0 x1 x2 x4 (λ x5 . explicit_Nats_one_plus x0 x1 x2 x4) x3
Definition explicit_Nats_one_exp := λ x0 x1 . λ x2 : ι → ι . λ x3 . explicit_Nats_primrec x0 x1 x2 x3 (λ x4 . explicit_Nats_one_mult x0 x1 x2 x3)
Theorem explicit_Nats_one_plus_1L : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . prim1 x3 x0explicit_Nats_one_plus x0 x1 x2 x1 x3 = x2 x3 (proof)
Theorem explicit_Nats_one_plus_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . prim1 x3 x0∀ x4 . prim1 x4 x0explicit_Nats_one_plus x0 x1 x2 (x2 x3) x4 = x2 (explicit_Nats_one_plus x0 x1 x2 x3 x4) (proof)
Theorem explicit_Nats_one_mult_1L : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . prim1 x3 x0explicit_Nats_one_mult x0 x1 x2 x1 x3 = x3 (proof)
Theorem explicit_Nats_one_mult_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . prim1 x3 x0∀ x4 . prim1 x4 x0explicit_Nats_one_mult x0 x1 x2 (x2 x3) x4 = explicit_Nats_one_plus x0 x1 x2 x4 (explicit_Nats_one_mult x0 x1 x2 x3 x4) (proof)
Theorem explicit_Nats_one_exp_1L : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . prim1 x3 x0explicit_Nats_one_exp x0 x1 x2 x3 x1 = x3 (proof)
Theorem explicit_Nats_one_exp_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . prim1 x3 x0∀ x4 . prim1 x4 x0explicit_Nats_one_exp x0 x1 x2 x3 (x2 x4) = explicit_Nats_one_mult x0 x1 x2 x3 (explicit_Nats_one_exp x0 x1 x2 x3 x4) (proof)

previous assets