Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: prim1 x1 (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3))).
Let x2 of type ι be given.
Assume H1: prim1 x2 (1216a.. (b5c9f.. x0 x0) (λ x3 . bij x0 x0 (λ x4 . f482f.. x3 x4))).
Apply unknownprop_e4362c04e65a765de9cf61045b78be0adc0f9e51a17754420e1088df0891ff67 with b5c9f.. x0 x0, λ x3 . bij x0 x0 (λ x4 . f482f.. x3 x4), x1, 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))) leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H2: prim1 x1 (b5c9f.. x0 x0).
Assume H3: bij x0 x0 (λ x3 . f482f.. x1 x3).
Apply unknownprop_e4362c04e65a765de9cf61045b78be0adc0f9e51a17754420e1088df0891ff67 with b5c9f.. x0 x0, λ x3 . bij x0 x0 (λ x4 . f482f.. x3 x4), x2, 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))) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H4: prim1 x2 (b5c9f.. x0 x0).
Assume H5: bij x0 x0 (λ x3 . f482f.. x2 x3).
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with b5c9f.. x0 x0, λ x3 . bij x0 x0 (λ x4 . f482f.. x3 x4), (λ x3 x4 . 0fc90.. x0 (λ x5 . f482f.. x4 (f482f.. x3 x5))) x1 x2 leaving 2 subgoals.
Apply unknownprop_78f4273a7b4d13f02d77d194b65be481121674fd021f4ffb88d69be4bcd0ab71 with x0, λ x3 . x0, λ x3 . f482f.. x2 (f482f.. x1 x3).
Let x3 of type ι be given.
Assume H12: prim1 x3 x0.
Apply L9 with f482f.. x1 x3.
Apply L6 with x3.
The subproof is completed by applying H12.
Apply and3I with ∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. (0fc90.. x0 (λ x4 . f482f.. x2 (f482f.. x1 x4))) x3) x0, ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ f482f.. (0fc90.. x0 (λ x5 . f482f.. x2 (f482f.. x1 x5))) x3 = f482f.. (0fc90.. x0 (λ x5 . f482f.. x2 (f482f.. x1 x5))) x4 ⟶ x3 = x4, ∀ x3 . prim1 x3 x0 ⟶ ∃ x4 . and (prim1 x4 x0) (f482f.. (0fc90.. x0 (λ x5 . f482f.. x2 (f482f.. x1 x5))) x4 = x3) leaving 3 subgoals.
Let x3 of type ι be given.
Assume H12: prim1 x3 x0.
Apply unknownprop_b456609235d152f08bccfce314d541d7c44f3716137c00b0ce21cf467ba83d17 with x0, λ x4 . f482f.. x2 (f482f.. x1 x4), x3, λ x4 x5 . prim1 x5 x0 leaving 2 subgoals.
The subproof is completed by applying H12.
Apply L9 with f482f.. x1 x3.
Apply L6 with ....
...
...
...
■