Proofgold Proposition

∀ x0 . RealsStruct x0 ⟶ ∀ x1 : ο . (RealsStruct_Npos x0 ⊆ field0 x0 ⟶ explicit_Nats (RealsStruct_Npos x0) (RealsStruct_one x0) (λ x2 . field1b x0 x2 (RealsStruct_one x0)) ⟶ RealsStruct_one x0 ∈ RealsStruct_Npos x0 ⟶ (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ field1b x0 x2 (RealsStruct_one x0) = RealsStruct_one x0 ⟶ ∀ x3 : ο . x3) ⟶ (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ ∀ x3 : ι → ο . x3 (RealsStruct_one x0) ⟶ (∀ x4 . x4 ∈ RealsStruct_Npos x0 ⟶ x3 (field1b x0 x4 (RealsStruct_one x0))) ⟶ x3 x2) ⟶ (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Npos x0 ⟶ explicit_Nats_one_plus (RealsStruct_Npos x0) (RealsStruct_one x0) (λ x5 . field1b x0 x5 (RealsStruct_one x0)) x2 x3 = field1b x0 x2 x3) ⟶ (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Npos x0 ⟶ explicit_Nats_one_mult (RealsStruct_Npos x0) (RealsStruct_one x0) (λ x5 . field1b x0 x5 (RealsStruct_one x0)) x2 x3 = field2b x0 x2 x3) ⟶ (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Npos x0 ⟶ field1b x0 x2 x3 ∈ RealsStruct_Npos x0) ⟶ (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x2 x3 ∈ RealsStruct_Npos x0) ⟶ x1) ⟶ x1

type
prop

theory
HotG

name
RealsStruct_Npos_props

proof
PUSVY..

Megalodon
RealsStruct_Npos_props

proofgold address
TMLHJ..^{RealsStruct_Npos_props}

creator
5804 Pr6Pc../4b25d..

owner
5804 Pr6Pc../4b25d..

term root
ac462..