Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrD1n../e379e..
PUdCX../1b5bf..
vout
PrD1n../34b0c.. 5.12 bars
TMa1f../1de9c.. BOUNTY 1.00 bars controlledby PrGxv.. upto 3000
TMY5W../45aaa.. BOUNTY 1.00 bars controlledby PrGxv.. upto 2500
TMW9v../a539b.. ownership of efdff.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFzC../7dee1.. ownership of 38437.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYyo../8d6ca.. ownership of 17be7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTRz../0b3de.. ownership of 20dca.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVkX../ecbe0.. ownership of 3f6f9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMU7m../abe8f.. ownership of a3e83.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFw6../40a83.. ownership of b4261.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVNF../fc1f2.. ownership of 03463.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZMB../a452b.. ownership of 42fd0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbeE../ca8d4.. ownership of bdebe.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSgo../bcc63.. ownership of aca1a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRuA../a20ec.. ownership of 21d26.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTxD../34a44.. ownership of 84f7f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcBC../9c44a.. ownership of 11ab5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMY8u../83672.. ownership of 8b3a5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNZe../4af86.. ownership of cff58.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTie../29632.. ownership of b316e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMU5K../78392.. ownership of ae1e7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP7q../f853f.. ownership of 16c10.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP7v../8d5b3.. ownership of f4200.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWHp../fbecc.. ownership of 4bdfc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN9s../5295b.. ownership of 1695e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVqh../d3dde.. ownership of 214ce.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd2C../6fe44.. ownership of 761b5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNtk../ce8f0.. ownership of d0180.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNCp../4b20c.. ownership of 76884.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLN3../812cf.. ownership of 092f4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcjk../52f6d.. ownership of d52bc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMS1T../47526.. ownership of 2011d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdAC../74ed8.. ownership of fd472.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNFs../6d71e.. ownership of 547ca.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNS4../c0385.. ownership of 46e4c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSnq../fbc23.. ownership of ca73c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJL1../6209c.. ownership of 43e17.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbmv../29f94.. ownership of c8e20.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcE6../34e96.. ownership of eeeb3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXJx../2e7db.. ownership of b6648.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJpn../4779e.. ownership of 53761.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYUw../18702.. ownership of 3e6f8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUxS../5e913.. ownership of 3cd07.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKD1../5889d.. ownership of 4a83c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN9L../e9bd4.. ownership of 79524.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVDe../8385e.. ownership of 2156c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQzw../91c7a.. ownership of 19d37.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML5y../2338c.. ownership of b4c82.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQF7../32a8d.. ownership of a5b13.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUxa../339e7.. ownership of 98718.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJhv../d535e.. ownership of 5c9f4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXMs../01418.. ownership of e3e6f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVES../87ce2.. ownership of 117be.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK8R../6ab31.. ownership of 21067.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUk9../d2e3f.. ownership of 98ae2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKkN../41dfd.. ownership of 1aee4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHe1../bb36e.. ownership of 72dc8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQt3../5612d.. ownership of 41bc1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMb41../ee5ed.. ownership of 7bb51.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK4y../9ee24.. ownership of 57d3c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMc9n../b5ed5.. ownership of d89e2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVaJ../7bc17.. ownership of fc3cd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLeu../6e11b.. ownership of 5eb4d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMW32../35301.. ownership of fb7af.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZfx../fe5c2.. ownership of fecdd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcXv../b6716.. ownership of 78238.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQRj../7db05.. ownership of 7df08.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEu4../e0930.. ownership of 024d1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSrG../94de9.. ownership of d5f15.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGNx../fc2cf.. ownership of 3a4f6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZjd../2091f.. ownership of f719e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdTt../d8a64.. ownership of 8b44a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPdN../e08fa.. ownership of a5b27.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUSv../f1897.. ownership of f3d9f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSL8../cab56.. ownership of 9ec22.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN5S../1fb94.. ownership of 5c8d7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNGu../eaaca.. ownership of 4c0da.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRU8../94057.. ownership of 88d35.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVW6../370e4.. ownership of 0637d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZma../d4c3e.. ownership of cc192.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbtc../897b0.. ownership of 5b226.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMG6u../f4d1e.. ownership of 3a245.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM7t../7db17.. ownership of f283d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdkf../4ad40.. ownership of 5dc8b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMahF../43814.. ownership of 0d48b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKLT../32b65.. ownership of d7d78.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLYb../97e6a.. ownership of a28dd.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNMk../11a62.. ownership of 858ff.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPyj../1c328.. ownership of f91e4.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNWQ../8598a.. ownership of 6e020.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaVj../42858.. ownership of 6f70a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMa6n../fa5a9.. ownership of cfc98.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFc4../0d4d1.. ownership of ede55.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPeB../124d5.. ownership of c0709.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMck8../1ff08.. ownership of c80fe.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN5q../72597.. ownership of 6c5f4.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRmJ../a3617.. ownership of 9933f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHup../46439.. ownership of 0b8ef.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQUq../79f6b.. ownership of fc359.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd2k../a7c51.. ownership of 07017.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGRX../32068.. ownership of 6c150.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PULLa../a1208.. doc published by PrGxv..
Param 236c6.. : ι
Definition 07017.. := λ x0 . x0 = 236c6..
Definition 0b8ef.. := prim0 (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0)))
Definition 6c5f4.. := prim0 (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim1 (λ x0 . x0)))
Known 93754.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ x1 = x3
Theorem 3a245.. : ∀ x0 x1 . 0b8ef.. x0 = 0b8ef.. x1 ⟶ x0 = x1 (proof)
Theorem cc192.. : ∀ x0 x1 . 6c5f4.. x0 = 6c5f4.. x1 ⟶ x0 = x1 (proof)
Known 50787.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ x0 = x2
Definition False := ∀ x0 : ο . x0
Known 0286c.. : ∀ x0 x1 . prim0 x0 x1 = 236c6.. ⟶ False
Known db6fe.. : ∀ x0 x1 : ι → ι . ∀ x2 . prim1 x0 = prim1 x1 ⟶ x0 x2 = x1 x2
Theorem 88d35.. : ∀ x0 x1 . 0b8ef.. x0 = 6c5f4.. x1 ⟶ ∀ x2 : ο . x2 (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition c0709.. := λ x0 x1 : ι → ο . λ x2 . or (∀ x3 : ο . (∀ x4 . and (x0 x4) (x2 = 0b8ef.. x4) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (x1 x4) (x2 = 6c5f4.. x4) ⟶ x3) ⟶ x3)
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 5c8d7.. : ∀ x0 x1 : ι → ο . ∀ x2 . x0 x2 ⟶ c0709.. x0 x1 (0b8ef.. x2) (proof)
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem f3d9f.. : ∀ x0 x1 : ι → ο . ∀ x2 . x1 x2 ⟶ c0709.. x0 x1 (6c5f4.. x2) (proof)
Theorem 8b44a.. : ∀ x0 x1 : ι → ο . ∀ x2 . c0709.. x0 x1 x2 ⟶ ∀ x3 : ι → ο . (∀ x4 . x0 x4 ⟶ x3 (0b8ef.. x4)) ⟶ (∀ x4 . x1 x4 ⟶ x3 (6c5f4.. x4)) ⟶ x3 x2 (proof)
Definition cfc98.. := λ x0 x1 . prim0 (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x3 x3) (prim0 x3 x3))))) (prim1 (λ x2 . x2))) (prim0 x0 x1)
Known 128d8.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ ∀ x4 : ο . (x0 = x2 ⟶ x1 = x3 ⟶ x4) ⟶ x4
Theorem 3a4f6.. : ∀ x0 x1 x2 x3 . cfc98.. x0 x1 = cfc98.. x2 x3 ⟶ and (x0 = x2) (x1 = x3) (proof)
Definition 6e020.. := λ x0 x1 : ι → ο . λ x2 . ∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 . and (and (x0 x4) (x1 x6)) (x2 = cfc98.. x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem 024d1.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 . x0 x2 ⟶ x1 x3 ⟶ 6e020.. x0 x1 (cfc98.. x2 x3) (proof)
Theorem 78238.. : ∀ x0 x1 : ι → ο . ∀ x2 . 6e020.. x0 x1 x2 ⟶ ∀ x3 : ι → ο . (∀ x4 x5 . x0 x4 ⟶ x1 x5 ⟶ x3 (cfc98.. x4 x5)) ⟶ x3 x2 (proof)
Param 5e331.. : ι
Param a3eb9.. : ι → ι → ι
Param bf68c.. : ι → ι → ι
Definition 858ff.. := λ x0 . λ x1 : ι → ο . ∀ x2 : ι → (ι → ο) → ο . x2 5e331.. 07017.. ⟶ (∀ x3 x4 . ∀ x5 x6 : ι → ο . x2 x3 x5 ⟶ x2 x4 x6 ⟶ x2 (a3eb9.. x3 x4) (c0709.. x5 x6)) ⟶ (∀ x3 x4 . ∀ x5 x6 : ι → ο . x2 x3 x5 ⟶ x2 x4 x6 ⟶ x2 (bf68c.. x3 x4) (6e020.. x5 x6)) ⟶ x2 x0 x1
Theorem fb7af.. : 858ff.. 5e331.. 07017.. (proof)
Theorem fc3cd.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . 858ff.. x0 x2 ⟶ 858ff.. x1 x3 ⟶ 858ff.. (a3eb9.. x0 x1) (c0709.. x2 x3) (proof)
Theorem 57d3c.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . 858ff.. x0 x2 ⟶ 858ff.. x1 x3 ⟶ 858ff.. (bf68c.. x0 x1) (6e020.. x2 x3) (proof)
Param 74e69.. : ι → ο
Known facf7.. : ∀ x0 : ι → ο . x0 5e331.. ⟶ (∀ x1 x2 . 74e69.. x1 ⟶ x0 x1 ⟶ 74e69.. x2 ⟶ x0 x2 ⟶ x0 (a3eb9.. x1 x2)) ⟶ (∀ x1 x2 . 74e69.. x1 ⟶ x0 x1 ⟶ 74e69.. x2 ⟶ x0 x2 ⟶ x0 (bf68c.. x1 x2)) ⟶ ∀ x1 . 74e69.. x1 ⟶ x0 x1
Theorem 41bc1.. : ∀ x0 . 74e69.. x0 ⟶ ∀ x1 : ο . (∀ x2 : ι → ο . 858ff.. x0 x2 ⟶ x1) ⟶ x1 (proof)
Theorem 1aee4.. : ∀ x0 : ι → (ι → ο) → ο . x0 5e331.. 07017.. ⟶ (∀ x1 x2 . ∀ x3 x4 : ι → ο . 858ff.. x1 x3 ⟶ x0 x1 x3 ⟶ 858ff.. x2 x4 ⟶ x0 x2 x4 ⟶ x0 (a3eb9.. x1 x2) (c0709.. x3 x4)) ⟶ (∀ x1 x2 . ∀ x3 x4 : ι → ο . 858ff.. x1 x3 ⟶ x0 x1 x3 ⟶ 858ff.. x2 x4 ⟶ x0 x2 x4 ⟶ x0 (bf68c.. x1 x2) (6e020.. x3 x4)) ⟶ ∀ x1 . ∀ x2 : ι → ο . 858ff.. x1 x2 ⟶ x0 x1 x2 (proof)
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known 9ec26.. : ∀ x0 x1 . 5e331.. = a3eb9.. x0 x1 ⟶ ∀ x2 : ο . x2
Known 59f91.. : ∀ x0 x1 . 5e331.. = bf68c.. x0 x1 ⟶ ∀ x2 : ο . x2
Known 5e750.. : ∀ x0 x1 x2 x3 . a3eb9.. x0 x1 = a3eb9.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known a8e2e.. : ∀ x0 x1 x2 x3 . a3eb9.. x0 x1 = bf68c.. x2 x3 ⟶ ∀ x4 : ο . x4
Known 2f86f.. : ∀ x0 x1 x2 x3 . bf68c.. x0 x1 = bf68c.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Theorem 21067.. : ∀ x0 . ∀ x1 : ι → ο . 858ff.. x0 x1 ⟶ ∀ x2 . ∀ x3 : ι → ο . 858ff.. x2 x3 ⟶ x0 = x2 ⟶ x1 = x3 (proof)
Theorem e3e6f.. : ∀ x0 . ∀ x1 x2 : ι → ο . 858ff.. x0 x1 ⟶ 858ff.. x0 x2 ⟶ x1 = x2 (proof)
Theorem 98718.. : ∀ x0 . ∀ x1 : ι → ο . 858ff.. x0 x1 ⟶ ∀ x2 : ο . (x0 = 5e331.. ⟶ x1 = 07017.. ⟶ x2) ⟶ (∀ x3 x4 . ∀ x5 x6 : ι → ο . 858ff.. x3 x5 ⟶ 858ff.. x4 x6 ⟶ x0 = a3eb9.. x3 x4 ⟶ x1 = c0709.. x5 x6 ⟶ x2) ⟶ (∀ x3 x4 . ∀ x5 x6 : ι → ο . 858ff.. x3 x5 ⟶ 858ff.. x4 x6 ⟶ x0 = bf68c.. x3 x4 ⟶ x1 = 6e020.. x5 x6 ⟶ x2) ⟶ x2 (proof)
Theorem b4c82.. : ∀ x0 x1 . ∀ x2 : ι → ο . 858ff.. (a3eb9.. x0 x1) x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ο . (∀ x5 : ο . (∀ x6 : ι → ο . and (and (858ff.. x0 x4) (858ff.. x1 x6)) (x2 = c0709.. x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Theorem 2156c.. : ∀ x0 x1 . ∀ x2 : ι → ο . 858ff.. (bf68c.. x0 x1) x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ο . (∀ x5 : ο . (∀ x6 : ι → ο . and (and (858ff.. x0 x4) (858ff.. x1 x6)) (x2 = 6e020.. x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Param c4def.. : ι
Param 6b90c.. : ι → ι → ι
Param c9248.. : ι
Param a6e19.. : ι → ι
Param 2fe34.. : ι → ι
Param e05e6.. : ι → ο
Param 3e00e.. : ι → ι → ι
Param f9341.. : ι → ι → ι
Param 1fa6d.. : ι → ι
Param 3a365.. : ι → ι
Definition d7d78.. := λ x0 x1 x2 . ∀ x3 : ι → ι → ι → ο . (∀ x4 . x3 c4def.. x4 x4) ⟶ (∀ x4 x5 x6 x7 x8 . x3 x4 x6 x7 ⟶ x3 x5 x7 x8 ⟶ x3 (6b90c.. x4 x5) x6 x8) ⟶ (∀ x4 . x3 c9248.. x4 236c6..) ⟶ (∀ x4 x5 x6 . x3 x4 x5 x6 ⟶ x3 (a6e19.. x4) x5 (0b8ef.. x6)) ⟶ (∀ x4 x5 x6 . x3 x4 x5 x6 ⟶ x3 (2fe34.. x4) x5 (6c5f4.. x6)) ⟶ (∀ x4 x5 x6 x7 x8 . e05e6.. x5 ⟶ x3 x4 (cfc98.. x6 x7) x8 ⟶ x3 (3e00e.. x4 x5) (cfc98.. (0b8ef.. x6) x7) x8) ⟶ (∀ x4 x5 x6 x7 x8 . e05e6.. x4 ⟶ x3 x5 (cfc98.. x6 x7) x8 ⟶ x3 (3e00e.. x4 x5) (cfc98.. (6c5f4.. x6) x7) x8) ⟶ (∀ x4 x5 x6 x7 x8 . x3 x4 x6 x7 ⟶ x3 x5 x6 x8 ⟶ x3 (f9341.. x4 x5) x6 (cfc98.. x7 x8)) ⟶ (∀ x4 x5 x6 x7 . x3 x4 x5 x7 ⟶ x3 (1fa6d.. x4) (cfc98.. x5 x6) x7) ⟶ (∀ x4 x5 x6 x7 . x3 x4 x6 x7 ⟶ x3 (3a365.. x4) (cfc98.. x5 x6) x7) ⟶ x3 x0 x1 x2
Theorem 4a83c.. : ∀ x0 . d7d78.. c4def.. x0 x0 (proof)
Theorem 3e6f8.. : ∀ x0 x1 x2 x3 x4 . d7d78.. x0 x2 x3 ⟶ d7d78.. x1 x3 x4 ⟶ d7d78.. (6b90c.. x0 x1) x2 x4 (proof)
Theorem b6648.. : ∀ x0 . d7d78.. c9248.. x0 236c6.. (proof)
Theorem c8e20.. : ∀ x0 x1 x2 . d7d78.. x0 x1 x2 ⟶ d7d78.. (a6e19.. x0) x1 (0b8ef.. x2) (proof)
Theorem ca73c.. : ∀ x0 x1 x2 . d7d78.. x0 x1 x2 ⟶ d7d78.. (2fe34.. x0) x1 (6c5f4.. x2) (proof)
Theorem 547ca.. : ∀ x0 x1 x2 x3 x4 . e05e6.. x1 ⟶ d7d78.. x0 (cfc98.. x2 x3) x4 ⟶ d7d78.. (3e00e.. x0 x1) (cfc98.. (0b8ef.. x2) x3) x4 (proof)
Theorem 2011d.. : ∀ x0 x1 x2 x3 x4 . e05e6.. x0 ⟶ d7d78.. x1 (cfc98.. x2 x3) x4 ⟶ d7d78.. (3e00e.. x0 x1) (cfc98.. (6c5f4.. x2) x3) x4 (proof)
Theorem 092f4.. : ∀ x0 x1 x2 x3 x4 . d7d78.. x0 x2 x3 ⟶ d7d78.. x1 x2 x4 ⟶ d7d78.. (f9341.. x0 x1) x2 (cfc98.. x3 x4) (proof)
Theorem d0180.. : ∀ x0 x1 x2 x3 . d7d78.. x0 x1 x3 ⟶ d7d78.. (1fa6d.. x0) (cfc98.. x1 x2) x3 (proof)
Theorem 214ce.. : ∀ x0 x1 x2 x3 . d7d78.. x0 x2 x3 ⟶ d7d78.. (3a365.. x0) (cfc98.. x1 x2) x3 (proof)
Theorem 4bdfc.. : ∀ x0 : ι → ι → ι → ο . (∀ x1 . d7d78.. c4def.. x1 x1 ⟶ x0 c4def.. x1 x1) ⟶ (∀ x1 x2 x3 x4 x5 . d7d78.. x1 x3 x4 ⟶ x0 x1 x3 x4 ⟶ d7d78.. x2 x4 x5 ⟶ x0 x2 x4 x5 ⟶ x0 (6b90c.. x1 x2) x3 x5) ⟶ (∀ x1 . d7d78.. c9248.. x1 236c6.. ⟶ x0 c9248.. x1 236c6..) ⟶ (∀ x1 x2 x3 . d7d78.. x1 x2 x3 ⟶ x0 x1 x2 x3 ⟶ x0 (a6e19.. x1) x2 (0b8ef.. x3)) ⟶ (∀ x1 x2 x3 . d7d78.. x1 x2 x3 ⟶ x0 x1 x2 x3 ⟶ x0 (2fe34.. x1) x2 (6c5f4.. x3)) ⟶ (∀ x1 x2 x3 x4 x5 . e05e6.. x2 ⟶ d7d78.. x1 (cfc98.. x3 x4) x5 ⟶ x0 x1 (cfc98.. x3 x4) x5 ⟶ x0 (3e00e.. x1 x2) (cfc98.. (0b8ef.. x3) x4) x5) ⟶ (∀ x1 x2 x3 x4 x5 . e05e6.. x1 ⟶ d7d78.. x2 (cfc98.. x3 x4) x5 ⟶ x0 x2 (cfc98.. x3 x4) x5 ⟶ x0 (3e00e.. x1 x2) (cfc98.. (6c5f4.. x3) x4) x5) ⟶ (∀ x1 x2 x3 x4 x5 . d7d78.. x1 x3 x4 ⟶ x0 x1 x3 x4 ⟶ d7d78.. x2 x3 x5 ⟶ x0 x2 x3 x5 ⟶ x0 (f9341.. x1 x2) x3 (cfc98.. x4 x5)) ⟶ (∀ x1 x2 x3 x4 . d7d78.. x1 x2 x4 ⟶ x0 x1 x2 x4 ⟶ x0 (1fa6d.. x1) (cfc98.. x2 x3) x4) ⟶ (∀ x1 x2 x3 x4 . d7d78.. x1 x3 x4 ⟶ x0 x1 x3 x4 ⟶ x0 (3a365.. x1) (cfc98.. x2 x3) x4) ⟶ ∀ x1 x2 x3 . d7d78.. x1 x2 x3 ⟶ x0 x1 x2 x3 (proof)
Theorem 16c10.. : ∀ x0 x1 x2 . d7d78.. x0 x1 x2 ⟶ ∀ x3 : ο . (x0 = c4def.. ⟶ x1 = x2 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 x8 . d7d78.. x4 x6 x7 ⟶ d7d78.. x5 x7 x8 ⟶ x0 = 6b90c.. x4 x5 ⟶ x1 = x6 ⟶ x2 = x8 ⟶ x3) ⟶ (x0 = c9248.. ⟶ x2 = 236c6.. ⟶ x3) ⟶ (∀ x4 x5 x6 . d7d78.. x4 x5 x6 ⟶ x0 = a6e19.. x4 ⟶ x1 = x5 ⟶ x2 = 0b8ef.. x6 ⟶ x3) ⟶ (∀ x4 x5 x6 . d7d78.. x4 x5 x6 ⟶ x0 = 2fe34.. x4 ⟶ x1 = x5 ⟶ x2 = 6c5f4.. x6 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 x8 . e05e6.. x5 ⟶ d7d78.. x4 (cfc98.. x6 x7) x8 ⟶ x0 = 3e00e.. x4 x5 ⟶ x1 = cfc98.. (0b8ef.. x6) x7 ⟶ x2 = x8 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 x8 . e05e6.. x4 ⟶ d7d78.. x5 (cfc98.. x6 x7) x8 ⟶ x0 = 3e00e.. x4 x5 ⟶ x1 = cfc98.. (6c5f4.. x6) x7 ⟶ x2 = x8 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 x8 . d7d78.. x4 x6 x7 ⟶ d7d78.. x5 x6 x8 ⟶ x0 = f9341.. x4 x5 ⟶ x1 = x6 ⟶ x2 = cfc98.. x7 x8 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 . d7d78.. x4 x5 x7 ⟶ x0 = 1fa6d.. x4 ⟶ x1 = cfc98.. x5 x6 ⟶ x2 = x7 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 . d7d78.. x4 x6 x7 ⟶ x0 = 3a365.. x4 ⟶ x1 = cfc98.. x5 x6 ⟶ x2 = x7 ⟶ x3) ⟶ x3 (proof)
Known a3634.. : ∀ x0 x1 . c4def.. = 6b90c.. x0 x1 ⟶ ∀ x2 : ο . x2
Known 5e60e.. : c4def.. = c9248.. ⟶ ∀ x0 : ο . x0
Known 924dd.. : ∀ x0 . c4def.. = a6e19.. x0 ⟶ ∀ x1 : ο . x1
Known 0cc7e.. : ∀ x0 . c4def.. = 2fe34.. x0 ⟶ ∀ x1 : ο . x1
Known 91964.. : ∀ x0 x1 . c4def.. = 3e00e.. x0 x1 ⟶ ∀ x2 : ο . x2
Known a14cf.. : ∀ x0 x1 . c4def.. = f9341.. x0 x1 ⟶ ∀ x2 : ο . x2
Known b8b08.. : ∀ x0 . c4def.. = 1fa6d.. x0 ⟶ ∀ x1 : ο . x1
Known f9749.. : ∀ x0 . c4def.. = 3a365.. x0 ⟶ ∀ x1 : ο . x1
Theorem b316e.. : ∀ x0 x1 . d7d78.. c4def.. x0 x1 ⟶ x0 = x1 (proof)
Known ffc37.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = 6b90c.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known dc5ae.. : ∀ x0 x1 . 6b90c.. x0 x1 = c9248.. ⟶ ∀ x2 : ο . x2
Known a9278.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = a6e19.. x2 ⟶ ∀ x3 : ο . x3
Known dabcf.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = 2fe34.. x2 ⟶ ∀ x3 : ο . x3
Known 07fb9.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = 3e00e.. x2 x3 ⟶ ∀ x4 : ο . x4
Known 72b8e.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = f9341.. x2 x3 ⟶ ∀ x4 : ο . x4
Known 0a32f.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = 1fa6d.. x2 ⟶ ∀ x3 : ο . x3
Known ff84b.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = 3a365.. x2 ⟶ ∀ x3 : ο . x3
Theorem 8b3a5.. : ∀ x0 x1 x2 x3 . d7d78.. (6b90c.. x0 x1) x2 x3 ⟶ ∀ x4 : ο . (∀ x5 . and (d7d78.. x0 x2 x5) (d7d78.. x1 x5 x3) ⟶ x4) ⟶ x4 (proof)
Known 84bad.. : ∀ x0 . c9248.. = a6e19.. x0 ⟶ ∀ x1 : ο . x1
Known 1832c.. : ∀ x0 . c9248.. = 2fe34.. x0 ⟶ ∀ x1 : ο . x1
Known 77b59.. : ∀ x0 x1 . c9248.. = 3e00e.. x0 x1 ⟶ ∀ x2 : ο . x2
Known b728e.. : ∀ x0 x1 . c9248.. = f9341.. x0 x1 ⟶ ∀ x2 : ο . x2
Known 0482c.. : ∀ x0 . c9248.. = 1fa6d.. x0 ⟶ ∀ x1 : ο . x1
Known 36b24.. : ∀ x0 . c9248.. = 3a365.. x0 ⟶ ∀ x1 : ο . x1
Theorem 84f7f.. : ∀ x0 x1 . d7d78.. c9248.. x0 x1 ⟶ x1 = 236c6.. (proof)
Known 84af1.. : ∀ x0 x1 . a6e19.. x0 = a6e19.. x1 ⟶ x0 = x1
Known 7241c.. : ∀ x0 x1 . a6e19.. x0 = 2fe34.. x1 ⟶ ∀ x2 : ο . x2
Known 62a09.. : ∀ x0 x1 x2 . a6e19.. x0 = 3e00e.. x1 x2 ⟶ ∀ x3 : ο . x3
Known cec81.. : ∀ x0 x1 x2 . a6e19.. x0 = f9341.. x1 x2 ⟶ ∀ x3 : ο . x3
Known 4bdb9.. : ∀ x0 x1 . a6e19.. x0 = 1fa6d.. x1 ⟶ ∀ x2 : ο . x2
Known 62476.. : ∀ x0 x1 . a6e19.. x0 = 3a365.. x1 ⟶ ∀ x2 : ο . x2
Theorem aca1a.. : ∀ x0 x1 x2 . d7d78.. (a6e19.. x0) x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . and (d7d78.. x0 x1 x4) (x2 = 0b8ef.. x4) ⟶ x3) ⟶ x3 (proof)
Known 2eb6f.. : ∀ x0 x1 . 2fe34.. x0 = 2fe34.. x1 ⟶ x0 = x1
Known a0ec1.. : ∀ x0 x1 x2 . 2fe34.. x0 = 3e00e.. x1 x2 ⟶ ∀ x3 : ο . x3
Known becdb.. : ∀ x0 x1 x2 . 2fe34.. x0 = f9341.. x1 x2 ⟶ ∀ x3 : ο . x3
Known a5def.. : ∀ x0 x1 . 2fe34.. x0 = 1fa6d.. x1 ⟶ ∀ x2 : ο . x2
Known cdd8a.. : ∀ x0 x1 . 2fe34.. x0 = 3a365.. x1 ⟶ ∀ x2 : ο . x2
Theorem 42fd0.. : ∀ x0 x1 x2 . d7d78.. (2fe34.. x0) x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . and (d7d78.. x0 x1 x4) (x2 = 6c5f4.. x4) ⟶ x3) ⟶ x3 (proof)
Known 42e43.. : ∀ x0 x1 x2 x3 . 3e00e.. x0 x1 = 3e00e.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known a1a1b.. : ∀ x0 x1 x2 x3 . 3e00e.. x0 x1 = f9341.. x2 x3 ⟶ ∀ x4 : ο . x4
Known 54459.. : ∀ x0 x1 x2 . 3e00e.. x0 x1 = 1fa6d.. x2 ⟶ ∀ x3 : ο . x3
Known fb77a.. : ∀ x0 x1 x2 . 3e00e.. x0 x1 = 3a365.. x2 ⟶ ∀ x3 : ο . x3
Theorem b4261.. : ∀ x0 x1 x2 x3 . d7d78.. (3e00e.. x0 x1) x2 x3 ⟶ or (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . and (x2 = cfc98.. (0b8ef.. x5) x7) (d7d78.. x0 (cfc98.. x5 x7) x3) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . and (x2 = cfc98.. (6c5f4.. x5) x7) (d7d78.. x1 (cfc98.. x5 x7) x3) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) (proof)
Known 063ac.. : ∀ x0 x1 x2 x3 . f9341.. x0 x1 = f9341.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known 38968.. : ∀ x0 x1 x2 . f9341.. x0 x1 = 1fa6d.. x2 ⟶ ∀ x3 : ο . x3
Known 6774e.. : ∀ x0 x1 x2 . f9341.. x0 x1 = 3a365.. x2 ⟶ ∀ x3 : ο . x3
Theorem 3f6f9.. : ∀ x0 x1 x2 x3 . d7d78.. (f9341.. x0 x1) x2 x3 ⟶ ∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . and (and (d7d78.. x0 x2 x5) (d7d78.. x1 x2 x7)) (x3 = cfc98.. x5 x7) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4 (proof)
Known a1c68.. : ∀ x0 x1 . 1fa6d.. x0 = 1fa6d.. x1 ⟶ x0 = x1
Known 9f429.. : ∀ x0 x1 . 1fa6d.. x0 = 3a365.. x1 ⟶ ∀ x2 : ο . x2
Theorem 17be7.. : ∀ x0 x1 x2 . d7d78.. (1fa6d.. x0) x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 . and (x1 = cfc98.. x4 x6) (d7d78.. x0 x4 x2) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Known f684d.. : ∀ x0 x1 . 3a365.. x0 = 3a365.. x1 ⟶ x0 = x1
Theorem efdff.. : ∀ x0 x1 x2 . d7d78.. (3a365.. x0) x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 . and (x1 = cfc98.. x4 x6) (d7d78.. x0 x6 x2) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Param 762f0.. : ι → ι → ι → ο
Conjecture 085db.. : ∀ x0 x1 x2 . 762f0.. x0 x1 x2 ⟶ ∀ x3 x4 : ι → ο . 858ff.. x1 x3 ⟶ 858ff.. x2 x4 ⟶ ∀ x5 x6 . x3 x5 ⟶ d7d78.. x0 x5 x6 ⟶ x4 x6
Definition 5dc8b.. := λ x0 x1 . and (∀ x2 . x0 = 0b8ef.. x2 ⟶ x1 = 6c5f4.. x2) (∀ x2 . x0 = 6c5f4.. x2 ⟶ x1 = 0b8ef.. x2)
Conjecture 181f2.. : ∀ x0 . 74e69.. x0 ⟶ ∀ x1 : ο . (∀ x2 . and (762f0.. x2 (a3eb9.. x0 x0) (a3eb9.. x0 x0)) (∀ x3 : ι → ο . 858ff.. x0 x3 ⟶ ∀ x4 x5 . c0709.. x3 x3 x4 ⟶ 5dc8b.. x4 x5 ⟶ d7d78.. x2 x4 x5) ⟶ x1) ⟶ x1