Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Let x2 of type ι → ι → ι be given.
Assume H0: ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4.
Assume H1: explicit_Group x0 x1.
Claim L2: ...
...
Apply H1 with ∀ x3 . prim1 x3 x0 ⟶ explicit_Group_inverse x0 x1 x3 = explicit_Group_inverse x0 x2 x3.
Assume H3: and (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x1 x3 x4) x0) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x1 x3 (x1 x4 x5) = x1 (x1 x3 x4) x5).
Assume H4: ∃ x3 . and (prim1 x3 x0) (and (∀ x4 . prim1 x4 x0 ⟶ and (x1 x3 x4 = x4) (x1 x4 x3 = x4)) (∀ x4 . prim1 x4 x0 ⟶ ∃ x5 . and (prim1 x5 x0) (and (x1 x4 x5 = x3) (x1 x5 x4 = x3)))).
Apply H3 with ∀ x3 . prim1 x3 x0 ⟶ explicit_Group_inverse x0 x1 x3 = explicit_Group_inverse x0 x2 x3.
Assume H5: ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x1 x3 x4) x0.
Assume H6: ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x1 x3 (x1 x4 x5) = x1 (x1 x3 x4) x5.
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Let x3 of type ι be given.
Assume H10: prim1 x3 x0.
Claim L11: ...
...
Claim L12: ...
...
Claim L13: ...
...
Claim L14: ...
...
Apply L9 with explicit_Group_inverse x0 x2 x3, λ x4 x5 . explicit_Group_inverse x0 x1 x3 = x4 leaving 2 subgoals.
The subproof is completed by applying L13.
Apply H0 with explicit_Group_identity x0 x2, explicit_Group_inverse x0 x2 x3, λ x4 x5 . explicit_Group_inverse x0 x1 x3 = x4 leaving 3 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying L13.
Apply explicit_Group_identity_repindep with x0, x1, x2, λ x4 x5 . explicit_Group_inverse x0 x1 x3 = x1 x4 (explicit_Group_inverse x0 x2 x3) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply L12 with λ x4 x5 . explicit_Group_inverse x0 x1 x3 = x1 x4 (explicit_Group_inverse x0 x2 x3).
Apply H6 with explicit_Group_inverse x0 x1 x3, x3, explicit_Group_inverse x0 x2 x3, λ x4 x5 . explicit_Group_inverse x0 x1 x3 = x4 leaving 4 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying H10.
The subproof is completed by applying L13.
Apply H0 with x3, explicit_Group_inverse x0 x2 x3, λ x4 x5 . explicit_Group_inverse x0 x1 x3 = x1 (explicit_Group_inverse x0 x1 x3) x5 leaving 3 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying L13.
Apply L14 with λ x4 x5 . explicit_Group_inverse x0 x1 x3 = x1 ... ....
...
■