Proofgold Proposition

∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 : ο . ((∀ x6 . x6 ∈ x0 ⟶ explicit_Field_minus x0 x1 x2 x3 x4 x6 ∈ x0) ⟶ explicit_Field_minus x0 x1 x2 x3 x4 x1 = x1 ⟶ (∀ x6 . x6 ∈ x0 ⟶ explicit_Field_minus x0 x1 x2 x3 x4 (explicit_Field_minus x0 x1 x2 x3 x4 x6) = x6) ⟶ (∀ x6 . x6 ∈ x0 ⟶ x3 (explicit_Field_minus x0 x1 x2 x3 x4 x6) x6 = x1) ⟶ (∀ x6 . x6 ∈ x0 ⟶ x3 x6 (explicit_Field_minus x0 x1 x2 x3 x4 x6) = x1) ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ x4 (x3 x6 x7) x8 = x3 (x4 x6 x8) (x4 x7 x8)) ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ explicit_Field_minus x0 x1 x2 x3 x4 (x3 x6 x7) = x3 (explicit_Field_minus x0 x1 x2 x3 x4 x6) (explicit_Field_minus x0 x1 x2 x3 x4 x7)) ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x4 (explicit_Field_minus x0 x1 x2 x3 x4 x6) x7 = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x6 x7)) ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x4 x6 (explicit_Field_minus x0 x1 x2 x3 x4 x7) = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x6 x7)) ⟶ (∀ x6 . x6 ∈ x0 ⟶ x4 x1 x6 = x1) ⟶ (∀ x6 . x6 ∈ x0 ⟶ x4 x6 x1 = x1) ⟶ explicit_Field_minus x0 x1 x2 x3 x4 x2 ∈ x0 ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ x4 x6 (x4 x7 x8) ∈ x0) ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ x3 (x3 x6 x7) (x3 x8 x9) = x3 (x3 x6 x9) (x3 x7 x8)) ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ x3 (x3 x6 x7) (x3 x8 x9) = x3 (x3 x6 x8) (x3 x7 x9)) ⟶ x5) ⟶ x5

type
prop

theory
HotG

name
-

proof
PUhdh..

Megalodon
-

proofgold address
TMNoK..

creator
4958 Pr6Pc../52a88..

owner
4958 Pr6Pc../52a88..

term root
93bbb..