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 . x1field0 x0field2b x0 (field4 x0) x1 = x1 leaving 2 subgoals.
Assume H1: explicit_CRing_with_id (field0 x0) (field3 x0) (field4 x0) (field1b x0) (field2b x0).
Assume H2: ∀ x1 . x1field0 x0∀ x2 . x2field0 x0field1b x0 x1 x2field0 x0.
Assume H3: ∀ x1 . x1field0 x0∀ x2 . x2field0 x0∀ x3 . x3field0 x0field1b x0 x1 (field1b x0 x2 x3) = field1b x0 (field1b x0 x1 x2) x3.
Assume H4: ∀ x1 . x1field0 x0∀ x2 . x2field0 x0field1b x0 x1 x2 = field1b x0 x2 x1.
Assume H5: field3 x0field0 x0.
Assume H6: ∀ x1 . x1field0 x0field1b x0 (field3 x0) x1 = x1.
Assume H7: ∀ x1 . x1field0 x0∃ x2 . and (x2field0 x0) (field1b x0 x1 x2 = field3 x0).
Assume H8: ∀ x1 . x1field0 x0∀ x2 . x2field0 x0field2b x0 x1 x2field0 x0.
Assume H9: ∀ x1 . x1field0 x0∀ x2 . x2field0 x0∀ x3 . x3field0 x0field2b x0 x1 (field2b x0 x2 x3) = field2b x0 (field2b x0 x1 x2) x3.
Assume H10: ∀ x1 . x1field0 x0∀ x2 . x2field0 x0field2b x0 x1 x2 = field2b x0 x2 x1.
Assume H11: field4 x0field0 x0.
Assume H12: field4 x0 = field3 x0∀ x1 : ο . x1.
Assume H13: ∀ x1 . x1field0 x0field2b x0 (field4 x0) x1 = x1.
Assume H14: ∀ x1 . x1field0 x0∀ x2 . x2field0 x0∀ x3 . x3field0 x0field2b x0 x1 (field1b x0 x2 x3) = field1b x0 (field2b x0 x1 x2) (field2b x0 x1 x3).
The subproof is completed by applying H13.
...