Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrQyi../621ba..
PULSH../112c2..
vout
PrQyi../2317b.. 5.78 bars
TMFgk../e9b95.. ownership of 23ec1.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdXn../498b8.. ownership of 1663e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMaBJ../54d53.. ownership of d1b1f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMR4t../c07ca.. ownership of 109cd.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMG7K../2942f.. ownership of e2503.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNHK../5dcbc.. ownership of a2428.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMUsG../d3c22.. ownership of c1eec.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMSKx../e1015.. ownership of 18844.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMY5o../dc4c2.. ownership of 1d158.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMf4../ef3e3.. ownership of 3db87.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMLBu../68d1f.. ownership of 58601.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMckW../ec597.. ownership of dd137.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPf6../34afb.. ownership of 7880c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPYL../7af15.. ownership of 24d40.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZYc../88689.. ownership of ebca8.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMP2r../52cbc.. ownership of 4ac37.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMWW5../95502.. ownership of 90cff.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMP34../150f1.. ownership of 82e80.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
PULKF../7543d.. doc published by Pr4zB..
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)
Param Church6_to_u6 : CT6 ι
Param nth_6_tuple : ιιιιιιιι
Definition u6_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 . Church6_to_u6 (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 (nth_6_tuple x0) (nth_6_tuple x1))
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
Known 39a8c.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x0)
Known bc219.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x1)
Known a050d.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x2)
Known 22a13.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x3)
Theorem ac4d2.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0∀ x1 : (ι → ι → ι → ι → ι → ι → ι) → ο . (Church6_lt4p x0x1 x0)x1 (λ x2 x3 x4 x5 x6 x7 . x6)x1 (λ x2 x3 x4 x5 x6 x7 . x7)x1 x0 (proof)
Theorem 7880c.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x1Church6_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 = permargs_i_3_2_1_0_4_5 x1 (proof)
Known 3b22d.. : Church6_p (λ x0 x1 x2 x3 x4 x5 . x3)
Known 8c295.. : Church6_p (λ x0 x1 x2 x3 x4 x5 . x2)
Known bebec.. : Church6_p (λ x0 x1 x2 x3 x4 x5 . x1)
Known 2d0c6.. : Church6_p (λ x0 x1 x2 x3 x4 x5 . x0)
Known 41e6a.. : Church6_p (λ x0 x1 x2 x3 x4 x5 . x4)
Known 28e18.. : Church6_p (λ x0 x1 x2 x3 x4 x5 . x5)
Theorem 58601.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_p x1Church6_p (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)
Param u6 : ι
Known 3ac64.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0nth_6_tuple (Church6_to_u6 x0) = x0
Known 3b8c0.. : ∀ x0 . x0u6Church6_p (nth_6_tuple x0)
Theorem 1d158.. : ∀ x0 . x0u6∀ x1 . x1u6Church6_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 (nth_6_tuple x0) (nth_6_tuple x1) = nth_6_tuple (u6_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)
Definition TwoRamseyGraph_4_6_Church6_squared_a := λ x0 x1 x2 x3 : ι → ι → ι → ι → ι → ι → ι . λ x4 x5 . x0 (x1 (x2 (x3 x4 x5 x4 x5 x4 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x5 x4 x4 x5 x5) (x3 x4 x5 x4 x4 x5 x4)) (x2 (x3 x5 x4 x5 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x4 x5 x4) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x4 x4 x4 x5 x4)) (x2 (x3 x4 x5 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x4 x4 x5 x5 x4)) (x2 (x3 x5 x4 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x4 x4 x5 x4 x5) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x4 x5 x4 x5 x4)) (x2 (x3 x4 x5 x5 x4 x4 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x5 x5 x4 x4 x4) (x3 x4 x5 x5 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x4 x4)) (x2 (x3 x5 x4 x4 x5 x5 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x5 x4 x4) (x3 x5 x4 x4 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4))) (x1 (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x5 x4 x5 x5 x4) (x3 x4 x5 x5 x5 x4 x5) (x3 x5 x4 x4 x4 x4 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x4 x5 x5 x5 x4)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x4 x5 x4 x4 x5) (x3 x5 x4 x5 x5 x5 x4) (x3 x4 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x4 x4 x5) (x3 x4 x5 x5 x5 x5 x4)) (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x4 x5 x5 x4) (x3 x5 x5 x4 x5 x4 x5) (x3 x4 x4 x5 x4 x5 x4) (x3 x4 x5 x5 x4 x5 x4) (x3 x5 x5 x5 x4 x5 x4)) (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x5 x4 x4 x5) (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x4 x4 x5 x4 x5) (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x5 x4 x5 x5 x4)) (x2 (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x4 x5 x4 x4 x4) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x5 x4) (x3 x5 x4 x5 x4 x4 x4)) (x2 (x3 x5 x4 x5 x4 x5 x5) (x3 x4 x5 x4 x5 x4 x4) (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x5) (x3 x4 x5 x4 x5 x4 x4))) (x1 (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x5 x4 x5 x4 x4)) (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x5 x5 x4 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x5 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x5 x5 x4 x4 x4)) (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x4 x4 x5) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x5 x5 x5 x4 x4)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x4 x5 x5 x4) (x3 x4 x4 x5 x5 x5 x5) (x3 x5 x4 x5 x5 x4 x4)) (x2 (x3 x4 x5 x4 x5 x4 x4) (x3 x4 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x5 x4 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x5 x4)) (x2 (x3 x5 x4 x5 x4 x4 x4) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x4 x5 x4 x4 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x4))) (x1 (x2 (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x4 x4 x4 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x4)) (x2 (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x5 x4 x4 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x5 x4 x4 x5) (x3 x4 x4 x5 x5 x4 x4)) (x2 (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x4 x5 x4 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x4)) (x2 (x3 x5 x4 x4 x5 x4 x5) (x3 x4 x4 x4 x5 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x4 x4)) (x2 (x3 x4 x5 x5 x4 x4 x4) (x3 x4 x5 x5 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x5 x5 x4 x4 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x4 x5 x5 x4)) (x2 (x3 x5 x4 x4 x5 x4 x4) (x3 x5 x4 x4 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x5 x4 x5 x4))) (x1 (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4)) (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x4 x4 x5) (x3 x4 x4 x5 x5 x5 x4)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x5 x5 x5 x5 x5) (x3 x4 x4 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x4)) (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x4 x5 x5 x5 x5) (x3 x4 x4 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x4)) (x2 (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x4 x5 x4 x4 x5) (x3 x4 x4 x4 x4 x4 x4)) (x2 (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x4 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x4) (x3 x4 x4 x4 x4 x4 x4))) (x1 (x2 (x3 x4 x5 x4 x4 x5 x5) (x3 x5 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x4)) (x2 (x3 x5 x4 x4 x4 x5 x5) (x3 x4 x5 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x4 x5 x5 x4 x4) (x3 x5 x4 x4 x5 x5 x4)) (x2 (x3 x4 x4 x4 x5 x5 x5) (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x5 x5 x5 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x5 x4 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x4)) (x2 (x3 x4 x4 x5 x4 x5 x5) (x3 x5 x5 x4 x5 x4 x5) (x3 x5 x4 x5 x5 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x5 x4 x4 x4 x4) (x3 x4 x5 x5 x4 x5 x4)) (x2 (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x4) (x3 x4 x4 x4 x4 x5 x5) (x3 x4 x4 x4 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x4)) (x2 (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4)))
Known 43ee4.. : ∀ x0 x1 x2 x3 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0Church6_lt4p x1Church6_p x2Church6_lt4p x3(TwoRamseyGraph_4_6_Church6_squared_a x0 x1 x2 x3 = λ x5 x6 . x5)TwoRamseyGraph_4_6_Church6_squared_a x0 (permargs_i_3_2_1_0_4_5 x1) x2 (permargs_i_3_2_1_0_4_5 x3) = λ x5 x6 . x5
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1)∀ x0 : ο . x0
Theorem c1eec.. : ∀ x0 x1 x2 x3 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0Church6_p x1Church6_p x2Church6_p x3(TwoRamseyGraph_4_6_Church6_squared_a x0 x1 x2 x3 = λ x5 x6 . x5)TwoRamseyGraph_4_6_Church6_squared_a x0 (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 (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 x2 x3) = λ x5 x6 . x5 (proof)
Definition TwoRamseyGraph_4_6_35_a := λ x0 x1 x2 x3 . TwoRamseyGraph_4_6_Church6_squared_a (nth_6_tuple x0) (nth_6_tuple x1) (nth_6_tuple x2) (nth_6_tuple x3) = λ x5 x6 . x5
Theorem e2503.. : ∀ x0 . x0u6∀ x1 . x1u6∀ x2 . x2u6∀ x3 . x3u6TwoRamseyGraph_4_6_35_a x0 x1 x2 x3TwoRamseyGraph_4_6_35_a x0 (u6_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 (u6_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 x2 x3) (proof)
Theorem d1b1f.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_p x1Church6_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 (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) = x1 (proof)
Known 985a3.. : ∀ x0 . x0u6Church6_to_u6 (nth_6_tuple x0) = x0
Theorem 23ec1.. : ∀ x0 . x0u6∀ x1 . x1u6u6_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 (u6_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) = x1 (proof)