Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: Subq x1 x0.
Apply and3I with 30750.. (987b2.. (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3))) (λ x2 x3 . 0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4)))), 30750.. (987b2.. (1216a.. (b5c9f.. x0 x0) (λ x2 . and (bij x0 x0 (λ x3 . f482f.. x2 x3)) (∀ x3 . prim1 x3 x1f482f.. x2 x3 = x3))) (λ x2 x3 . 0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4)))), 93c99.. (987b2.. (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3))) (λ x2 x3 . 0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4)))) (λ x2 . λ x3 : ι → ι → ι . 93c99.. (987b2.. (1216a.. (b5c9f.. x0 x0) (λ x4 . and (bij x0 x0 (λ x5 . f482f.. x4 x5)) (∀ x5 . prim1 x5 x1f482f.. x4 x5 = x5))) (λ x4 x5 . 0fc90.. x0 (λ x6 . f482f.. x5 (f482f.. x4 x6)))) (λ x4 . λ x5 : ι → ι → ι . and (and (987b2.. (1216a.. (b5c9f.. x0 x0) (λ x6 . and (bij x0 x0 (λ x7 . f482f.. x6 x7)) (∀ x7 . prim1 x7 x1f482f.. x6 x7 = x7))) (λ x6 x7 . 0fc90.. x0 (λ x8 . f482f.. x7 (f482f.. x6 x8))) = 987b2.. x4 x3) (4f2b4.. (987b2.. x4 x3))) (Subq x4 x2))) leaving 3 subgoals.
Apply unknownprop_10272f9d8a272cf914054010d8c3a4593cfbbcb7954b0a903e2d867e85e26e68 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_fa05ec58213d1b0cffa4f336539515d7ea4c1904e33786a57aa3d93e90546a62 with x0.
Apply unknownprop_10272f9d8a272cf914054010d8c3a4593cfbbcb7954b0a903e2d867e85e26e68 with 1216a.. (b5c9f.. x0 x0) (λ x2 . and (bij x0 x0 (λ x3 . f482f.. x2 x3)) (∀ x3 . prim1 x3 x1f482f.. x2 x3 = x3)), λ x2 x3 . 0fc90.. x0 (λ x4 . f482f.. x3 (f482f.. x2 x4)).
Apply unknownprop_303ef75292a7bd9ed5b0c013e4f57cfe7915f538d6e5ad2c3b57bf918b912190 with x0, x1.
The subproof is completed by applying H0.
Apply unknownprop_cd20f7dbc591f4f87c87c35509dc2db382cd96f4518c628ca9882a10b2d1671d with 1216a.. (b5c9f.. x0 x0) (λ x2 . and (bij x0 x0 (λ x3 . f482f.. x2 x3)) (∀ x3 . prim1 x3 x1f482f.. x2 x3 = x3)), 1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3)), λ x2 x3 . 0fc90.. ... ..., ..., ....
...