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))).
Apply unknownprop_e4362c04e65a765de9cf61045b78be0adc0f9e51a17754420e1088df0891ff67 with b5c9f.. x0 x0, λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3), x1, and (and (prim1 (0fc90.. x0 (λ x2 . inv x0 (λ x3 . f482f.. x1 x3) x2)) (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3)))) (0fc90.. x0 (λ x2 . f482f.. (0fc90.. x0 (λ x3 . inv x0 (λ x4 . f482f.. x1 x4) x3)) (f482f.. x1 x2)) = 0fc90.. x0 (λ x2 . x2))) (0fc90.. x0 (λ x2 . f482f.. x1 (f482f.. (0fc90.. x0 (λ x3 . inv x0 (λ x4 . f482f.. x1 x4) x3)) x2)) = 0fc90.. x0 (λ x2 . x2)) leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: prim1 x1 (b5c9f.. x0 x0).
Assume H2: bij x0 x0 (λ x2 . f482f.. x1 x2).
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Apply and3I with prim1 (0fc90.. x0 (λ x2 . inv x0 (λ x3 . f482f.. x1 x3) x2)) (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3))), 0fc90.. x0 (λ x2 . f482f.. (0fc90.. x0 (λ x3 . inv x0 (λ x4 . f482f.. x1 x4) x3)) (f482f.. x1 x2)) = 0fc90.. x0 (λ x2 . x2), 0fc90.. x0 (λ x2 . f482f.. x1 (f482f.. (0fc90.. x0 (λ x3 . inv x0 (λ x4 . f482f.. x1 x4) x3)) x2)) = 0fc90.. x0 (λ x2 . x2) leaving 3 subgoals.
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with b5c9f.. x0 x0, λ x2 . bij x0 x0 (λ x3 . f482f.. x2 x3), 0fc90.. x0 (λ x2 . inv x0 (λ x3 . f482f.. x1 x3) x2) leaving 2 subgoals.
Apply unknownprop_78f4273a7b4d13f02d77d194b65be481121674fd021f4ffb88d69be4bcd0ab71 with x0, λ x2 . x0, λ x2 . inv x0 (λ x3 . f482f.. x1 x3) x2.
The subproof is completed by applying L7.
Apply and3I with ∀ x2 . prim1 x2 x0prim1 (f482f.. (0fc90.. x0 (λ x3 . inv x0 (λ x4 . f482f.. x1 x4) x3)) x2) x0, ∀ x2 . ...∀ x3 . prim1 ... ...f482f.. (0fc90.. x0 (λ x4 . inv x0 (λ x5 . f482f.. x1 x5) x4)) x2 = f482f.. (0fc90.. x0 (λ x4 . inv x0 (λ x5 . f482f.. x1 x5) x4)) x3x2 = x3, ... leaving 3 subgoals.
...
...
...
...
...