Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrJGW../32edc..
PUV8f../5dfcd..
vout
PrJGW../bb6e0.. 1.98 bars
TMM1Q../ab25f.. ownership of 17cd1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUh9../461f5.. ownership of 20fea.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG4J../b8be8.. ownership of e34e9.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRKo../86499.. ownership of a65ad.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXsG../21d93.. ownership of ae6de.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPAN../f8c8d.. ownership of 2e669.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHaZ../8acd7.. ownership of 0f09c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZ7F../8de15.. ownership of 40815.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFCo../fb63d.. ownership of 90dd1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUE5../44dc1.. ownership of e09d5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY8E../fdeae.. ownership of 4b2cb.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYgu../78831.. ownership of 975b0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP7P../b9b6a.. ownership of 8100b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRgb../53107.. ownership of ef840.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJLL../25aff.. ownership of 75cd2.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQvu../77358.. ownership of 5c468.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSQP../ab0a6.. ownership of ef6b7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMW3k../876ed.. ownership of 1cc87.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMV22../351b3.. ownership of 9b61a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbPN../08e9b.. ownership of cc40e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX9R../2e37b.. ownership of 1b56f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYLv../9af91.. ownership of a373a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLRQ../504da.. ownership of 527b1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUQa../d753d.. ownership of d34b0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJji../9a144.. ownership of 3f3ae.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJRp../1f52b.. ownership of c6b75.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSoB../fe131.. ownership of a7402.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVbg../10cdb.. ownership of badc6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQCp../bc7de.. ownership of c2196.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcKe../c4d67.. ownership of 33319.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLKa../d1fee.. ownership of af7b1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSZx../9a04b.. ownership of 207c6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRMJ../9c2ad.. ownership of 980fb.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLZS../c8e48.. ownership of a9417.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMd3../67b65.. ownership of d1d50.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFou../9b53b.. ownership of 1cae6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGEo../25822.. ownership of a6d01.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMKG../2fb92.. ownership of 8fb4d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRof../a2977.. ownership of 8c884.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYNn../8f269.. ownership of a1cd4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY9T../4d5ff.. ownership of 7c3c8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUUE../52ec3.. ownership of 2f5fb.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHmU../2bbae.. ownership of 1ba04.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMH7P../f65bb.. ownership of b53e6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHvh../38dd3.. ownership of 5571d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLWR../4cd91.. ownership of e35c4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMczB../57aa5.. ownership of d27f1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEz5../3c827.. ownership of a0b53.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMdV../c2346.. ownership of 9a5fa.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYKq../9f5a7.. ownership of e6652.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSR5../21b20.. ownership of 0b1f3.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcYP../c3153.. ownership of 38508.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWF5../4d921.. ownership of 52c1f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXk6../1556b.. ownership of 1162c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSpb../ae08c.. ownership of cd821.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKtn../a6d86.. ownership of 0596e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLsb../9a332.. ownership of b5f6e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEkN../a2079.. ownership of 79524.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNGE../c7656.. ownership of 8cdbd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUUg../4c462.. ownership of 46b31.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRuA../9a354.. ownership of 7804e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY6c../78f86.. ownership of ec957.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbkH../efaad.. ownership of b0d1f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKSR../89c9b.. ownership of 94366.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdaD../b83b2.. ownership of 914f6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSmd../b167f.. ownership of fe589.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaPK../ee55c.. ownership of 4aa6c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcfs../76239.. ownership of 830d3.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVoE../cdb52.. ownership of e2a7c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWZ7../31b64.. ownership of bfc9d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMM5K../77655.. ownership of d613a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWGk../03b37.. ownership of 8f4ea.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdxq../24fee.. ownership of 8123e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVz8../79c01.. ownership of 420ed.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcqR../0d712.. ownership of 60acf.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVVj../ba18a.. ownership of 27707.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHeX../59949.. ownership of c95dd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMH5L../e5533.. ownership of 38b5f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJza../761d1.. ownership of 1bfa8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNwz../f5132.. ownership of 65ca8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLaW../8c480.. ownership of bba79.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS9E../abfcc.. ownership of 7a150.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG2q../f3da0.. ownership of 64fce.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQhg../7ac5b.. ownership of 019eb.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGLg../a9eae.. ownership of de13a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMH5Q../a87bf.. ownership of 2e5d0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWDY../c4b5b.. ownership of 8e808.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTNk../e4627.. ownership of e122f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKQZ../bda1a.. ownership of 0c0ca.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNAA../809bd.. ownership of f82ff.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PURWH../e37a5.. doc published by PrGxv..
Param and : ο → ο → ο
Param 244aa.. : (ι → ι → ο) → ο
Param 98f68.. : (ι → ι → ο) → ο
Param 5d0c6.. : (ι → ι → ο) → ο
Param True : ο
Definition 0c0ca.. := λ x0 : ι → ι → ο . and (and (and (244aa.. x0) (98f68.. x0)) (5d0c6.. x0)) True
Param 39ffe.. : (ι → ι → ο) → ο
Param 548f8.. : (ι → ι → ο) → ο
Param 29aed.. : (ι → ι → ο) → ο
Definition 8e808.. := λ x0 : ι → ι → ο . and (and (and (39ffe.. x0) (548f8.. x0)) (29aed.. x0)) True
Definition de13a.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x0 x1) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0))))))))))))))))))))
Param 57d6a.. : ι → ι → ι
Param 67ee8.. : ι
Param 27862.. : ι
Param bcddf.. : ι → (ι → ι) → ι
Param 1f2c4.. : ι
Param 25ca3.. : ι
Param 62f06.. : ι
Param 5b8fe.. : ι
Definition 60acf.. := 57d6a.. 67ee8.. (57d6a.. 27862.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) 5b8fe..))))
Param 7a0ec.. : ι
Definition 64fce.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)))) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. x1 x2) x2))))
Definition bba79.. := λ x0 : ι → ι → ο . and (0c0ca.. x0) (x0 de13a.. 60acf..)
Param d478c.. : (ι → ι → ο) → (ι → ι → ο) → ι → ο
Conjecture 98a99.. : ∀ x0 x1 : ι → ι → ο . 0c0ca.. x0 ⟶ 8e808.. x1 ⟶ d478c.. x0 x1 60acf..
Param 6fe8d.. : (ι → ι → ο) → (ι → ι → ο) → (ι → ι → ο) → ι → ι → ο
Param 5c39b.. : ι → ι → ο
Conjecture 7abd2.. : ∀ x0 x1 : ι → ι → ο . 0c0ca.. x0 ⟶ 8e808.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 64fce.. 60acf..
Definition 1bfa8.. := λ x0 : ι → ι → ο . and (8e808.. x0) (x0 de13a.. 64fce..)
Definition c95dd.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0)))))))))))))))))))))
Definition 60acf.. := 57d6a.. 67ee8.. (57d6a.. 27862.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) 5b8fe..))))
Param f3baa.. : ι
Definition 8123e.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)))) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. x1 x2) x3)) (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. x1 x3) x4)) (57d6a.. (57d6a.. x1 x2) x4))))))))))
Definition d613a.. := λ x0 : ι → ι → ο . and (bba79.. x0) (x0 c95dd.. 60acf..)
Conjecture 9b592.. : ∀ x0 x1 : ι → ι → ο . bba79.. x0 ⟶ 1bfa8.. x1 ⟶ d478c.. x0 x1 60acf..
Conjecture 53ae6.. : ∀ x0 x1 : ι → ι → ο . bba79.. x0 ⟶ 1bfa8.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 8123e.. 60acf..
Definition e2a7c.. := λ x0 : ι → ι → ο . and (1bfa8.. x0) (x0 c95dd.. 8123e..)
Definition 4aa6c.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim1 (λ x0 . x0)))))))))))))
Definition 914f6.. := 57d6a.. 67ee8.. (57d6a.. 27862.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))))))
Param 62b32.. : ι
Param 0eacd.. : ι
Definition b0d1f.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)))) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. 62b32.. (57d6a.. (57d6a.. x1 x2) x3)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x3)))))
Definition 7804e.. := λ x0 : ι → ι → ο . and (d613a.. x0) (x0 4aa6c.. 914f6..)
Conjecture b9046.. : ∀ x0 x1 : ι → ι → ο . d613a.. x0 ⟶ e2a7c.. x1 ⟶ d478c.. x0 x1 914f6..
Conjecture a9ae7.. : ∀ x0 x1 : ι → ι → ο . d613a.. x0 ⟶ e2a7c.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. b0d1f.. 914f6..
Definition 8cdbd.. := λ x0 : ι → ι → ο . and (e2a7c.. x0) (x0 4aa6c.. b0d1f..)
Definition b5f6e.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x0 x1) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0)))))))))))))))))))))))
Param 3cd3c.. : ι
Param cb931.. : ι
Definition cd821.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)))) (λ x1 . 57d6a.. (57d6a.. de13a.. x0) (57d6a.. (57d6a.. 4aa6c.. x0) x1))))))
Param c85c4.. : ι
Definition 52c1f.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)))) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x3 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. x1 x2) x2)) x3)) (λ x4 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x2)) x3)) (λ x5 . 57d6a.. x5 (57d6a.. (57d6a.. c85c4.. x0) x2)))))))
Definition 0b1f3.. := λ x0 : ι → ι → ο . and (7804e.. x0) (x0 b5f6e.. cd821..)
Conjecture 142d8.. : ∀ x0 x1 : ι → ι → ο . 7804e.. x0 ⟶ 8cdbd.. x1 ⟶ d478c.. x0 x1 cd821..
Conjecture c382f.. : ∀ x0 x1 : ι → ι → ο . 7804e.. x0 ⟶ 8cdbd.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 52c1f.. cd821..
Definition 9a5fa.. := λ x0 : ι → ι → ο . and (8cdbd.. x0) (x0 b5f6e.. 52c1f..)
Definition d27f1.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0))))))))))))))))))))
Definition 5571d.. := 57d6a.. 67ee8.. (57d6a.. 27862.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. 27862.. (bcddf.. 1f2c4.. (λ x1 . 57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. (57d6a.. (57d6a.. 62f06.. x0) x1)) 5b8fe..))))))
Definition 1ba04.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. 1f2c4.. (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) x1))) (λ x2 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x1) (57d6a.. x2 x3)) (57d6a.. x2 x4))) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x3) x4))))))))
Definition 7c3c8.. := λ x0 : ι → ι → ο . and (0b1f3.. x0) (x0 d27f1.. 5571d..)
Conjecture 1c10a.. : ∀ x0 x1 : ι → ι → ο . 0b1f3.. x0 ⟶ 9a5fa.. x1 ⟶ d478c.. x0 x1 5571d..
Conjecture e0608.. : ∀ x0 x1 : ι → ι → ο . 0b1f3.. x0 ⟶ 9a5fa.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 1ba04.. 5571d..
Definition 8c884.. := λ x0 : ι → ι → ο . and (9a5fa.. x0) (x0 d27f1.. 1ba04..)
Definition a6d01.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0))))))))))))))))))))))
Definition a7402.. := 57d6a.. 67ee8.. (57d6a.. 27862.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) x0))) 5b8fe..))))
Definition d1d50.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) x0)))) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) (57d6a.. (57d6a.. x1 x2) x3)) (57d6a.. (57d6a.. x1 x3) x2)))))))
Definition 980fb.. := λ x0 : ι → ι → ο . and (7c3c8.. x0) (x0 a6d01.. a7402..)
Conjecture f604f.. : ∀ x0 x1 : ι → ι → ο . 7c3c8.. x0 ⟶ 8c884.. x1 ⟶ d478c.. x0 x1 a7402..
Conjecture 2a8a4.. : ∀ x0 x1 : ι → ι → ο . 7c3c8.. x0 ⟶ 8c884.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. d1d50.. a7402..
Definition af7b1.. := λ x0 : ι → ι → ο . and (8c884.. x0) (x0 a6d01.. d1d50..)
Definition c2196.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0))))))))))))))))))))))
Definition a7402.. := 57d6a.. 67ee8.. (57d6a.. 27862.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) x0))) 5b8fe..))))
Definition 3f3ae.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) x0)))) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) (57d6a.. (57d6a.. x1 (57d6a.. (57d6a.. x1 x2) x3)) x4)) (57d6a.. (57d6a.. x1 x2) (57d6a.. (57d6a.. x1 x3) x4))))))))))
Definition 527b1.. := λ x0 : ι → ι → ο . and (980fb.. x0) (x0 c2196.. a7402..)
Conjecture a8c34.. : ∀ x0 x1 : ι → ι → ο . 980fb.. x0 ⟶ af7b1.. x1 ⟶ d478c.. x0 x1 a7402..
Conjecture c1d7c.. : ∀ x0 x1 : ι → ι → ο . 980fb.. x0 ⟶ af7b1.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 3f3ae.. a7402..
Definition 1b56f.. := λ x0 : ι → ι → ο . and (af7b1.. x0) (x0 c2196.. 3f3ae..)
Definition 9b61a.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim1 (λ x0 . x0))))))))))))))))))))
Definition ef6b7.. := 57d6a.. 67ee8.. (57d6a.. 27862.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (57d6a.. (57d6a.. 62f06.. (57d6a.. (57d6a.. 62f06.. x0) x0)) 5b8fe..)))))
Definition 75cd2.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)))) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) x0))) (λ x2 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. x1 x3) x4)) (57d6a.. (57d6a.. x1 (57d6a.. x2 x3)) (57d6a.. x2 x4)))))))))
Definition 8100b.. := λ x0 : ι → ι → ο . and (527b1.. x0) (x0 9b61a.. ef6b7..)
Conjecture 66cc8.. : ∀ x0 x1 : ι → ι → ο . 527b1.. x0 ⟶ 1b56f.. x1 ⟶ d478c.. x0 x1 ef6b7..
Conjecture e7dc6.. : ∀ x0 x1 : ι → ι → ο . 527b1.. x0 ⟶ 1b56f.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 75cd2.. ef6b7..
Definition 4b2cb.. := λ x0 : ι → ι → ο . and (1b56f.. x0) (x0 9b61a.. 75cd2..)
Definition 90dd1.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0)))))))))))))))))))))))
Definition 0f09c.. := 57d6a.. 67ee8.. (57d6a.. 27862.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) x0))) (57d6a.. (57d6a.. 62f06.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) x0))) 5b8fe..)))))
Definition ae6de.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) x0)))) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) x0)))) (λ x2 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x5 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) (57d6a.. (57d6a.. x1 x3) (57d6a.. (57d6a.. x2 x4) x5))) (57d6a.. (57d6a.. x2 (57d6a.. (57d6a.. x1 x3) x4)) (57d6a.. (57d6a.. x1 x3) x5)))))))))))
Definition e34e9.. := λ x0 : ι → ι → ο . and (8100b.. x0) (x0 90dd1.. 0f09c..)
Conjecture 46c2b.. : ∀ x0 x1 : ι → ι → ο . 8100b.. x0 ⟶ 4b2cb.. x1 ⟶ d478c.. x0 x1 0f09c..
Conjecture 4c81c.. : ∀ x0 x1 : ι → ι → ο . 8100b.. x0 ⟶ 4b2cb.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. ae6de.. 0f09c..
Definition 17cd1.. := λ x0 : ι → ι → ο . and (4b2cb.. x0) (x0 90dd1.. ae6de..)
Definition e34e9.. := e34e9..
Definition 17cd1.. := 17cd1..