Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCit../f5c12..
PUX4S../79af7..
vout
PrCit../8fbc9.. 5.97 bars
TMSkR../7d30e.. ownership of 67bf8.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMEzE../13128.. ownership of 08eff.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZtc../25d6e.. ownership of 20b75.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQJe../6e5eb.. ownership of 3aee7.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUvr../f3332.. ownership of f2cf3.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMKq3../a635b.. ownership of 18558.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMR13../4997c.. ownership of 9280e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMMh8../694ef.. ownership of 88f2c.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMTCx../5a364.. ownership of 5b6f8.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMEg4../dc6aa.. ownership of 518f8.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
PrRh4../9ae35.. 0.00 bars
PrRGS../a034b.. 0.00 bars
PrJYE../41a54.. 0.00 bars
PrE35../2d9da.. 0.00 bars
PrFj7../34f60.. 0.00 bars
PrAAq../1c072.. 0.00 bars
PrKix../8a5dd.. 0.00 bars
PrB8m../0e960.. 0.00 bars
PrS2B../c899b.. 0.00 bars
Pr8Ky../d7712.. 0.00 bars
PUZeu../693bc.. doc published by Pr4zB..
Param nat_pnat_p : ιο
Param ordsuccordsucc : ιι
Definition ChurchNum_ii_6 := λ x0 : (ι → ι)ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 (x0 (x0 x1)))))
Definition ChurchNum2 := λ x0 : ι → ι . λ x1 . x0 (x0 x1)
Known f3785.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2x1 (x0 x2))∀ x2 . x1 x2x1 (ChurchNum_ii_6 ChurchNum2 x0 x2)
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Definition ChurchNum_ii_5 := λ x0 : (ι → ι)ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 (x0 x1))))
Known 9821b.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2x1 (x0 x2))∀ x2 . x1 x2x1 (ChurchNum_ii_5 ChurchNum2 x0 x2)
Known nat_3nat_3 : nat_p 3
Theorem 5b6f8.. : nat_p 99 (proof)
Param add_natadd_nat : ιιι
Definition ChurchNum_ii_3 := λ x0 : (ι → ι)ι → ι . λ x1 : ι → ι . x0 (x0 (x0 x1))
Known 93d19.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . ∀ x2 : ι → ι . (∀ x3 . x1 x3x1 (x0 x3))(∀ x3 . x1 x3x2 (x0 x3) = x0 (x2 x3))∀ x3 . x1 x3x2 (ChurchNum_ii_5 ChurchNum2 x0 x3) = ChurchNum_ii_5 ChurchNum2 x0 (x2 x3)
Known add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_9nat_9 : nat_p 9
Known 69b84.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . ∀ x2 : ι → ι . (∀ x3 . x1 x3x1 (x0 x3))(∀ x3 . x1 x3x2 (x0 x3) = x0 (x2 x3))∀ x3 . x1 x3x2 (ChurchNum_ii_3 ChurchNum2 x0 x3) = ChurchNum_ii_3 ChurchNum2 x0 (x2 x3)
Known nat_1nat_1 : nat_p 1
Known nat_0nat_0 : nat_p 0
Known add_nat_0Radd_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem 9280e.. : add_nat 99 41 = 140 (proof)
Param TwoRamseyPropTwoRamseyProp : ιιιο
Param TwoRamseyProp_atleastp : ιιιο
Known 97c7e.. : ∀ x0 x1 x2 x3 . nat_p x2nat_p x3TwoRamseyProp_atleastp (ordsucc x0) x1 x2TwoRamseyProp_atleastp x0 (ordsucc x1) x3TwoRamseyProp (ordsucc x0) (ordsucc x1) (ordsucc (add_nat x2 x3))
Known 61d53.. : nat_p 41
Param atleastpatleastp : ιιο
Known TwoRamseyProp_atleastp_atleastp : ∀ x0 x1 x2 x3 x4 . TwoRamseyProp x0 x2 x4atleastp x1 x0atleastp x3 x2TwoRamseyProp_atleastp x1 x3 x4
Known TwoRamseyProp_4_7_99 : TwoRamseyProp 4 7 99
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Known TwoRamseyProp_3_8_41 : TwoRamseyProp 3 8 41
Theorem TwoRamseyProp_4_8_141 : TwoRamseyProp 4 8 141 (proof)
Definition ChurchNum_ii_8 := λ x0 : (ι → ι)ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))
Definition ChurchNum_ii_4 := λ x0 : (ι → ι)ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 x1)))
Known b8288.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2x1 x3 (x0 x2))∀ x2 x3 . x1 x3 x2x1 x3 (ChurchNum_ii_6 ChurchNum2 x0 x2)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Known 80fa6.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2x1 x3 (x0 x2))∀ x2 x3 . x1 x3 x2x1 x3 (ChurchNum_ii_5 ChurchNum2 x0 x2)
Known 8c01a.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2x1 x3 (x0 x2))∀ x2 x3 . x1 x3 x2x1 x3 (ChurchNum_ii_4 ChurchNum2 x0 x2)
Known 1b77a.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2x1 x3 (x0 x2))∀ x2 x3 . x1 x3 x2x1 x3 (ChurchNum2 x0 x2)
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Theorem 20b75.. : 141ChurchNum_ii_8 ChurchNum2 ordsucc 0 (proof)
Known 46dcf.. : ∀ x0 x1 x2 x3 . atleastp x2 x3TwoRamseyProp x0 x1 x2TwoRamseyProp x0 x1 x3
Param exp_natexp_nat : ιιι
Known atleastp_traatleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1atleastp x1 x2atleastp x0 x2
Known bbc1b.. : exp_nat 2 8 = ChurchNum_ii_8 ChurchNum2 ordsucc 0
Known nat_In_atleastp : ∀ x0 . nat_p x0∀ x1 . x1x0atleastp x1 x0
Known 28496.. : nat_p 256
Param equipequip : ιιο
Known equip_atleastpequip_atleastp : ∀ x0 x1 . equip x0 x1atleastp x0 x1
Known equip_symequip_sym : ∀ x0 x1 . equip x0 x1equip x1 x0
Known 293d3.. : ∀ x0 . nat_p x0equip (prim4 x0) (exp_nat 2 x0)
Known nat_8nat_8 : nat_p 8
Theorem TwoRamseyProp_4_8_Power_8TwoRamseyProp_4_8_Power_8 : TwoRamseyProp 4 8 (prim4 8) (proof)