Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: RealsStruct x0.
Apply set_ext with RealsStruct_Z x0, {x1 ∈ field0 x0|or (or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x1 ∈ RealsStruct_Npos x0) (x1 = field4 x0)) (x1 ∈ RealsStruct_Npos x0)} leaving 2 subgoals.
Let x1 of type ι be given.
Assume H1: x1 ∈ RealsStruct_Z x0.
Apply SepE with field0 x0, λ x2 . or (or (Field_minus (Field_of_RealsStruct x0) x2 ∈ RealsStruct_Npos x0) (x2 = field4 x0)) (x2 ∈ RealsStruct_Npos x0), x1, x1 ∈ {x2 ∈ field0 x0|or (or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x2 ∈ RealsStruct_Npos x0) (x2 = field4 x0)) (x2 ∈ RealsStruct_Npos x0)} leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2: x1 ∈ field0 x0.
Assume H3: or (or (Field_minus (Field_of_RealsStruct x0) x1 ∈ RealsStruct_Npos x0) (x1 = field4 x0)) (x1 ∈ RealsStruct_Npos x0).
Apply SepI with field0 x0, λ x2 . or (or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x2 ∈ RealsStruct_Npos x0) (x2 = field4 x0)) (x2 ∈ RealsStruct_Npos x0), x1 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply H3 with or (or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x1 ∈ RealsStruct_Npos x0) (x1 = field4 x0)) (x1 ∈ RealsStruct_Npos x0) leaving 2 subgoals.
Assume H4: or (Field_minus (Field_of_RealsStruct x0) x1 ∈ RealsStruct_Npos x0) (x1 = field4 x0).
Apply H4 with or (or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x1 ∈ RealsStruct_Npos x0) (x1 = field4 x0)) (x1 ∈ RealsStruct_Npos x0) leaving 2 subgoals.
Assume H5: Field_minus (Field_of_RealsStruct x0) x1 ∈ RealsStruct_Npos x0.
Apply orIL with or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x1 ∈ RealsStruct_Npos x0) (x1 = field4 x0), x1 ∈ RealsStruct_Npos x0.
Apply orIL with explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x1 ∈ RealsStruct_Npos x0, x1 = field4 x0.
Apply RealsStruct_minus_eq2 with x0, x1, λ x2 x3 . x2 ∈ RealsStruct_Npos x0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H5.
Assume H5: x1 = field4 x0.
Apply orIL with or (explicit_Field_minus (field0 x0) (field4 ...) ... ... ... ... ∈ ...) ..., ....
...
...
...
■