Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrJGW../77b48..
PUcsN../06be1..
vout
PrJGW../ce3fa.. 1.97 bars
TMS4o../cdb81.. ownership of 34df7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGHp../55598.. ownership of e6518.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZ7k../6893c.. ownership of 605a7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJdP../6b754.. ownership of 7f9eb.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNbz../4cf80.. ownership of 3404c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMV3W../de864.. ownership of 8f9f0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLzN../8fde8.. ownership of 3cfc6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYak../f4993.. ownership of 41da6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMW4z../dfc5f.. ownership of 2192a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG86../749a7.. ownership of 8cece.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMDW../437a3.. ownership of 0a564.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa4E../b5053.. ownership of 23c67.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY3J../83b9f.. ownership of fdff9.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRuV../d362b.. ownership of 0c56a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJEj../caace.. ownership of d31e4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNyP../70be6.. ownership of 95674.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZHt../61239.. ownership of 6dc4c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ7k../48ad7.. ownership of efe71.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMabm../ca0a3.. ownership of 1031e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSZ3../b7f91.. ownership of 019d9.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMavg../f01bf.. ownership of 55863.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJFZ../f54e6.. ownership of 16dfc.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXHr../e8068.. ownership of 117bd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNYj../77517.. ownership of 63d37.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPUj../c3f46.. ownership of 33a91.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF31../7145e.. ownership of 5195a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNJg../24f6f.. ownership of 26a87.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFrC../76cc3.. ownership of 929d0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbte../921f9.. ownership of e39f2.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFkA../b83bd.. ownership of 71c71.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKWj../2e675.. ownership of dc7e8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFcg../f4289.. ownership of 08c8c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVMy../1a0b5.. ownership of 53569.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYAx../1165b.. ownership of 7df90.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZfj../918b9.. ownership of a0e3f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSVC../fa2f3.. ownership of ad009.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWjQ../c3dca.. ownership of 9f378.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXyi../37963.. ownership of 10aef.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVhc../27926.. ownership of c7956.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbZh../0c4a3.. ownership of 31cbd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJeC../fd385.. ownership of 4a327.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFzG../9b3b4.. ownership of 9d1c8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZNx../b39e3.. ownership of 679d8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQBg../dc4e5.. ownership of 5987c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJCF../eaf40.. ownership of 9ed8f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGfZ../e75ce.. ownership of b46ef.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMLN../cd983.. ownership of c7fbc.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSkY../4212c.. ownership of afa9d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMHH../9fdbc.. ownership of 3ea55.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGBh../1b7b4.. ownership of c644d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMd4K../99af5.. ownership of ca802.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLhB../dc3a7.. ownership of 8530a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZUA../2489e.. ownership of aed70.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYcd../7bdd3.. ownership of 8f250.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTBW../e3460.. ownership of 81d91.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdHB../9c1e1.. ownership of 69f94.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaiC../0fa33.. ownership of 3edb3.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVYw../47257.. ownership of 94f6d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa2y../25249.. ownership of 879d0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYn9../96f88.. ownership of 4597c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNHZ../0301e.. ownership of 86d33.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKjV../a00f7.. ownership of ccb36.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZtD../e14d5.. ownership of e4293.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJjb../d75d7.. ownership of 8f8cd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJQp../eac33.. ownership of 82bc1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKGT../5c55b.. ownership of 1a1c8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLvR../0eeed.. ownership of b3869.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaxo../598f8.. ownership of d4be8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSts../806a6.. ownership of 79f98.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMamb../a3557.. ownership of fdfc1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMas8../cb055.. ownership of 68987.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWcA../5675a.. ownership of 9f7bb.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMW9u../3a9a8.. ownership of b9cfa.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN2X../3ce41.. ownership of be7bc.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLXg../9efe1.. ownership of f8137.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdVk../81562.. ownership of 2baa5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQyk../aadc1.. ownership of 1e741.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMW2F../8aadd.. ownership of 8893a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZdR../42c93.. ownership of 6e880.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS66../0638e.. ownership of 30718.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaDg../a3e9d.. ownership of 7f199.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJrM../f9959.. ownership of 23a8a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUrA../e03b0.. ownership of 2fce4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaf9../baaca.. ownership of 4aecc.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHAx../61684.. ownership of fa10d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZdB../a457d.. ownership of 8c1b7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMR37../25944.. ownership of 8ff2e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZpE../a2cad.. ownership of b9895.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ5S../8e58e.. ownership of 9761f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGmN../0b0b4.. ownership of dac31.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUCx../1823d.. ownership of 15a56.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXj6../7571a.. ownership of d1c2a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJqS../995fc.. ownership of e9f3d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZZc../e35b9.. ownership of ff98c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFH9../6e882.. ownership of 5da20.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMH8k../cc0e7.. ownership of b15d1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQqk../6c7a5.. ownership of 14a9a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLBD../5ccac.. ownership of 0231e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYrW../dcb91.. ownership of 76102.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXbA../f1d08.. ownership of 6841b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa3w../30684.. ownership of 3cfef.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMqY../d577c.. ownership of d64a3.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcDw../c4090.. ownership of c7112.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc24../6597a.. ownership of 0d687.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa63../d26b4.. ownership of caa73.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXu9../f8c32.. ownership of c5fb2.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdE2../71008.. ownership of 780a9.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRAb../4de66.. ownership of 26052.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPNn../6c8e9.. ownership of 9d195.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLuL../7607d.. ownership of 5c752.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGYD../09bbc.. ownership of 7af9e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWfV../a4b35.. ownership of d4de7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXEC../4b0be.. ownership of 74351.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFeB../3c83a.. ownership of 84b7a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMU7c../5b2b0.. ownership of d86d6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMbJ../10d7e.. ownership of 4c927.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYn1../f9bfe.. ownership of 3ece5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK2s../6396d.. ownership of 7fd20.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMuX../39293.. ownership of 0f581.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbKX../d5fd6.. ownership of ac04c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWeG../853bb.. ownership of 02131.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJZT../788bb.. ownership of 8c05b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFwG../ccf42.. ownership of f73d5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWKm../1e90f.. ownership of 6302f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcAt../ef0af.. ownership of 6c7e1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXa5../897d3.. ownership of 9a614.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbYW../fbf09.. ownership of 65996.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKph../eaabd.. ownership of 07d23.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTct../e93fa.. ownership of 10817.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaNi../c7af9.. ownership of b54c4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaV6../bdaaf.. ownership of 9c473.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJzx../fc00f.. ownership of a0640.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUNEB../c29a4.. doc published by PrGxv..
Param and : ο → ο → ο
Param 244aa.. : (ι → ι → ο) → ο
Param 98f68.. : (ι → ι → ο) → ο
Param e34e9.. : (ι → ι → ο) → ο
Param 5d0c6.. : (ι → ι → ο) → ο
Param True : ο
Definition 9c473.. := λ x0 : ι → ι → ο . and (and (and (and (244aa.. x0) (98f68.. x0)) (e34e9.. x0)) (5d0c6.. x0)) True
Param 39ffe.. : (ι → ι → ο) → ο
Param 548f8.. : (ι → ι → ο) → ο
Param 17cd1.. : (ι → ι → ο) → ο
Param 29aed.. : (ι → ι → ο) → ο
Definition 10817.. := λ x0 : ι → ι → ο . and (and (and (and (39ffe.. x0) (548f8.. x0)) (17cd1.. x0)) (29aed.. x0)) True
Definition 65996.. := 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 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 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 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 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0))))))))))
Param 1f2c4.. : ι
Definition 1f2c4.. := 1f2c4..
Definition 6c7e1.. := λ x0 : ι → ι → ο . and (9c473.. x0) (x0 65996.. 1f2c4..)
Param d478c.. : (ι → ι → ο) → (ι → ι → ο) → ι → ο
Conjecture 24dae.. : ∀ x0 x1 : ι → ι → ο . 9c473.. x0 ⟶ 10817.. x1 ⟶ d478c.. x0 x1 1f2c4..
Definition f73d5.. := 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 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 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 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 x0)) (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 x1 x0))))) (prim1 (λ x0 . x0))))))))))
Param 57d6a.. : ι → ι → ι
Param 67ee8.. : ι
Param 25ca3.. : ι
Definition 3ece5.. := 57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)
Definition 02131.. := λ x0 : ι → ι → ο . and (6c7e1.. x0) (x0 f73d5.. 3ece5..)
Conjecture d24fe.. : ∀ x0 x1 : ι → ι → ο . 6c7e1.. x0 ⟶ 10817.. x1 ⟶ d478c.. x0 x1 3ece5..
Definition 0f581.. := 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 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 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 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 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 x1 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 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0)))))))))))
Definition 3ece5.. := 57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)
Definition d86d6.. := λ x0 : ι → ι → ο . and (02131.. x0) (x0 0f581.. 3ece5..)
Conjecture 97f0d.. : ∀ x0 x1 : ι → ι → ο . 02131.. x0 ⟶ 10817.. x1 ⟶ d478c.. x0 x1 3ece5..
Definition 74351.. := 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 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 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 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 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 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x1))))) (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 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 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 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 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x1))))) (prim1 (λ x0 . x0)))))))))))))))))))))
Param 3cd3c.. : ι
Param 7a0ec.. : ι
Param 62f06.. : ι
Param 5b8fe.. : ι
Param bcddf.. : ι → (ι → ι) → ι
Param f3baa.. : ι
Definition 7af9e.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. 65996..) 5b8fe..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. 65996..) 5b8fe..))) (λ x0 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x0 f73d5..)) (57d6a.. (57d6a.. f3baa.. (57d6a.. x0 0f581..)) (57d6a.. (57d6a.. 7a0ec.. 65996..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (57d6a.. x0)))))))
Definition 9d195.. := λ x0 : ι → ι → ο . and (d86d6.. x0) (x0 74351.. 7af9e..)
Conjecture 04b9e.. : ∀ x0 x1 : ι → ι → ο . d86d6.. x0 ⟶ 10817.. x1 ⟶ d478c.. x0 x1 7af9e..
Definition 780a9.. := 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 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 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 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 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 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x1))))) (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 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 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 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 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 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 27862.. : ι
Definition caa73.. := 57d6a.. 67ee8.. (57d6a.. 27862.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. 65996..) x0))))))
Definition c7112.. := λ x0 : ι → ι → ο . and (9d195.. x0) (x0 780a9.. caa73..)
Conjecture f2b08.. : ∀ x0 x1 : ι → ι → ο . 9d195.. x0 ⟶ 10817.. x1 ⟶ d478c.. x0 x1 caa73..
Definition 3cfef.. := 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 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 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 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 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 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 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x1))))) (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 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 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 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 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (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 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 x0)) (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 x1 x0))))) (prim1 (λ x0 . x0)))))))))))))))))))))))))))))
Param cb931.. : ι
Param 5bcaf.. : ι
Definition 76102.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. (57d6a.. 5bcaf.. x0) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. x0) x1) x2) f73d5..)) x1)))))))
Definition 14a9a.. := λ x0 : ι → ι → ο . and (c7112.. x0) (x0 3cfef.. 76102..)
Conjecture bb904.. : ∀ x0 x1 : ι → ι → ο . c7112.. x0 ⟶ 10817.. x1 ⟶ d478c.. x0 x1 76102..
Definition 5da20.. := 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 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 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 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 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 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 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x1))))) (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 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 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 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 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (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 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 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 x1 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 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0))))))))))))))))))))))))))))))
Definition e9f3d.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. (57d6a.. 5bcaf.. x0) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. x0) x1) x2) 0f581..)) x2)))))))
Definition 15a56.. := λ x0 : ι → ι → ο . and (14a9a.. x0) (x0 5da20.. e9f3d..)
Conjecture a0000.. : ∀ x0 x1 : ι → ι → ο . 14a9a.. x0 ⟶ 10817.. x1 ⟶ d478c.. x0 x1 e9f3d..
Definition 9761f.. := 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 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 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 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (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 x1 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 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 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 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x1))))) (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 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 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 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 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (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 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 x0)) (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 x1 x0))))) (prim1 (λ x0 . x0)))))))))))))))))))))))))))))))))
Definition 8ff2e.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. (57d6a.. 5bcaf.. x0) x1) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. x0) x1) x2) f73d5..))))))))
Param de260.. : ι
Definition fa10d.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. de260.. x0) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. x0) x1) x2) f73d5..)) x1) (57d6a.. (57d6a.. (57d6a.. 3cfef.. x0) x1) x2))))
Definition 2fce4.. := λ x0 : ι → ι → ο . and (15a56.. x0) (x0 9761f.. 8ff2e..)
Conjecture 7b5ff.. : ∀ x0 x1 : ι → ι → ο . 15a56.. x0 ⟶ 10817.. x1 ⟶ d478c.. x0 x1 8ff2e..
Param 6fe8d.. : (ι → ι → ο) → (ι → ι → ο) → (ι → ι → ο) → ι → ι → ο
Param 5c39b.. : ι → ι → ο
Conjecture 50215.. : ∀ x0 x1 : ι → ι → ο . 15a56.. x0 ⟶ 10817.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. fa10d.. 8ff2e..
Definition 7f199.. := λ x0 : ι → ι → ο . and (10817.. x0) (x0 9761f.. fa10d..)
Definition 6e880.. := 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 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 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 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (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 x1 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 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 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 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x1))))) (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 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 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 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 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (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 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 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 x1 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 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0))))))))))))))))))))))))))))))))))
Definition 1e741.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. (57d6a.. 5bcaf.. x0) x2) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. x0) x1) x2) 0f581..))))))))
Definition f8137.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. de260.. x0) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. x0) x1) x2) 0f581..)) x2) (57d6a.. (57d6a.. (57d6a.. 5da20.. x0) x1) x2))))
Definition b9cfa.. := λ x0 : ι → ι → ο . and (2fce4.. x0) (x0 6e880.. 1e741..)
Conjecture ec7d3.. : ∀ x0 x1 : ι → ι → ο . 2fce4.. x0 ⟶ 7f199.. x1 ⟶ d478c.. x0 x1 1e741..
Conjecture ed346.. : ∀ x0 x1 : ι → ι → ο . 2fce4.. x0 ⟶ 7f199.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. f8137.. 1e741..
Definition 68987.. := λ x0 : ι → ι → ο . and (7f199.. x0) (x0 6e880.. f8137..)
Definition 79f98.. := 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 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 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 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 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 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 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 x1)) (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 x1))))) (prim1 (λ x0 . x0))))))))))))))))
Param 0eacd.. : ι
Definition b3869.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 65996..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x0 . 57d6a.. (57d6a.. 7a0ec.. 65996..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x0) x1)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. x2) x2)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . x2)))) x1)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . x2)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. x2) x2)))) x1)) x0))))))
Param 81b7d.. : ι
Definition 82bc1.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x1 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x0) x1)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 81b7d.. 65996..) x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x2 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x3 . 57d6a.. (57d6a.. f3baa.. x3) x3)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x3 . x3)))) x2)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x3 . x3)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x3 . 57d6a.. (57d6a.. f3baa.. x3) x3)))) x2)) x0))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 74351.. (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x2 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x3 . 57d6a.. (57d6a.. f3baa.. x3) x3)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x3 . x3)))) x2)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x3 . x3)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x3 . 57d6a.. (57d6a.. f3baa.. x3) x3)))) x2)) x2))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 9761f.. 5b8fe..) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. x2) x2)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . x2)))) f73d5..)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . x2)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. x2) x2)))) f73d5..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . x2))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 9761f.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. x2) x2)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . x2)))) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . x2))) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. x2) (λ x3 . x3)))))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 6e880.. 5b8fe..) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. x2) x2)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . x2)))) 0f581..)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . x2)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. x2) x2)))) 0f581..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . x2))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 6e880.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . x2)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. x2) x2)))) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . x2))) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. x2) (λ x3 . x3)))))) x0)) x1))))
Definition e4293.. := λ x0 : ι → ι → ο . and (b9cfa.. x0) (x0 79f98.. b3869..)
Conjecture 22c44.. : ∀ x0 x1 : ι → ι → ο . b9cfa.. x0 ⟶ 68987.. x1 ⟶ d478c.. x0 x1 b3869..
Conjecture 97095.. : ∀ x0 x1 : ι → ι → ο . b9cfa.. x0 ⟶ 68987.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 82bc1.. b3869..
Definition 86d33.. := λ x0 : ι → ι → ο . and (68987.. x0) (x0 79f98.. 82bc1..)
Definition 879d0.. := 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 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 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 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 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 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 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 x0)) (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 x1 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 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 x1 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 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0)))))))))))))))))))))))
Param c8911.. : ι
Definition 3edb3.. := 57d6a.. 3cd3c.. (57d6a.. c8911.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) f73d5..) 0f581..))
Param ae581.. : ι
Definition 81d91.. := bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) f73d5..) 0f581..)) (λ x0 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 5da20.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. x1) x1)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . x1)))) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . x1))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 3cfef.. 5b8fe..) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. x1) x1)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . x1)))) 0f581..)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 5b8fe..) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . x1)))) (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. x1) x1)))) 0f581..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . x1))) (57d6a.. (57d6a.. (57d6a.. 79f98.. f73d5..) 0f581..) x0))) ae581..)
Definition aed70.. := λ x0 : ι → ι → ο . and (e4293.. x0) (x0 879d0.. 3edb3..)
Conjecture 008f2.. : ∀ x0 x1 : ι → ι → ο . e4293.. x0 ⟶ 86d33.. x1 ⟶ d478c.. x0 x1 3edb3..
Conjecture d732b.. : ∀ x0 x1 : ι → ι → ο . e4293.. x0 ⟶ 86d33.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 81d91.. 3edb3..
Definition ca802.. := λ x0 : ι → ι → ο . and (86d33.. x0) (x0 879d0.. 81d91..)
Definition 3ea55.. := 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 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 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 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 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 x1 x1) (prim0 x0 x1))))) (prim1 (λ x0 . x0))))))))))
Definition c7fbc.. := 57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. 65996..) 65996..))
Definition 9ed8f.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 65996..) 0f581..) f73d5..))
Definition 679d8.. := λ x0 : ι → ι → ο . and (aed70.. x0) (x0 3ea55.. c7fbc..)
Conjecture 0aa61.. : ∀ x0 x1 : ι → ι → ο . aed70.. x0 ⟶ ca802.. x1 ⟶ d478c.. x0 x1 c7fbc..
Conjecture 5b876.. : ∀ x0 x1 : ι → ι → ο . aed70.. x0 ⟶ ca802.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 9ed8f.. c7fbc..
Definition 4a327.. := λ x0 : ι → ι → ο . and (ca802.. x0) (x0 3ea55.. 9ed8f..)
Definition c7956.. := 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 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 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 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 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (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 x1 x1) (prim0 x0 x1))))) (prim1 (λ x0 . x0))))))))))
Definition 9f378.. := 57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. 65996..) (57d6a.. (57d6a.. 62f06.. 65996..) 65996..)))
Definition a0e3f.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x1 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. 780a9.. 65996..) x1) 0f581..) x0))
Definition 53569.. := λ x0 : ι → ι → ο . and (679d8.. x0) (x0 c7956.. 9f378..)
Conjecture fbeff.. : ∀ x0 x1 : ι → ι → ο . 679d8.. x0 ⟶ 4a327.. x1 ⟶ d478c.. x0 x1 9f378..
Conjecture bf1d1.. : ∀ x0 x1 : ι → ι → ο . 679d8.. x0 ⟶ 4a327.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. a0e3f.. 9f378..
Definition dc7e8.. := λ x0 : ι → ι → ο . and (4a327.. x0) (x0 c7956.. a0e3f..)
Definition e39f2.. := 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 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 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 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 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (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 x1 x1) (prim0 x0 x1))))) (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 x0)) (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 x1 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 x1))))) (prim1 (λ x0 . x0)))))))))))))))))
Definition 26a87.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 65996..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x0 . 57d6a.. (57d6a.. 7a0ec.. 65996..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) (57d6a.. (57d6a.. c7956.. x0) x1)) f73d5..)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x0) f73d5..))))))
Param 2a8bd.. : ι
Param c85c4.. : ι
Param a809c.. : ι
Definition 33a91.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 74351.. (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x0 . 57d6a.. (57d6a.. 7a0ec.. 65996..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) (57d6a.. (57d6a.. c7956.. x0) x1)) f73d5..)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x0) f73d5..)))))) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x0 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 9761f.. 65996..) x0) 0f581..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x1) f73d5..)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) f73d5..) f73d5..)))) (bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x0) f73d5..)) (λ x1 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. 65996..) x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x2 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x2) f73d5..))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. 65996..) x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x0)))) (57d6a.. (57d6a.. c85c4.. 65996..) x0)) f73d5..) x1)) f73d5..) x1))))) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x0 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 6e880.. 65996..) x0) 0f581..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x1) f73d5..)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) 0f581..) f73d5..)))) (bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) 0f581..) f73d5..)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. a809c.. 65996..) f73d5..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x1 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x1) f73d5..))) (57d6a.. (57d6a.. c85c4.. 65996..) f73d5..)) 0f581..)))))))
Definition 117bd.. := λ x0 : ι → ι → ο . and (53569.. x0) (x0 e39f2.. 26a87..)
Conjecture 105b7.. : ∀ x0 x1 : ι → ι → ο . 53569.. x0 ⟶ dc7e8.. x1 ⟶ d478c.. x0 x1 26a87..
Conjecture 133a7.. : ∀ x0 x1 : ι → ι → ο . 53569.. x0 ⟶ dc7e8.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 33a91.. 26a87..
Definition 55863.. := λ x0 : ι → ι → ο . and (dc7e8.. x0) (x0 e39f2.. 33a91..)
Definition 1031e.. := 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 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 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 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 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (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 x1 x1) (prim0 x0 x1))))) (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 x0)) (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 x1 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))))) (prim1 (λ x0 . x0)))))))))))))))))
Definition 6dc4c.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 65996..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x0 . 57d6a.. (57d6a.. 7a0ec.. 65996..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) (57d6a.. (57d6a.. c7956.. x0) x1)) f73d5..)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x1) f73d5..))))))
Definition d31e4.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x1 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. 74351.. (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) (57d6a.. (57d6a.. c7956.. x2) x1)) f73d5..)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x1) f73d5..)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 9761f.. 65996..) x1) 0f581..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x2) f73d5..)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x1) f73d5..)))) (bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x1) f73d5..)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. 65996..) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x1)))) (57d6a.. (57d6a.. c85c4.. 65996..) x1)) f73d5..))))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 6e880.. 65996..) x1) 0f581..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x2) f73d5..)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x1) f73d5..)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 74351.. (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) 0f581..) f73d5..)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x2) f73d5..)))) (bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) 0f581..) f73d5..)) (λ x2 . 57d6a.. (57d6a.. c85c4.. 65996..) f73d5..))) (bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) 0f581..) f73d5..)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. a809c.. 65996..) f73d5..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x2 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x2) f73d5..))) (57d6a.. (57d6a.. c85c4.. 65996..) f73d5..)) 0f581..)))) x1))) x0))
Definition fdff9.. := λ x0 : ι → ι → ο . and (117bd.. x0) (x0 1031e.. 6dc4c..)
Conjecture 88142.. : ∀ x0 x1 : ι → ι → ο . 117bd.. x0 ⟶ 55863.. x1 ⟶ d478c.. x0 x1 6dc4c..
Conjecture 26049.. : ∀ x0 x1 : ι → ι → ο . 117bd.. x0 ⟶ 55863.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. d31e4.. 6dc4c..
Definition 0a564.. := λ x0 : ι → ι → ο . and (55863.. x0) (x0 1031e.. d31e4..)
Definition 2192a.. := 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 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 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 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 x0)) (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 x1 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 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 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 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 x1 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 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0)))))))))))))))))))
Param 62b32.. : ι
Definition 3cfc6.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 65996..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x0 . 57d6a.. (57d6a.. 62b32.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x0) f73d5..)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x0) 0f581..))))
Param b5f6e.. : ι
Definition 3404c.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 74351.. (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x0 . 57d6a.. (57d6a.. 62b32.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x0) f73d5..)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) x0) 0f581..)))) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) f73d5..) f73d5..)) x0)) (λ x1 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) f73d5..) 0f581..)) x0)) (λ x2 . 57d6a.. x1 (57d6a.. (57d6a.. c85c4.. 65996..) f73d5..)))))) (57d6a.. (57d6a.. (57d6a.. b5f6e.. 65996..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 65996..)) (λ x1 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. 65996..) 0f581..) f73d5..)))) 0f581..)))
Definition 605a7.. := λ x0 : ι → ι → ο . and (fdff9.. x0) (x0 2192a.. 3cfc6..)
Conjecture 3c340.. : ∀ x0 x1 : ι → ι → ο . fdff9.. x0 ⟶ 0a564.. x1 ⟶ d478c.. x0 x1 3cfc6..
Conjecture 2662c.. : ∀ x0 x1 : ι → ι → ο . fdff9.. x0 ⟶ 0a564.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 3404c.. 3cfc6..
Definition 34df7.. := λ x0 : ι → ι → ο . and (0a564.. x0) (x0 2192a.. 3404c..)
Definition 605a7.. := 605a7..
Definition 34df7.. := 34df7..