Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: RealsStruct x0.
Apply andI with struct_b_b_e_e (pack_b_b_e_e (field0 x0) (field1b x0) (field2b x0) (field4 x0) (RealsStruct_one x0)), unpack_b_b_e_e_o (pack_b_b_e_e (field0 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.
Apply pack_struct_b_b_e_e_I with field0 x0, field1b x0, field2b x0, field4 x0, RealsStruct_one x0 leaving 4 subgoals.
Apply RealsStruct_plus_clos with x0.
The subproof is completed by applying H0.
Apply RealsStruct_mult_clos with x0.
The subproof is completed by applying H0.
Apply RealsStruct_zero_In with x0.
The subproof is completed by applying H0.
Apply RealsStruct_one_In with x0.
The subproof is completed by applying H0.
Apply unpack_b_b_e_e_o_eq with λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_Field x1 x4 x5 x2 x3, field0 x0, field1b x0, field2b x0, field4 x0, RealsStruct_one x0, λ x1 x2 : ο . x2 leaving 2 subgoals.
Let x1 of type ι → ι → ι be given.
Assume H1: ∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field1b x0 x2 x3 = x1 x2 x3.
Let x2 of type ι → ι → ι be given.
Assume H2: ∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ field2b x0 x3 x4 = x2 x3 x4.
Apply prop_ext with explicit_Field (field0 x0) (field4 x0) (RealsStruct_one x0) x1 x2, explicit_Field (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0).
Apply iff_sym with explicit_Field (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0), explicit_Field (field0 x0) (field4 x0) (RealsStruct_one x0) x1 x2.
Apply explicit_Field_repindep with field0 x0, field4 x0, RealsStruct_one x0, field1b x0, field2b x0, x1, x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply explicit_Field_of_RealsStruct with x0.
The subproof is completed by applying H0.
■