Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPP6../d5c28..
PUhmU../edd8e..
vout
PrPP6../5dd1c.. 0.00 bars
TMSvi../cfb2d.. ownership of a4145.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMakC../5bd85.. ownership of 98982.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTwh../2d10f.. ownership of 67b67.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFaR../2f881.. ownership of 68192.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK5u../63543.. ownership of 461e0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdAo../c0286.. ownership of 90c83.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR8r../cc417.. ownership of b5a4f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR2V../5bd2d.. ownership of 012ca.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSRM../4e6c6.. ownership of e511b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQmr../a8c3b.. ownership of f2757.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTJs../5a019.. ownership of cdfc5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEgn../fde8d.. ownership of edda2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVgQ../5f15b.. ownership of 44d9a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVPN../3ab59.. ownership of 54840.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUcZ../da6e6.. ownership of 0ae27.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMa4f../a051b.. ownership of 020ff.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLbW../e6896.. ownership of 259f6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJtW../90d32.. ownership of ac2d5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSKa../945af.. ownership of 1c6bf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLPP../c46e5.. ownership of 95eba.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVWz../1d5cb.. ownership of e12a0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM9o../facda.. ownership of a5dfc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdHr../74419.. ownership of b0df2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGL1../3eb2f.. ownership of 1ccf7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFJW../e4646.. ownership of 38cca.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcgC../1f6ea.. ownership of 8ab18.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT4e../2e680.. ownership of fdf51.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTjm../281bf.. ownership of 96798.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PULFy../948ae.. doc published by PrGxv..
Param explicit_Ring_with_id : ι → ι → ι → (ι → ι → ι) → (ι → ι → ι) → ο
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known explicit_Ring_with_id_I : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x3 x5 x6) x0) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x3 x5 (x3 x6 x7) = x3 (x3 x5 x6) x7) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 x5 x6 = x3 x6 x5) ⟶ prim1 x1 x0 ⟶ (∀ x5 . prim1 x5 x0 ⟶ x3 x1 x5 = x5) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 : ο . (∀ x7 . and (prim1 x7 x0) (x3 x5 x7 = x1) ⟶ x6) ⟶ x6) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x4 x5 x6) x0) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x5 (x4 x6 x7) = x4 (x4 x5 x6) x7) ⟶ prim1 x2 x0 ⟶ (x2 = x1 ⟶ ∀ x5 : ο . x5) ⟶ (∀ x5 . prim1 x5 x0 ⟶ x4 x2 x5 = x5) ⟶ (∀ x5 . prim1 x5 x0 ⟶ x4 x5 x2 = x5) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x5 (x3 x6 x7) = x3 (x4 x5 x6) (x4 x5 x7)) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 (x3 x5 x6) x7 = x3 (x4 x5 x7) (x4 x6 x7)) ⟶ explicit_Ring_with_id x0 x1 x2 x3 x4
Known explicit_Ring_with_id_E : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ο . (explicit_Ring_with_id x0 x1 x2 x3 x4 ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ prim1 (x3 x6 x7) x0) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x3 x6 (x3 x7 x8) = x3 (x3 x6 x7) x8) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x3 x6 x7 = x3 x7 x6) ⟶ prim1 x1 x0 ⟶ (∀ x6 . prim1 x6 x0 ⟶ x3 x1 x6 = x6) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 : ο . (∀ x8 . and (prim1 x8 x0) (x3 x6 x8 = x1) ⟶ x7) ⟶ x7) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ prim1 (x4 x6 x7) x0) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 x6 (x4 x7 x8) = x4 (x4 x6 x7) x8) ⟶ prim1 x2 x0 ⟶ (x2 = x1 ⟶ ∀ x6 : ο . x6) ⟶ (∀ x6 . prim1 x6 x0 ⟶ x4 x2 x6 = x6) ⟶ (∀ x6 . prim1 x6 x0 ⟶ x4 x6 x2 = x6) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 x6 (x3 x7 x8) = x3 (x4 x6 x7) (x4 x6 x8)) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 (x3 x6 x7) x8 = x3 (x4 x6 x8) (x4 x7 x8)) ⟶ x5) ⟶ explicit_Ring_with_id x0 x1 x2 x3 x4 ⟶ x5
Param nat_primrec : ι → (ι → ι → ι) → ι → ι
Definition explicit_Ring_with_id_exp_nat := λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 . nat_primrec x2 (λ x6 . x4 x5)
Param f482f.. : ι → ι → ι
Definition fdf51.. := λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 x6 x7 . nat_primrec x1 (λ x8 . x3 (x4 (f482f.. x6 x8) (explicit_Ring_with_id_exp_nat x0 x1 x2 x3 x4 x7 x8))) x5
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem b0df2.. : ∀ x0 x1 x2 . ∀ x3 x4 x5 x6 : ι → ι → ι . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x3 x7 x8 = x5 x7 x8) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 x7 x8 = x6 x7 x8) ⟶ explicit_Ring_with_id x0 x1 x2 x3 x4 ⟶ explicit_Ring_with_id x0 x1 x2 x5 x6 (proof)
Param iff : ο → ο → ο
Known iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem explicit_Ring_with_id_repindep : ∀ x0 x1 x2 . ∀ x3 x4 x5 x6 : ι → ι → ι . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x3 x7 x8 = x5 x7 x8) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 x7 x8 = x6 x7 x8) ⟶ iff (explicit_Ring_with_id x0 x1 x2 x3 x4) (explicit_Ring_with_id x0 x1 x2 x5 x6) (proof)
Param explicit_CRing_with_id : ι → ι → ι → (ι → ι → ι) → (ι → ι → ι) → ο
Known explicit_CRing_with_id_I : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x3 x5 x6) x0) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x3 x5 (x3 x6 x7) = x3 (x3 x5 x6) x7) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 x5 x6 = x3 x6 x5) ⟶ prim1 x1 x0 ⟶ (∀ x5 . prim1 x5 x0 ⟶ x3 x1 x5 = x5) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 : ο . (∀ x7 . and (prim1 x7 x0) (x3 x5 x7 = x1) ⟶ x6) ⟶ x6) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x4 x5 x6) x0) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x5 (x4 x6 x7) = x4 (x4 x5 x6) x7) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x4 x5 x6 = x4 x6 x5) ⟶ prim1 x2 x0 ⟶ (x2 = x1 ⟶ ∀ x5 : ο . x5) ⟶ (∀ x5 . prim1 x5 x0 ⟶ x4 x2 x5 = x5) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x5 (x3 x6 x7) = x3 (x4 x5 x6) (x4 x5 x7)) ⟶ explicit_CRing_with_id x0 x1 x2 x3 x4
Known explicit_CRing_with_id_E : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ο . (explicit_CRing_with_id x0 x1 x2 x3 x4 ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ prim1 (x3 x6 x7) x0) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x3 x6 (x3 x7 x8) = x3 (x3 x6 x7) x8) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x3 x6 x7 = x3 x7 x6) ⟶ prim1 x1 x0 ⟶ (∀ x6 . prim1 x6 x0 ⟶ x3 x1 x6 = x6) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 : ο . (∀ x8 . and (prim1 x8 x0) (x3 x6 x8 = x1) ⟶ x7) ⟶ x7) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ prim1 (x4 x6 x7) x0) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 x6 (x4 x7 x8) = x4 (x4 x6 x7) x8) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x6 x7 = x4 x7 x6) ⟶ prim1 x2 x0 ⟶ (x2 = x1 ⟶ ∀ x6 : ο . x6) ⟶ (∀ x6 . prim1 x6 x0 ⟶ x4 x2 x6 = x6) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 x6 (x3 x7 x8) = x3 (x4 x6 x7) (x4 x6 x8)) ⟶ x5) ⟶ explicit_CRing_with_id x0 x1 x2 x3 x4 ⟶ x5
Theorem 1c6bf.. : ∀ x0 x1 x2 . ∀ x3 x4 x5 x6 : ι → ι → ι . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x3 x7 x8 = x5 x7 x8) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 x7 x8 = x6 x7 x8) ⟶ explicit_CRing_with_id x0 x1 x2 x3 x4 ⟶ explicit_CRing_with_id x0 x1 x2 x5 x6 (proof)
Theorem explicit_CRing_with_id_repindep : ∀ x0 x1 x2 . ∀ x3 x4 x5 x6 : ι → ι → ι . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x3 x7 x8 = x5 x7 x8) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 x7 x8 = x6 x7 x8) ⟶ iff (explicit_CRing_with_id x0 x1 x2 x3 x4) (explicit_CRing_with_id x0 x1 x2 x5 x6) (proof)
Param explicit_Field : ι → ι → ι → (ι → ι → ι) → (ι → ι → ι) → ο
Known explicit_Field_E : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ο . (explicit_Field x0 x1 x2 x3 x4 ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ prim1 (x3 x6 x7) x0) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x3 x6 (x3 x7 x8) = x3 (x3 x6 x7) x8) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x3 x6 x7 = x3 x7 x6) ⟶ prim1 x1 x0 ⟶ (∀ x6 . prim1 x6 x0 ⟶ x3 x1 x6 = x6) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 : ο . (∀ x8 . and (prim1 x8 x0) (x3 x6 x8 = x1) ⟶ x7) ⟶ x7) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ prim1 (x4 x6 x7) x0) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 x6 (x4 x7 x8) = x4 (x4 x6 x7) x8) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x6 x7 = x4 x7 x6) ⟶ prim1 x2 x0 ⟶ (x2 = x1 ⟶ ∀ x6 : ο . x6) ⟶ (∀ x6 . prim1 x6 x0 ⟶ x4 x2 x6 = x6) ⟶ (∀ x6 . prim1 x6 x0 ⟶ (x6 = x1 ⟶ ∀ x7 : ο . x7) ⟶ ∀ x7 : ο . (∀ x8 . and (prim1 x8 x0) (x4 x6 x8 = x2) ⟶ x7) ⟶ x7) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 x6 (x3 x7 x8) = x3 (x4 x6 x7) (x4 x6 x8)) ⟶ x5) ⟶ explicit_Field x0 x1 x2 x3 x4 ⟶ x5
Known explicit_Field_I : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x3 x5 x6) x0) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x3 x5 (x3 x6 x7) = x3 (x3 x5 x6) x7) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 x5 x6 = x3 x6 x5) ⟶ prim1 x1 x0 ⟶ (∀ x5 . prim1 x5 x0 ⟶ x3 x1 x5 = x5) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 : ο . (∀ x7 . and (prim1 x7 x0) (x3 x5 x7 = x1) ⟶ x6) ⟶ x6) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x4 x5 x6) x0) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x5 (x4 x6 x7) = x4 (x4 x5 x6) x7) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x4 x5 x6 = x4 x6 x5) ⟶ prim1 x2 x0 ⟶ (x2 = x1 ⟶ ∀ x5 : ο . x5) ⟶ (∀ x5 . prim1 x5 x0 ⟶ x4 x2 x5 = x5) ⟶ (∀ x5 . prim1 x5 x0 ⟶ (x5 = x1 ⟶ ∀ x6 : ο . x6) ⟶ ∀ x6 : ο . (∀ x7 . and (prim1 x7 x0) (x4 x5 x7 = x2) ⟶ x6) ⟶ x6) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x5 (x3 x6 x7) = x3 (x4 x5 x6) (x4 x5 x7)) ⟶ explicit_Field x0 x1 x2 x3 x4
Theorem 0ae27.. : ∀ x0 x1 x2 . ∀ x3 x4 x5 x6 : ι → ι → ι . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x3 x7 x8 = x5 x7 x8) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 x7 x8 = x6 x7 x8) ⟶ explicit_Field x0 x1 x2 x3 x4 ⟶ explicit_Field x0 x1 x2 x5 x6 (proof)
Theorem explicit_Field_repindep : ∀ x0 x1 x2 . ∀ x3 x4 x5 x6 : ι → ι → ι . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x3 x7 x8 = x5 x7 x8) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 x7 x8 = x6 x7 x8) ⟶ iff (explicit_Field x0 x1 x2 x3 x4) (explicit_Field x0 x1 x2 x5 x6) (proof)
Theorem cdfc5.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ explicit_CRing_with_id x0 x1 x2 x3 x4 (proof)
Param c77b5.. : ι → (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι
Definition 3f0d0.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ prim1 (x4 x5 x6) x2) ⟶ ∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ x1 (c77b5.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Param c3510.. : ι → (ι → (ι → ι → ι) → (ι → ι → ι) → ι → ι → ο) → ο
Known 24f4f.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → ι → ι → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5) ⟶ c3510.. (c77b5.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5
Definition d7e73.. := λ x0 . and (3f0d0.. x0) (c3510.. x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_Ring_with_id x1 x4 x5 x2 x3))
Known prop_ext : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 = x1
Theorem e511b.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 . c3510.. (c77b5.. x0 x1 x2 x3 x4) (λ x6 . λ x7 x8 : ι → ι → ι . λ x9 x10 . explicit_Ring_with_id x6 x9 x10 x7 x8) = explicit_Ring_with_id x0 x3 x4 x1 x2 (proof)
Definition dac20.. := λ x0 . and (3f0d0.. x0) (c3510.. x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_CRing_with_id x1 x4 x5 x2 x3))
Theorem b5a4f.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 . c3510.. (c77b5.. x0 x1 x2 x3 x4) (λ x6 . λ x7 x8 : ι → ι → ι . λ x9 x10 . explicit_CRing_with_id x6 x9 x10 x7 x8) = explicit_CRing_with_id x0 x3 x4 x1 x2 (proof)
Definition 38cca.. := λ x0 . and (3f0d0.. x0) (c3510.. x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_Field x1 x4 x5 x2 x3))
Theorem 461e0.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 . c3510.. (c77b5.. x0 x1 x2 x3 x4) (λ x6 . λ x7 x8 : ι → ι → ι . λ x9 x10 . explicit_Field x6 x9 x10 x7 x8) = explicit_Field x0 x3 x4 x1 x2 (proof)
Known explicit_CRing_with_id_Ring_with_id : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_CRing_with_id x0 x1 x2 x3 x4 ⟶ explicit_Ring_with_id x0 x1 x2 x3 x4
Theorem 67b67.. : ∀ x0 . dac20.. x0 ⟶ d7e73.. x0 (proof)
Theorem a4145.. : ∀ x0 . 38cca.. x0 ⟶ dac20.. x0 (proof)