Proofgold Signed Transaction

vin
PrEvg../b1c91.. PULY8../996b0..

vout

PrEvg../59bb4.. 0.37 bars
TMPJt../564ef.. negprop ownership controlledby PrGxv.. upto 0
TMXim../9856d.. negprop ownership controlledby PrGxv.. upto 0
TMZj1../41e60.. negprop ownership controlledby PrGxv.. upto 0
TMdKV../c0405.. ownership of a63fb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMS1u../37b29.. ownership of 01e02.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMY6v../61a0e.. ownership of 9df63.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJMS../99cd1.. ownership of 5dbf3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSZz../ee6b7.. ownership of 09e09.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP3e../5a53b.. ownership of 2e30d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdXD../40df3.. ownership of b581d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMG41../3ae5c.. ownership of 32641.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKcn../e476e.. ownership of f4e4d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUkG../f9b63.. ownership of 83873.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYkH../4def7.. ownership of 913b8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGZB../45b1d.. ownership of ac56e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWey../eefef.. ownership of b8a80.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTKD../7009c.. ownership of fb66b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSFR../bf7ae.. ownership of 64513.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNE9../22e77.. ownership of bc2f5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFiv../e10de.. ownership of d69a1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXfu../6e00e.. ownership of 51080.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSw5../47582.. ownership of dfeb0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEjT../025f2.. ownership of 8456f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJif../b16be.. ownership of 798c1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSCJ../1855d.. ownership of 2e4c9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdn4../3b6e3.. ownership of 7d6ad.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFW7../fa3c2.. ownership of 2c6d5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHKz../d7c79.. ownership of f0743.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHmX../93a52.. ownership of 7aca6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXyF../d6e83.. ownership of c1535.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdLs../2cfda.. ownership of b4b18.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTSL../b70ed.. ownership of 40b47.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYGh../71e35.. ownership of fb2a3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNcd../cbf5c.. ownership of 02f21.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSfV../f8dbf.. ownership of 08f03.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGfa../f89f4.. ownership of 87e44.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH2M../67e99.. ownership of 2cf7b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaAW../5f4c0.. ownership of 74efc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKXp../c81a4.. ownership of 8b629.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRKU../1a1bd.. ownership of 0a05d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMML3../1010e.. ownership of 98f7d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdce../d3d22.. ownership of 63d4e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPCr../daa6a.. ownership of 07b32.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSJv../89aa6.. ownership of b916f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGt9../0fc94.. ownership of 2d122.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEoc../03b14.. ownership of 61590.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPVq../6fcf9.. ownership of 7c3b1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbzi../72da0.. ownership of 94d41.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMgA../fb7ed.. ownership of 6cb16.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJk6../1dfcd.. ownership of d478c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMc3N../55407.. ownership of acffe.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMG4j../f210b.. ownership of ee912.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNCR../0c1e8.. ownership of 5ca39.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZVF../33c05.. ownership of 6fe8d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHdq../7fd66.. ownership of e2f6d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVws../5550d.. ownership of f6435.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVbX../00c6f.. ownership of 41932.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPRC../414be.. ownership of a603a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGZP../5d8ca.. ownership of d07ba.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSwn../bb0dc.. ownership of 5c39b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTc1../60fce.. ownership of d1fb0.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFYG../5b7c5.. ownership of 13ace.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVYd../6f5f9.. ownership of 46a74.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGDs../fe07f.. ownership of d3ec1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRfJ../db4f0.. ownership of 735be.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR5J../51c0b.. ownership of 93971.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMajH../174e7.. ownership of 993b1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM4N../15716.. ownership of 1ca3e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWss../73121.. ownership of 0e0f1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYyC../bb146.. ownership of 051a7.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPzk../f2e74.. ownership of baa42.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGb3../5e6f3.. ownership of 91fd5.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMc6u../396e2.. ownership of 2059c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVeT../591ed.. ownership of d7cf0.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRyP../68f40.. ownership of e3d1e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPxC../11fcf.. ownership of bcddf.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML5i../0299a.. ownership of 47c65.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLRX../63edd.. ownership of 32d20.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVgx../bda87.. ownership of b5b4c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWQD../cdd27.. ownership of 6915e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZqr../8e9b5.. ownership of b071f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PULLz../e1474.. doc published by PrGxv..

