Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply and3I with ∀ x1 . prim1 x1 (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3)))∀ x2 . prim1 x2 (1216a.. (b5c9f.. x0 x0) (λ x3 . bij x0 x0 (λ x4 . f482f.. x3 x4)))prim1 ((λ x3 x4 . 0fc90.. x0 (λ x5 . f482f.. x4 (f482f.. x3 x5))) x1 x2) (1216a.. (b5c9f.. x0 x0) (λ x3 . bij x0 x0 (λ x4 . f482f.. x3 x4))), ∀ x1 . prim1 x1 (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3)))∀ x2 . prim1 x2 (1216a.. (b5c9f.. x0 x0) (λ x3 . bij x0 x0 (λ x4 . f482f.. x3 x4)))∀ x3 . prim1 x3 (1216a.. (b5c9f.. x0 x0) (λ x4 . bij x0 x0 (λ x5 . f482f.. x4 x5)))(λ x4 x5 . 0fc90.. x0 (λ x6 . f482f.. x5 (f482f.. x4 x6))) x1 ((λ x4 x5 . 0fc90.. x0 (λ x6 . f482f.. x5 (f482f.. x4 x6))) x2 x3) = (λ x4 x5 . 0fc90.. x0 (λ x6 . f482f.. x5 (f482f.. x4 x6))) ((λ x4 x5 . 0fc90.. x0 (λ x6 . f482f.. x5 (f482f.. x4 x6))) x1 x2) x3, ∃ x1 . and (prim1 x1 (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3)))) (and (∀ x2 . prim1 x2 (1216a.. (b5c9f.. x0 x0) (λ x3 . bij x0 x0 (λ x4 . f482f.. x3 x4)))and ((λ x3 x4 . 0fc90.. x0 (λ x5 . f482f.. x4 (f482f.. x3 x5))) x1 x2 = x2) ((λ x3 x4 . 0fc90.. x0 (λ x5 . f482f.. x4 (f482f.. x3 x5))) x2 x1 = x2)) (∀ x2 . prim1 x2 (1216a.. (b5c9f.. x0 x0) (λ x3 . bij x0 ... ...))∃ x3 . and (prim1 x3 (1216a.. (b5c9f.. x0 x0) (λ x4 . bij x0 x0 (λ x5 . f482f.. x4 x5)))) (and ((λ x4 x5 . 0fc90.. x0 (λ x6 . f482f.. x5 (f482f.. x4 x6))) x2 x3 = x1) ((λ x4 x5 . 0fc90.. x0 (λ x6 . f482f.. x5 (f482f.. x4 x6))) x3 x2 = x1)))) leaving 3 subgoals.
...
...
...