Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCit../26bbc..
PUbVe../512bd..
vout
PrCit../808dc.. 4.91 bars
TMR6N../2a25c.. ownership of f9dcb.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMTfN../55c1d.. ownership of 9c729.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZn9../f3afd.. ownership of 4c42e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQ9C../44f8b.. ownership of 62f94.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMLkY../2a72d.. ownership of 5681c.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMLNM../6bb67.. ownership of 99164.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMY1p../f9d5c.. ownership of 4b6e2.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMT5F../eec26.. ownership of 5236a.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRub../75842.. ownership of 0e84a.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNKP../bc25c.. ownership of ffb14.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMFMJ../7a543.. ownership of be3a6.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRT2../327d8.. ownership of c21ba.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSbw../4426e.. ownership of 1f07b.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMcQJ../183b6.. ownership of 9b334.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNNM../76b7c.. ownership of f964e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMax7../fc06b.. ownership of 29ccb.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMave../72f02.. ownership of 1f384.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMadV../e37c1.. ownership of 4e462.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRxk../2a613.. ownership of 86df1.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSNX../e1b08.. ownership of f74f5.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMR9V../9c7c5.. ownership of af667.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMYiy../aacbf.. ownership of c0eb4.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMWBj../1c6db.. ownership of 9e037.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQAp../ecb02.. ownership of 8a85d.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMHUm../350b4.. ownership of d3a23.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRQU../1beeb.. ownership of b4b0b.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMVGm../5f174.. ownership of b5b60.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSMi../f8825.. ownership of d02d6.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMYXh../7fd4e.. ownership of 737c8.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRxn../54f95.. ownership of 2deda.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMN2s../c16d2.. ownership of 00076.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMWzW../0c9f5.. ownership of 5f23a.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMG5P../59ba9.. ownership of 6eb3e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMTaS../772e0.. ownership of 3ce04.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMbZu../67f7b.. ownership of 428fd.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSEU../bdcf2.. ownership of ddfd0.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMF3W../fdb86.. ownership of 5445c.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMPcQ../3739c.. ownership of 5a882.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMWG2../c6651.. ownership of 9de19.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMHcf../1a8e1.. ownership of 96902.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUr8../aa177.. ownership of f28e7.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMKJb../600e6.. ownership of 8ec16.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMY5m../2eda2.. ownership of 9b660.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMc6k../7efc6.. ownership of 86ce9.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNRm../a8ca7.. ownership of 229cb.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMKnm../0f659.. ownership of c1227.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSQN../63131.. ownership of 331bd.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSFL../16b90.. ownership of 92bfd.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMT1y../cb663.. ownership of e5bd5.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRHL../a82b2.. ownership of 39d12.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMFC6../b61b1.. ownership of bb6a5.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMLnt../c73b7.. ownership of 5b5f3.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
PUXqr../4ca31.. doc published by Pr4zB..
Definition bb6a5.. := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 . x0 (x1 x3 x2 x2 x3 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x3) (x1 x2 x3 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x2 x3 x3 x3 x3) (x1 x2 x3 x3 x2 x3 x2 x3 x3 x2 x3 x3 x3 x3 x3 x2 x3 x3) (x1 x3 x2 x2 x3 x2 x3 x3 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x3 x2 x3 x2 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3) (x1 x3 x3 x2 x3 x2 x3 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x3) (x1 x3 x2 x3 x3 x2 x3 x3 x2 x2 x3 x3 x3 x3 x3 x2 x3 x3) (x1 x2 x3 x3 x3 x3 x2 x2 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x2 x2 x3 x3 x3) (x1 x3 x3 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x2 x3 x3 x2 x3) (x1 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x3 x3 x2 x2 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x2 x3 x3 x3 x3 x3 x3 x2) (x1 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x2 x3 x3 x3 x3 x3 x2) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x3 x2) (x1 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3 x2 x3 x3 x3 x3 x2) (x1 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x2 x3)
Definition Church17_p := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x7) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x8) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x9) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x10) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x11) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x12) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x13) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x14) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x15) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x16) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x17) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x18) ⟶ x1 x0
Definition TwoRamseyGraph_3_6_Church17 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 . x0 (x1 x2 x2 x2 x3 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x3) (x1 x2 x2 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x2 x3 x3 x3 x3) (x1 x2 x3 x2 x2 x3 x2 x3 x3 x2 x3 x3 x3 x3 x3 x2 x3 x3) (x1 x3 x2 x2 x2 x2 x3 x3 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x3 x2 x2 x2 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3) (x1 x3 x3 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x3) (x1 x3 x2 x3 x3 x2 x3 x2 x2 x2 x3 x3 x3 x3 x3 x2 x3 x3) (x1 x2 x3 x3 x3 x3 x2 x2 x2 x3 x2 x3 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x2 x2 x2 x3 x3 x3) (x1 x3 x3 x3 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x3 x3 x2 x3) (x1 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x2 x3 x3 x2 x2 x3 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x2 x3 x3 x2 x2 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x2 x3 x3 x2 x3 x3 x3 x2) (x1 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x2 x3 x3 x2 x3 x3 x2) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x3 x2 x3 x2) (x1 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x2) (x1 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x2 x2)
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False ⟶ ∀ x0 : ο . x0
Theorem 9b660.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ bb6a5.. x0 x1 = TwoRamseyGraph_3_6_Church17 x0 x1 (proof)
Theorem f28e7.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ bb6a5.. x0 x0 = λ x2 x3 . x3 (proof)
Theorem 9de19.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ bb6a5.. x0 x1 = bb6a5.. x1 x0 (proof)
Param u17 : ι
Param u17_to_Church17 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι
Definition e5bd5.. := λ x0 x1 . x0 ∈ u17 ⟶ x1 ∈ u17 ⟶ bb6a5.. (u17_to_Church17 x0) (u17_to_Church17 x1) = λ x3 x4 . x3
Known db165.. : ∀ x0 . x0 ∈ u17 ⟶ Church17_p (u17_to_Church17 x0)
Theorem 5445c.. : ∀ x0 x1 . e5bd5.. x0 x1 ⟶ e5bd5.. x1 x0 (proof)
Definition Church17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x2 x4 x1 x3 x6 x8 x5 x7 x11 x9 x12 x10 x14 x15 x16 x13
Param ordsuccordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition Church17_to_u17 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x0 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16
Definition u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 := λ x0 . Church17_to_u17 (Church17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 (u17_to_Church17 x0))
Known c5926.. : u17_to_Church17 0 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x1
Theorem 428fd.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 0 = u1 (proof)
Known b0ce1.. : u17_to_Church17 u1 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x2
Theorem 6eb3e.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u1 = u3 (proof)
Known e8ec5.. : u17_to_Church17 u2 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x3
Theorem 00076.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u2 = 0 (proof)
Known 1ef08.. : u17_to_Church17 u3 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x4
Theorem 737c8.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u3 = u2 (proof)
Known 05513.. : u17_to_Church17 u4 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x5
Theorem b5b60.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u4 = u5 (proof)
Known 22977.. : u17_to_Church17 u5 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x6
Theorem d3a23.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u5 = u7 (proof)
Known 0e32a.. : u17_to_Church17 u6 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x7
Theorem 9e037.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u6 = u4 (proof)
Known b0f83.. : u17_to_Church17 u7 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x8
Theorem af667.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u7 = u6 (proof)
Known 48ba7.. : u17_to_Church17 u8 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x9
Theorem 86df1.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u8 = u10 (proof)
Known a3fb1.. : u17_to_Church17 u9 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x10
Theorem 1f384.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u9 = u8 (proof)
Known d7087.. : u17_to_Church17 u10 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x11
Theorem f964e.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u10 = u11 (proof)
Known a87a3.. : u17_to_Church17 u11 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x12
Theorem 1f07b.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u11 = u9 (proof)
Known a52d8.. : u17_to_Church17 u12 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x13
Theorem be3a6.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u12 = u13 (proof)
Known 0975c.. : u17_to_Church17 u13 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x14
Theorem 0e84a.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u13 = u14 (proof)
Known cf897.. : u17_to_Church17 u14 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x15
Theorem 4b6e2.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u14 = u15 (proof)
Known c424d.. : u17_to_Church17 u15 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x16
Theorem 5681c.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u15 = u12 (proof)
Known 480e6.. : u17_to_Church17 u16 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x17
Theorem 4c42e.. : u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u16 = u16 (proof)
Known 660da.. : ∀ x0 . x0 ∈ u16 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 x0
Known 6ec80.. : 1 ∈ 16
Known f312e.. : 3 ∈ 16
Known 2c104.. : 0 ∈ 16
Known b34ab.. : 2 ∈ 16
Known fe610.. : 5 ∈ 16
Known 64265.. : 7 ∈ 16
Known add3d.. : 4 ∈ 16
Known 6d5be.. : 6 ∈ 16
Known 662c8.. : 10 ∈ 16
Known 98f71.. : 8 ∈ 16
Known 2039c.. : 11 ∈ 16
Known fdaf0.. : 9 ∈ 16
Known e0b58.. : 13 ∈ 16
Known d4076.. : 14 ∈ 16
Known 0e6a7.. : 15 ∈ 16
Known be924.. : 12 ∈ 16
Theorem f9dcb.. : ∀ x0 . x0 ∈ u16 ⟶ u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x0 ∈ u16 (proof)