Definition 8e91b.. := λ x0 : ι → ι → ο . λ x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x0 x4 x5 ⟶ x3 x4 x5) ⟶ (∀ x4 x5 x6 . x3 x4 x5 ⟶ x3 x5 x6 ⟶ x3 x4 x6) ⟶ x3 x1 x2
Theorem 94d41.. : ∀ x0 x1 : ι → ι → ο . (∀ x2 x3 . x0 x2 x3 ⟶ x1 x2 x3) ⟶ ∀ x2 x3 . 8e91b.. x0 x2 x3 ⟶ 8e91b.. x1 x2 x3 (proof)
Definition 236c6.. := prim1 (λ x0 . x0)
Definition 6915e.. := prim1 (λ x0 . 236c6..)
Definition 32d20.. := prim1 (λ x0 . prim1 (λ x1 . x0))
Known 148f8.. : ∀ x0 : ι → ι → ι . 236c6.. = prim1 (λ x2 . prim1 (x0 x2)) ⟶ ∀ x1 : ο . x1
Theorem 61590.. : 236c6.. = 6915e.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem b916f.. : 236c6.. = 32d20.. ⟶ ∀ x0 : ο . x0 (proof)
Known b4755.. : ∀ x0 x1 : ι → ι . prim1 x0 = prim1 x1 ⟶ x0 = x1
Theorem 63d4e.. : 6915e.. = 32d20.. ⟶ ∀ x0 : ο . x0 (proof)
Definition 57d6a.. := λ x0 x1 . prim0 236c6.. (prim0 x0 x1)
Definition bcddf.. := λ x0 . λ x1 : ι → ι . prim0 6915e.. (prim0 x0 (prim1 x1))
Definition d7cf0.. := λ x0 . λ x1 : ι → ι . prim0 32d20.. (prim0 x0 (prim1 x1))
Definition 91fd5.. := λ x0 x1 . d7cf0.. x0 (λ x2 . x1)
Definition 051a7.. := λ x0 : ι → ι → ο . λ x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x0 x4 x5 ⟶ x3 x4 x5) ⟶ (∀ x4 . x3 x4 x4) ⟶ (∀ x4 x5 x6 x7 . x3 x4 x5 ⟶ x3 x6 x7 ⟶ x3 (57d6a.. x4 x6) (57d6a.. x5 x7)) ⟶ (∀ x4 x5 . ∀ x6 x7 : ι → ι . x3 x4 x5 ⟶ (∀ x8 . x3 (x6 x8) (x7 x8)) ⟶ x3 (bcddf.. x4 x6) (bcddf.. x5 x7)) ⟶ (∀ x4 x5 . ∀ x6 x7 : ι → ι . x3 x4 x5 ⟶ (∀ x8 . x3 (x6 x8) (x7 x8)) ⟶ x3 (d7cf0.. x4 x6) (d7cf0.. x5 x7)) ⟶ x3 x1 x2
Theorem 0a05d.. : ∀ x0 x1 : ι → ι → ο . (∀ x2 x3 . x0 x2 x3 ⟶ x1 x2 x3) ⟶ ∀ x2 x3 . 051a7.. x0 x2 x3 ⟶ 051a7.. x1 x2 x3 (proof)
Definition 1ca3e.. := λ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . ∀ x4 : ι → ι . ∀ x5 . x2 (bcddf.. x3 x4) (x4 x5)) ⟶ x2 x0 x1
Definition 93971.. := λ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 x4 . x2 (bcddf.. x3 (57d6a.. x4)) x4) ⟶ x2 x0 x1
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition d3ec1.. := λ x0 : ι → ι → ο . 8e91b.. (051a7.. (λ x1 x2 . or (x0 x1 x2) (1ca3e.. x1 x2)))
Definition 13ace.. := λ x0 : ι → ι → ο . 8e91b.. (051a7.. (λ x1 x2 . or (or (x0 x1 x2) (1ca3e.. x1 x2)) (93971.. x1 x2)))
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem 74efc.. : ∀ x0 x1 : ι → ι → ο . (∀ x2 x3 . x0 x2 x3 ⟶ x1 x2 x3) ⟶ ∀ x2 x3 . d3ec1.. x0 x2 x3 ⟶ d3ec1.. x1 x2 x3 (proof)
Definition False := ∀ x0 : ο . x0
Definition 5c39b.. := λ x0 x1 . False
Param and : ο → ο → ο
Definition a603a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 . or (x0 x3 x4) (and (x3 = x1) (x4 = x2))
Theorem 87e44.. : ∀ x0 x1 : ι → ι → ο . ∀ x2 x3 . (∀ x4 x5 . x0 x4 x5 ⟶ x1 x4 x5) ⟶ ∀ x4 x5 . a603a.. x0 x2 x3 x4 x5 ⟶ a603a.. x1 x2 x3 x4 x5 (proof)
Definition f6435.. := λ x0 . or (x0 = 32d20..) (x0 = 6915e..)
Theorem 02f21.. : f6435.. 32d20.. (proof)
Theorem 40b47.. : f6435.. 6915e.. (proof)
Definition 6fe8d.. := λ x0 x1 x2 : ι → ι → ο . λ x3 x4 . ∀ x5 : (ι → ι → ο) → ι → ι → ο . (∀ x6 : ι → ι → ο . ∀ x7 x8 . x0 x7 x8 ⟶ x5 x6 x7 x8) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 . x6 x7 x8 ⟶ x5 x6 x7 x8) ⟶ (∀ x6 : ι → ι → ο . x5 x6 32d20.. 6915e..) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 . ∀ x9 : ι → ι . f6435.. x7 ⟶ x5 x6 x8 32d20.. ⟶ (∀ x10 . x5 (a603a.. x6 x10 x8) (x9 x10) x7) ⟶ x5 x6 (d7cf0.. x8 x9) x7) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 x9 . ∀ x10 : ι → ι . x5 x6 x7 (d7cf0.. x9 x10) ⟶ x5 x6 x8 x9 ⟶ x5 x6 (57d6a.. x7 x8) (x10 x8)) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 . ∀ x9 x10 : ι → ι . f6435.. x7 ⟶ x5 x6 (d7cf0.. x8 x10) x7 ⟶ (∀ x11 . x5 (a603a.. x6 x11 x8) (x9 x11) (x10 x11)) ⟶ x5 x6 (bcddf.. 236c6.. x9) (d7cf0.. x8 x10)) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 . ∀ x9 x10 : ι → ι . f6435.. x7 ⟶ x5 x6 (d7cf0.. x8 x10) x7 ⟶ (∀ x11 . x5 (a603a.. x6 x11 x8) (x9 x11) (x10 x11)) ⟶ x5 x6 (bcddf.. x8 x9) (d7cf0.. x8 x10)) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 x9 x10 x11 . f6435.. x7 ⟶ x5 x6 x8 x9 ⟶ x5 x6 x10 x7 ⟶ d3ec1.. x1 x9 x11 ⟶ d3ec1.. x1 x10 x11 ⟶ x5 x6 x8 x10) ⟶ x5 x2 x3 x4
Theorem c1535.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 . x0 x3 x4 ⟶ 6fe8d.. x0 x1 x2 x3 x4 (proof)
Theorem f0743.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 . x2 x3 x4 ⟶ 6fe8d.. x0 x1 x2 x3 x4 (proof)
Theorem 7d6ad.. : ∀ x0 x1 x2 : ι → ι → ο . 6fe8d.. x0 x1 x2 32d20.. 6915e.. (proof)
Theorem 798c1.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 . ∀ x5 : ι → ι . f6435.. x3 ⟶ 6fe8d.. x0 x1 x2 x4 32d20.. ⟶ (∀ x6 . 6fe8d.. x0 x1 (a603a.. x2 x6 x4) (x5 x6) x3) ⟶ 6fe8d.. x0 x1 x2 (d7cf0.. x4 x5) x3 (proof)
Theorem dfeb0.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 x5 . ∀ x6 : ι → ι . 6fe8d.. x0 x1 x2 x3 (d7cf0.. x5 x6) ⟶ 6fe8d.. x0 x1 x2 x4 x5 ⟶ 6fe8d.. x0 x1 x2 (57d6a.. x3 x4) (x6 x4) (proof)
Theorem d69a1.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 . ∀ x5 x6 : ι → ι . f6435.. x3 ⟶ 6fe8d.. x0 x1 x2 (d7cf0.. x4 x6) x3 ⟶ (∀ x7 . 6fe8d.. x0 x1 (a603a.. x2 x7 x4) (x5 x7) (x6 x7)) ⟶ 6fe8d.. x0 x1 x2 (bcddf.. 236c6.. x5) (d7cf0.. x4 x6) (proof)
Theorem 64513.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 . ∀ x5 x6 : ι → ι . f6435.. x3 ⟶ 6fe8d.. x0 x1 x2 (d7cf0.. x4 x6) x3 ⟶ (∀ x7 . 6fe8d.. x0 x1 (a603a.. x2 x7 x4) (x5 x7) (x6 x7)) ⟶ 6fe8d.. x0 x1 x2 (bcddf.. x4 x5) (d7cf0.. x4 x6) (proof)
Theorem b8a80.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 x5 x6 x7 . f6435.. x3 ⟶ 6fe8d.. x0 x1 x2 x4 x5 ⟶ 6fe8d.. x0 x1 x2 x6 x3 ⟶ d3ec1.. x1 x5 x7 ⟶ d3ec1.. x1 x6 x7 ⟶ 6fe8d.. x0 x1 x2 x4 x6 (proof)
Theorem 913b8.. : ∀ x0 x1 x2 x3 x4 : ι → ι → ο . (∀ x5 x6 . x0 x5 x6 ⟶ x2 x5 x6) ⟶ (∀ x5 x6 . x1 x5 x6 ⟶ x3 x5 x6) ⟶ ∀ x5 x6 . 6fe8d.. x0 x1 x4 x5 x6 ⟶ 6fe8d.. x2 x3 x4 x5 x6 (proof)
Theorem f4e4d.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 . 6fe8d.. x0 x1 x2 x3 x4 ⟶ ∀ x5 : ι → ι → ο . (∀ x6 x7 . x2 x6 x7 ⟶ x5 x6 x7) ⟶ 6fe8d.. x0 x1 x5 x3 x4 (proof)
Theorem b581d.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 x5 . f6435.. x3 ⟶ 6fe8d.. x0 x1 x2 x4 32d20.. ⟶ 6fe8d.. x0 x1 x2 x5 x3 ⟶ 6fe8d.. x0 x1 x2 (91fd5.. x4 x5) x3 (proof)
Theorem 09e09.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 . 6fe8d.. x0 x1 x2 x3 32d20.. ⟶ 6fe8d.. x0 x1 x2 x4 32d20.. ⟶ 6fe8d.. x0 x1 x2 (91fd5.. x3 x4) 32d20.. (proof)
Definition ee912.. := λ x0 : ι → ι → ο . ∀ x1 x2 x3 . x0 x1 x2 ⟶ x0 x1 x3 ⟶ x2 = x3
Definition d478c.. := λ x0 x1 : ι → ι → ο . λ x2 . or (6fe8d.. x0 x1 5c39b.. x2 6915e..) (6fe8d.. x0 x1 5c39b.. x2 32d20..)
Theorem 9df63.. : ∀ x0 x1 : ι → ι → ο . ∀ x2 . 6fe8d.. x0 x1 5c39b.. x2 6915e.. ⟶ d478c.. x0 x1 x2 (proof)
Theorem a63fb.. : ∀ x0 x1 : ι → ι → ο . ∀ x2 . 6fe8d.. x0 x1 5c39b.. x2 32d20.. ⟶ d478c.. x0 x1 x2 (proof)