Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrS2B../fa922..
PUe9x../6faf6..
vout
PrS2B../cfcab.. 0.00 bars
TMc2Z../cf432.. ownership of 5bea3.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMUcA../7fff5.. ownership of 2a3ea.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMyX../3f450.. ownership of ca554.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHnw../9569d.. ownership of e2935.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMS8h../3592f.. ownership of 3a34f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMaeC../39955.. ownership of 22158.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
PUbvB../e769d.. doc published by Pr4zB..
Definition Church6_p := λ x0 : ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 . x2)x1 (λ x2 x3 x4 x5 x6 x7 . x3)x1 (λ x2 x3 x4 x5 x6 x7 . x4)x1 (λ x2 x3 x4 x5 x6 x7 . x5)x1 (λ x2 x3 x4 x5 x6 x7 . x6)x1 (λ x2 x3 x4 x5 x6 x7 . x7)x1 x0
Definition Church6_lt4p := λ x0 : ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 . x2)x1 (λ x2 x3 x4 x5 x6 x7 . x3)x1 (λ x2 x3 x4 x5 x6 x7 . x4)x1 (λ x2 x3 x4 x5 x6 x7 . x5)x1 x0
Definition permargs_i_1_0_3_2_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 . x0 x2 x1 x4 x3
Definition Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι . λ x2 x3 x4 x5 x6 x7 . x0 (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x6 x7)
Known 3f4a9.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x0Church6_lt4p (permargs_i_1_0_3_2_4_5 x0)
Known bc219.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x1)
Known 39a8c.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x0)
Known 22a13.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x3)
Known a050d.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x2)
Theorem 3a34f.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x1Church6_lt4p (Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 x0 x1) (proof)
Definition permargs_i_2_3_0_1_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 . x0 x3 x4 x1 x2
Definition Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι . λ x2 x3 x4 x5 x6 x7 . x0 (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7)
Known bc9c2.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x0Church6_lt4p (permargs_i_2_3_0_1_4_5 x0)
Theorem ca554.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x1Church6_lt4p (Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 x0 x1) (proof)
Definition permargs_i_3_2_1_0_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 . x0 x4 x3 x2 x1
Definition Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι . λ x2 x3 x4 x5 x6 x7 . x0 (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x6 x7)
Known bcfec.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x0Church6_lt4p (permargs_i_3_2_1_0_4_5 x0)
Theorem 5bea3.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x1Church6_lt4p (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x0 x1) (proof)