Search for blocks/addresses/...

Proofgold Asset

asset id
693bc215a70a650edb25b2d547ae5e0528d312dbbcbacef3e70295e93f9ff3d7
asset hash
3b0cfc544fdb42e0bc398b8db5bda9b9c1623d154486876be11be490308d4cb9
bday / block
15602
tx
e94e7..
preasset
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)