Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: Subq x1 x0.
Claim L1: ...
...
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ∀ x2 . prim1 x2 (1216a.. (b5c9f.. x0 x0) (λ x3 . and (bij x0 x0 (λ x4 . f482f.. x3 x4)) (∀ x4 . prim1 x4 x1f482f.. x3 x4 = x4)))prim1 (explicit_Group_inverse (1216a.. (b5c9f.. x0 x0) (λ x3 . bij x0 x0 (λ x4 . f482f.. x3 x4))) (λ x3 x4 . 0fc90.. x0 (λ x5 . f482f.. x4 (f482f.. x3 x5))) x2) (1216a.. (b5c9f.. x0 x0) (λ x3 . and (bij x0 x0 (λ x4 . f482f.. x3 x4)) (∀ x4 . prim1 x4 x1f482f.. x3 x4 = x4)))
Let x2 of type ι be given.
Assume H5: prim1 x2 ....
...
Claim L6: ∀ x2 . prim1 x2 (1216a.. (b5c9f.. x0 x0) (λ x3 . and (bij x0 x0 (λ x4 . f482f.. x3 x4)) (∀ x4 . prim1 x4 x1f482f.. x3 x4 = x4)))∀ x3 . prim1 x3 (1216a.. (b5c9f.. x0 x0) (λ x4 . and (bij x0 x0 (λ x5 . f482f.. x4 x5)) (∀ x5 . prim1 x5 x1f482f.. x4 x5 = x5)))prim1 (0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4))) (1216a.. (b5c9f.. x0 x0) (λ x4 . and (bij x0 x0 (λ x5 . f482f.. x4 x5)) (∀ x5 . prim1 x5 x1f482f.. x4 x5 = x5)))
Apply unknownprop_303ef75292a7bd9ed5b0c013e4f57cfe7915f538d6e5ad2c3b57bf918b912190 with x0, x1.
The subproof is completed by applying H0.
Claim L7: 4f2b4.. (987b2.. (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3))) (λ x2 x3 . 0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4))))
Apply unknownprop_18724cb817cb481b8967b1efe13d39d42daa75ec771890da7ad3a6b6981daf0e with 1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3)), λ x2 x3 . 0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4)).
The subproof is completed by applying unknownprop_bc372826b7f0da52f3a8a3ea86862b41fc91267615627787d3fb4a389b8c72dc with x0.
Apply unknownprop_8b9f561399e269db803fe2eecd073d07a2901172a21a3c5747e20aa002026685 with 1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3)), λ x2 x3 . 0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4)), 1216a.. (b5c9f.. x0 x0) (λ x2 . and (bij x0 x0 (λ x3 . f482f.. x2 x3)) (∀ x3 . prim1 x3 x1f482f.. x2 x3 = x3)) leaving 5 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L1.
The subproof is completed by applying L3.
The subproof is completed by applying L5.
The subproof is completed by applying L6.