Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: RealsStruct x0.
Claim L1: ...
...
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Apply explicit_Field_E with RealsStruct_Q x0, field4 x0, RealsStruct_one x0, field1b x0, field2b x0, and (struct_b_b_e_e (pack_b_b_e_e (RealsStruct_Q x0) (field1b x0) (field2b x0) (field4 x0) (RealsStruct_one x0))) (unpack_b_b_e_e_o (pack_b_b_e_e (RealsStruct_Q x0) (field1b x0) (field2b x0) (field4 x0) (RealsStruct_one x0)) (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_Field x1 x4 x5 x2 x3)) leaving 2 subgoals.
Assume H6: explicit_Field (RealsStruct_Q x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0).
Assume H7: ∀ x1 . x1 ∈ RealsStruct_Q x0 ⟶ ∀ x2 . x2 ∈ RealsStruct_Q x0 ⟶ field1b x0 x1 x2 ∈ RealsStruct_Q x0.
Assume H8: ∀ x1 . x1 ∈ RealsStruct_Q x0 ⟶ ∀ x2 . x2 ∈ RealsStruct_Q x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Q x0 ⟶ field1b x0 x1 (field1b x0 x2 x3) = field1b x0 (field1b x0 x1 x2) x3.
Assume H9: ∀ x1 . x1 ∈ RealsStruct_Q x0 ⟶ ∀ x2 . x2 ∈ RealsStruct_Q x0 ⟶ field1b x0 x1 x2 = field1b x0 x2 x1.
Assume H10: field4 x0 ∈ RealsStruct_Q x0.
Assume H11: ∀ x1 . x1 ∈ RealsStruct_Q x0 ⟶ field1b x0 (field4 x0) x1 = x1.
Assume H12: ∀ x1 . x1 ∈ RealsStruct_Q x0 ⟶ ∃ x2 . and (x2 ∈ RealsStruct_Q x0) (field1b x0 x1 x2 = field4 x0).
Assume H13: ∀ x1 . x1 ∈ RealsStruct_Q x0 ⟶ ∀ x2 . x2 ∈ RealsStruct_Q x0 ⟶ field2b x0 x1 x2 ∈ RealsStruct_Q x0.
Assume H14: ∀ x1 . x1 ∈ RealsStruct_Q x0 ⟶ ∀ x2 . x2 ∈ RealsStruct_Q x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Q x0 ⟶ field2b x0 x1 (field2b x0 x2 x3) = field2b x0 (field2b x0 x1 x2) x3.
Assume H15: ∀ x1 . x1 ∈ RealsStruct_Q x0 ⟶ ∀ x2 . x2 ∈ RealsStruct_Q x0 ⟶ field2b x0 x1 x2 = field2b x0 x2 x1.
Assume H16: RealsStruct_one x0 ∈ RealsStruct_Q x0.
Assume H17: RealsStruct_one x0 = field4 x0 ⟶ ∀ x1 : ο . x1.
Assume H18: ∀ x1 . x1 ∈ RealsStruct_Q x0 ⟶ field2b x0 (RealsStruct_one x0) x1 = x1.
Assume H19: ∀ x1 . ... ⟶ ... ⟶ ∃ x2 . and (x2 ∈ RealsStruct_Q x0) (field2b x0 x1 x2 = RealsStruct_one x0).
...
...
■