Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrJGW../c150f..
PUdmi../6247a..
vout
PrJGW../32edc.. 1.99 bars
TMHZF../e190c.. ownership of 548f8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc7V../f84aa.. ownership of e1dfd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNkK../27bc3.. ownership of 98f68.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaHG../54995.. ownership of df009.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPH7../a2d06.. ownership of f1cac.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGmr../08ad5.. ownership of f9cb3.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEg2../d37f2.. ownership of 09d0b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZsV../fca38.. ownership of 3097b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN9h../891f4.. ownership of 447f5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFXG../828ea.. ownership of 5b7fb.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYg3../1f5df.. ownership of 5b618.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKse../3d1a7.. ownership of 170ae.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMU98../bf33f.. ownership of 7412a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRgb../1ea88.. ownership of 27579.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa1h../3538e.. ownership of a08a7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNDA../12e88.. ownership of 650aa.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHFL../0e2f5.. ownership of e7395.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN5U../0e7a8.. ownership of b51a5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVAm../c10dc.. ownership of 43b81.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLaK../4af68.. ownership of 0fea5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFhY../1408d.. ownership of 8484b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQY1../a3c77.. ownership of 693d1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJkC../2adb3.. ownership of c75ec.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFP5../cb045.. ownership of 38c21.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGcs../d635f.. ownership of 950bd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXcF../a5333.. ownership of 7f366.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSiW../fdefb.. ownership of 1798d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSaT../40330.. ownership of 67542.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXcB../5d33d.. ownership of aa823.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa9H../703ea.. ownership of 4da61.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaE7../10861.. ownership of 6afe7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKFS../ccb33.. ownership of e0a27.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMd9A../352cc.. ownership of 0dcda.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQLe../7ca54.. ownership of 217a4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJNp../86d4a.. ownership of 3e999.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJnf../4c136.. ownership of 77329.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSPS../74a0b.. ownership of ff764.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEyS../401f7.. ownership of 151c0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJ4n../c8706.. ownership of c842a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKQW../9b0a2.. ownership of 52617.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZ1D../096d3.. ownership of c09b1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMR3o../d9407.. ownership of 11a7e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFqq../91cca.. ownership of 9c283.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZ15../8bd12.. ownership of e0ce2.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLiR../8777a.. ownership of 5ca0f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLgK../90ee0.. ownership of 39663.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcoJ../45a08.. ownership of f4e87.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMrt../ecef9.. ownership of 4456e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUfB../db6f2.. ownership of a1610.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPYZ../bcdc3.. ownership of 51f7f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcKx../e2238.. ownership of 18e36.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdCy../7e9b3.. ownership of 51272.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLai../82bc2.. ownership of 96f1c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSL8../b1fcd.. ownership of c72f4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb3r../a9c92.. ownership of bcf0f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJcL../33bc2.. ownership of 6cd8a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKXK../109f4.. ownership of dfe2d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMV51../81ff1.. ownership of 96d01.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUQM9../00513.. doc published by PrGxv..
Definition dfe2d.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 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 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))))) (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 57d6a.. : ι → ι → ι
Param 3cd3c.. : ι
Param 7a0ec.. : ι
Param 5b8fe.. : ι
Param bcddf.. : ι → (ι → ι) → ι
Param 67ee8.. : ι
Param 25ca3.. : ι
Param f3baa.. : ι
Param 2f6f1.. : ι
Definition bcf0f.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (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))) (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. 2f6f1.. x0) x1)) x2))))))))
Definition 96f1c.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. f3baa.. x0) (57d6a.. (57d6a.. f3baa.. x1) x2))) (λ x3 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. 2f6f1.. x0) x1)) (λ x4 . 57d6a.. (57d6a.. x4 x2) x3)))))
Param and : ο → ο → ο
Param aac29.. : (ι → ι → ο) → ο
Definition 18e36.. := λ x0 : ι → ι → ο . and (aac29.. x0) (x0 dfe2d.. bcf0f..)
Param 505b1.. : (ι → ι → ο) → ο
Param d478c.. : (ι → ι → ο) → (ι → ι → ο) → ι → ο
Conjecture fe7ba.. : ∀ x0 x1 : ι → ι → ο . aac29.. x0 ⟶ 505b1.. x1 ⟶ d478c.. x0 x1 bcf0f..
Param 6fe8d.. : (ι → ι → ο) → (ι → ι → ο) → (ι → ι → ο) → ι → ι → ο
Param 5c39b.. : ι → ι → ο
Conjecture a2bbc.. : ∀ x0 x1 : ι → ι → ο . aac29.. x0 ⟶ 505b1.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 96f1c.. bcf0f..
Definition a1610.. := λ x0 : ι → ι → ο . and (505b1.. x0) (x0 dfe2d.. 96f1c..)
Definition f4e87.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 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 x1)) (prim0 (prim0 x0 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x1) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim1 (λ x0 . x0))))))))))))
Definition 5ca0f.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. 2f6f1.. x0) x1)) x0)))))
Definition 9c283.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. 2f6f1.. x0) x1)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. dfe2d.. x0) x1) x0) (bcddf.. (57d6a.. 3cd3c.. x0) (λ x2 . bcddf.. (57d6a.. 3cd3c.. x1) (λ x3 . x2)))))))
Definition c09b1.. := λ x0 : ι → ι → ο . and (18e36.. x0) (x0 f4e87.. 5ca0f..)
Conjecture 879c3.. : ∀ x0 x1 : ι → ι → ο . 18e36.. x0 ⟶ a1610.. x1 ⟶ d478c.. x0 x1 5ca0f..
Conjecture e348c.. : ∀ x0 x1 : ι → ι → ο . 18e36.. x0 ⟶ a1610.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 9c283.. 5ca0f..
Definition c842a.. := λ x0 : ι → ι → ο . and (a1610.. x0) (x0 f4e87.. 9c283..)
Definition ff764.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 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 x1)) (prim0 (prim0 x0 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x1) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim1 (λ x0 . x0))))))))))))
Definition 3e999.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. 2f6f1.. x0) x1)) x1)))))
Definition 0dcda.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. 2f6f1.. x0) x1)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. dfe2d.. x0) x1) x1) (bcddf.. (57d6a.. 3cd3c.. x0) (λ x2 . bcddf.. (57d6a.. 3cd3c.. x1) (λ x3 . x3)))))))
Definition 6afe7.. := λ x0 : ι → ι → ο . and (c09b1.. x0) (x0 ff764.. 3e999..)
Conjecture f28ac.. : ∀ x0 x1 : ι → ι → ο . c09b1.. x0 ⟶ c842a.. x1 ⟶ d478c.. x0 x1 3e999..
Conjecture 78997.. : ∀ x0 x1 : ι → ι → ο . c09b1.. x0 ⟶ c842a.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 0dcda.. 3e999..
Definition aa823.. := λ x0 : ι → ι → ο . and (c842a.. x0) (x0 ff764.. 0dcda..)
Definition 1798d.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 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 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))))) (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 62b32.. : ι
Definition 950bd.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (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)) (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. 62b32.. x0) x1)) x2)))))))))
Definition c75ec.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. f3baa.. x0) x2)) (λ x3 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. f3baa.. x1) x2)) (λ x4 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. 62b32.. x0) x1)) (λ x5 . 57d6a.. (57d6a.. (57d6a.. x5 x2) x3) x4))))))
Definition 8484b.. := λ x0 : ι → ι → ο . and (6afe7.. x0) (x0 1798d.. 950bd..)
Conjecture 57c7a.. : ∀ x0 x1 : ι → ι → ο . 6afe7.. x0 ⟶ aa823.. x1 ⟶ d478c.. x0 x1 950bd..
Conjecture cbf41.. : ∀ x0 x1 : ι → ι → ο . 6afe7.. x0 ⟶ aa823.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. c75ec.. 950bd..
Definition 43b81.. := λ x0 : ι → ι → ο . and (aa823.. x0) (x0 1798d.. c75ec..)
Definition e7395.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 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 x1)) (prim0 (prim0 x0 x1) (prim0 x1 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 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0))))))))))))))))
Param 62f06.. : ι
Definition fb4c3.. := 57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. 5b8fe..) 5b8fe..))
Param c8911.. : ι
Definition a08a7.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. 62b32.. x0) (57d6a.. c8911.. x0))
Definition 7412a.. := λ x0 : ι → ι → ο . and (8484b.. x0) (x0 e7395.. fb4c3..)
Conjecture 104a2.. : ∀ x0 x1 : ι → ι → ο . 8484b.. x0 ⟶ 43b81.. x1 ⟶ d478c.. x0 x1 fb4c3..
Conjecture 77591.. : ∀ x0 x1 : ι → ι → ο . 8484b.. x0 ⟶ 43b81.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. a08a7.. fb4c3..
Definition 5b618.. := λ x0 : ι → ι → ο . and (43b81.. x0) (x0 e7395.. a08a7..)
Definition 447f5.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 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 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x0 x1) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 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 cb931.. : ι
Param 1f2c4.. : ι
Param 36978.. : ι
Definition 09d0b.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x1 x3)) x2)))) (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. 36978.. x0) x1)) x2))))))))
Definition f1cac.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x1 x3)) x2)))) (λ x3 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. 36978.. x0) x1)) (λ x4 . 57d6a.. (57d6a.. x4 x2) x3)))))
Definition 98f68.. := λ x0 : ι → ι → ο . and (7412a.. x0) (x0 447f5.. 09d0b..)
Conjecture 019fe.. : ∀ x0 x1 : ι → ι → ο . 7412a.. x0 ⟶ 5b618.. x1 ⟶ d478c.. x0 x1 09d0b..
Conjecture b45fa.. : ∀ x0 x1 : ι → ι → ο . 7412a.. x0 ⟶ 5b618.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. f1cac.. 09d0b..
Definition 548f8.. := λ x0 : ι → ι → ο . and (5b618.. x0) (x0 447f5.. f1cac..)
Definition 98f68.. := 98f68..
Definition 548f8.. := 548f8..