Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: CRing_with_id x0.
Apply explicit_CRing_with_id_E with field0 x0, field3 x0, field4 x0, field1b x0, field2b x0, ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field2b x0 x1 (field1b x0 x2 x3) = field1b x0 (field2b x0 x1 x2) (field2b x0 x1 x3) leaving 2 subgoals.
Assume H1: explicit_CRing_with_id (field0 x0) (field3 x0) (field4 x0) (field1b x0) (field2b x0).
Assume H2: ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ field1b x0 x1 x2 ∈ field0 x0.
Assume H3: ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field1b x0 x1 (field1b x0 x2 x3) = field1b x0 (field1b x0 x1 x2) x3.
Assume H4: ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ field1b x0 x1 x2 = field1b x0 x2 x1.
Assume H5: field3 x0 ∈ field0 x0.
Assume H6: ∀ x1 . x1 ∈ field0 x0 ⟶ field1b x0 (field3 x0) x1 = x1.
Assume H7: ∀ x1 . x1 ∈ field0 x0 ⟶ ∃ x2 . and (x2 ∈ field0 x0) (field1b x0 x1 x2 = field3 x0).
Assume H8: ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ field2b x0 x1 x2 ∈ field0 x0.
Assume H9: ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field2b x0 x1 (field2b x0 x2 x3) = field2b x0 (field2b x0 x1 x2) x3.
Assume H10: ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ field2b x0 x1 x2 = field2b x0 x2 x1.
Assume H11: field4 x0 ∈ field0 x0.
Assume H12: field4 x0 = field3 x0 ⟶ ∀ x1 : ο . x1.
Assume H13: ∀ x1 . x1 ∈ field0 x0 ⟶ field2b x0 (field4 x0) x1 = x1.
Assume H14: ∀ x1 . ... ⟶ ∀ x2 . ... ⟶ ∀ x3 . ... ⟶ field2b x0 x1 (field1b x0 x2 x3) = field1b x0 (field2b x0 x1 x2) ....
...
...
■