Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrEvg../64a28..
PUSw2../e918d..
vout
PrEvg../1d6f8.. 0.35 bars
TMQ9R../61735.. ownership of 39ffe.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQfG../88893.. ownership of 73e6e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcMB../5cc0f.. ownership of 244aa.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ1B../0d447.. ownership of 93bfb.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJVC../9e13b.. ownership of 11543.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQkF../0d2fd.. ownership of 062e0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZxz../c039a.. ownership of 00b46.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMatb../f0e0f.. ownership of cdaf8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPJ9../565bd.. ownership of 00c71.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWL2../9a56c.. ownership of a8ce4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXcq../9522f.. ownership of a604f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRwN../4296a.. ownership of 242c4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXL5../51aae.. ownership of b2995.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEnu../0203c.. ownership of 50570.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHaS../d59d3.. ownership of b9ba9.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaVt../92541.. ownership of f6109.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKab../12e6b.. ownership of 6e624.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUxU../67230.. ownership of b25e0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMW3N../0d7d1.. ownership of 36978.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG87../3de28.. ownership of fd87c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcXP../faec9.. ownership of ffd30.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZed../1790c.. ownership of 60089.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJv2../25014.. ownership of 31a35.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVjU../4b21d.. ownership of bb4d6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaFJ../70dca.. ownership of 49b5c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZ8M../1f4f4.. ownership of 81d50.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMR43../d3a9c.. ownership of 8f3a7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVpS../2644c.. ownership of e2b8a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYZW../d5ebd.. ownership of 62b32.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT3m../7e79d.. ownership of 6eb03.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbwh../66775.. ownership of b3fef.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdsw../159c2.. ownership of 81fe2.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbnY../4265f.. ownership of ed300.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMLf../3a6a2.. ownership of 0ec21.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ7v../b2e3f.. ownership of 80bb2.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHeS../ddb45.. ownership of af3d4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHY5../08a75.. ownership of 2f6f1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGEY../1caeb.. ownership of 52829.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPj5../0a3d6.. ownership of 0ae4d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSxt../b8def.. ownership of 02a50.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNg5../32211.. ownership of 31c5d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFsW../57911.. ownership of 158eb.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPFj../092ab.. ownership of ff75b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRBu../9adab.. ownership of 11d4a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZga../3c9d5.. ownership of fb4c3.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJkA../3abc8.. ownership of 9464e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdrS../e14e6.. ownership of c8911.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSX7../3fada.. ownership of 2bd1f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTMb../d41af.. ownership of be8f5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF4P../f03c6.. ownership of f65bb.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLHb../90bb4.. ownership of 1efc7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKXe../607c4.. ownership of 0e243.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdqT../74593.. ownership of 3569a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYLE../6fbc2.. ownership of 76d7f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaR7../1ef4d.. ownership of a9a29.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJWd../2cd3d.. ownership of 1d01c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK8z../83012.. ownership of 6c8dd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNhy../e6785.. ownership of e36a0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcmu../676f0.. ownership of f0a4f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGXf../f35b2.. ownership of 11756.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGXo../8a6dd.. ownership of 43ba7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLgE../7d558.. ownership of ed683.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKtM../7588f.. ownership of b72ce.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXbV../715df.. ownership of a1850.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJ98../ae9e9.. ownership of ae581.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXaR../9719b.. ownership of b4d07.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVnY../22d29.. ownership of 0af41.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMV97../e012a.. ownership of 1c739.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRZh../38b8f.. ownership of eb3d5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPw2../7b3e3.. ownership of 29796.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNN7../e5b00.. ownership of 9f288.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWNZ../f3f6b.. ownership of b323e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHs1../14f0d.. ownership of 81a9b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMM1p../411d9.. ownership of 8c8ad.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMStN../66b3d.. ownership of 46c0e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKfR../2c55e.. ownership of 1db82.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcsn../b6e09.. ownership of db882.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXqf../a7008.. ownership of 6d048.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUWJJ../5cbbb.. doc published by PrGxv..
Param and : ο → ο → ο
Param 5d0c6.. : (ι → ι → ο) → ο
Param True : ο
Definition db882.. := λ x0 : ι → ι → ο . and (5d0c6.. x0) True
Param 29aed.. : (ι → ι → ο) → ο
Definition 46c0e.. := λ x0 : ι → ι → ο . and (29aed.. x0) True
Definition 81a9b.. := 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 x0 x1))))) (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 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))))) (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 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.. : ι
Param 5b8fe.. : ι
Definition b72ce.. := 57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)
Param 7a0ec.. : ι
Param bcddf.. : ι → (ι → ι) → ι
Param f3baa.. : ι
Definition 9f288.. := 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. f3baa.. x0) x0))
Definition eb3d5.. := λ x0 : ι → ι → ο . and (db882.. x0) (x0 81a9b.. b72ce..)
Param d478c.. : (ι → ι → ο) → (ι → ι → ο) → ι → ο
Conjecture 97d81.. : ∀ x0 x1 : ι → ι → ο . db882.. x0 ⟶ 46c0e.. x1 ⟶ d478c.. x0 x1 b72ce..
Param 6fe8d.. : (ι → ι → ο) → (ι → ι → ο) → (ι → ι → ο) → ι → ι → ο
Param 5c39b.. : ι → ι → ο
Conjecture 24deb.. : ∀ x0 x1 : ι → ι → ο . db882.. x0 ⟶ 46c0e.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 9f288.. b72ce..
Definition 0af41.. := λ x0 : ι → ι → ο . and (46c0e.. x0) (x0 81a9b.. 9f288..)
Definition ae581.. := 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 x0 x1))))) (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 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))))) (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 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 b72ce.. := 57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)
Definition 43ba7.. := 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . x0))
Definition f0a4f.. := λ x0 : ι → ι → ο . and (eb3d5.. x0) (x0 ae581.. b72ce..)
Conjecture f59f8.. : ∀ x0 x1 : ι → ι → ο . eb3d5.. x0 ⟶ 0af41.. x1 ⟶ d478c.. x0 x1 b72ce..
Conjecture 7bc07.. : ∀ x0 x1 : ι → ι → ο . eb3d5.. x0 ⟶ 0af41.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 43ba7.. b72ce..
Definition 6c8dd.. := λ x0 : ι → ι → ο . and (0af41.. x0) (x0 ae581.. 43ba7..)
Definition a9a29.. := 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 x0 x1))))) (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 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))))) (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 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 x1 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 62f06.. : ι
Definition 8f3a7.. := 57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. 5b8fe..) (57d6a.. (57d6a.. 62f06.. 5b8fe..) 5b8fe..)))
Definition 3569a.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (57d6a.. (57d6a.. f3baa.. x0)))
Definition 1efc7.. := λ x0 : ι → ι → ο . and (f0a4f.. x0) (x0 a9a29.. 8f3a7..)
Conjecture 042d9.. : ∀ x0 x1 : ι → ι → ο . f0a4f.. x0 ⟶ 6c8dd.. x1 ⟶ d478c.. x0 x1 8f3a7..
Conjecture 233d8.. : ∀ x0 x1 : ι → ι → ο . f0a4f.. x0 ⟶ 6c8dd.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 3569a.. 8f3a7..
Definition be8f5.. := λ x0 : ι → ι → ο . and (6c8dd.. x0) (x0 a9a29.. 3569a..)
Definition c8911.. := 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 x0 x1))))) (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 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))))) (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 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))))) (prim1 (λ x0 . x0))))))))))))))))
Definition fb4c3.. := 57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. 5b8fe..) 5b8fe..))
Definition ff75b.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. f3baa.. x0) ae581..)
Definition 31c5d.. := λ x0 : ι → ι → ο . and (1efc7.. x0) (x0 c8911.. fb4c3..)
Conjecture ec382.. : ∀ x0 x1 : ι → ι → ο . 1efc7.. x0 ⟶ be8f5.. x1 ⟶ d478c.. x0 x1 fb4c3..
Conjecture 3fed5.. : ∀ x0 x1 : ι → ι → ο . 1efc7.. x0 ⟶ be8f5.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. ff75b.. fb4c3..
Definition 0ae4d.. := λ x0 : ι → ι → ο . and (be8f5.. x0) (x0 c8911.. ff75b..)
Definition 2f6f1.. := 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 x0 x1))))) (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 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))))) (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 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))))) (prim1 (λ x0 . x0))))))))))))))))
Definition 8f3a7.. := 57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. 5b8fe..) (57d6a.. (57d6a.. 62f06.. 5b8fe..) 5b8fe..)))
Definition 80bb2.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. f3baa.. x0) (57d6a.. (57d6a.. f3baa.. x1) x2))) x2))))
Definition ed300.. := λ x0 : ι → ι → ο . and (31c5d.. x0) (x0 2f6f1.. 8f3a7..)
Conjecture caf82.. : ∀ x0 x1 : ι → ι → ο . 31c5d.. x0 ⟶ 0ae4d.. x1 ⟶ d478c.. x0 x1 8f3a7..
Conjecture e4488.. : ∀ x0 x1 : ι → ι → ο . 31c5d.. x0 ⟶ 0ae4d.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 80bb2.. 8f3a7..
Definition b3fef.. := λ x0 : ι → ι → ο . and (0ae4d.. x0) (x0 2f6f1.. 80bb2..)
Definition 62b32.. := 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 x0 x1))))) (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 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))))) (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 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))))) (prim1 (λ x0 . x0)))))))))))))))
Definition 8f3a7.. := 57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. 5b8fe..) (57d6a.. (57d6a.. 62f06.. 5b8fe..) 5b8fe..)))
Definition 49b5c.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. f3baa.. x0) x2)) (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. f3baa.. x1) x2)) x2)))))
Definition 31a35.. := λ x0 : ι → ι → ο . and (ed300.. x0) (x0 62b32.. 8f3a7..)
Conjecture 3f3b3.. : ∀ x0 x1 : ι → ι → ο . ed300.. x0 ⟶ b3fef.. x1 ⟶ d478c.. x0 x1 8f3a7..
Conjecture f34bd.. : ∀ x0 x1 : ι → ι → ο . ed300.. x0 ⟶ b3fef.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 49b5c.. 8f3a7..
Definition ffd30.. := λ x0 : ι → ι → ο . and (b3fef.. x0) (x0 62b32.. 49b5c..)
Definition 36978.. := 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 x0 x1))))) (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 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))))) (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 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))))) (prim1 (λ x0 . x0)))))))))))))))
Param 27862.. : ι
Param 1f2c4.. : ι
Definition 6e624.. := 57d6a.. 67ee8.. (57d6a.. 27862.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)) 5b8fe..))))
Definition b9ba9.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x1 x2)) x2))))))))
Definition b2995.. := λ x0 : ι → ι → ο . and (31a35.. x0) (x0 36978.. 6e624..)
Conjecture 599ee.. : ∀ x0 x1 : ι → ι → ο . 31a35.. x0 ⟶ ffd30.. x1 ⟶ d478c.. x0 x1 6e624..
Conjecture e531a.. : ∀ x0 x1 : ι → ι → ο . 31a35.. x0 ⟶ ffd30.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. b9ba9.. 6e624..
Definition a604f.. := λ x0 : ι → ι → ο . and (ffd30.. x0) (x0 36978.. b9ba9..)
Definition 00c71.. := 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 x0 x1))))) (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 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))))) (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 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim1 (λ x0 . x0))))))))))))))
Param 3cd3c.. : ι
Definition 00b46.. := 57d6a.. 3cd3c.. 81a9b..
Definition 11543.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 3cd3c.. x0) (λ x1 . x1))
Definition 244aa.. := λ x0 : ι → ι → ο . and (b2995.. x0) (x0 00c71.. 00b46..)
Conjecture 65921.. : ∀ x0 x1 : ι → ι → ο . b2995.. x0 ⟶ a604f.. x1 ⟶ d478c.. x0 x1 00b46..
Conjecture 9421d.. : ∀ x0 x1 : ι → ι → ο . b2995.. x0 ⟶ a604f.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 11543.. 00b46..
Definition 39ffe.. := λ x0 : ι → ι → ο . and (a604f.. x0) (x0 00c71.. 11543..)
Definition 244aa.. := 244aa..
Definition 39ffe.. := 39ffe..