Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: 1 ∈ x0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H2: 68498.. x0 x2.
Assume H3: SNo x3.
Assume H4: SNo x4.
Assume H5: binunion x1 {(λ x6 . SetAdjoin x6 (Sing x0)) x5|x5 ∈ x3} = binunion x2 {(λ x6 . SetAdjoin x6 (Sing x0)) x5|x5 ∈ x4}.
Let x5 of type ι be given.
Assume H6: x5 ∈ x3.
Claim L7: ...
...
Apply binunionE with x2, {(λ x7 . SetAdjoin x7 (Sing x0)) x6|x6 ∈ x4}, (λ x6 . SetAdjoin x6 (Sing x0)) x5, x5 ∈ x4 leaving 3 subgoals.
The subproof is completed by applying L7.
Assume H8: (λ x6 . SetAdjoin x6 (Sing x0)) x5 ∈ x2.
Apply FalseE with x5 ∈ x4.
Apply H2 with (λ x6 . SetAdjoin x6 (Sing x0)) x5, False leaving 2 subgoals.
The subproof is completed by applying H8.
Let x6 of type ι be given.
Assume H9: (λ x7 . and (SNo x7) (or (SetAdjoin x5 (Sing x0) ∈ x7) (∃ x8 . and (x8 ∈ x7) (∃ x9 . and (x9 ∈ x0) (and (1 ∈ x9) (SetAdjoin x5 (Sing x0) = SetAdjoin x8 (Sing x9))))))) x6.
Apply H9 with False.
Assume H10: SNo x6.
Assume H11: or (SetAdjoin x5 (Sing x0) ∈ x6) (∃ x7 . and (x7 ∈ x6) (∃ x8 . and (x8 ∈ x0) (and (1 ∈ x8) (SetAdjoin x5 (Sing x0) = SetAdjoin x7 (Sing x8))))).
Apply H11 with False leaving 2 subgoals.
Assume H12: (λ x7 . SetAdjoin x7 (Sing x0)) x5 ∈ x6.
Apply unknownprop_b77e4d13156bc801da7c50d615690a07853273eb1e278cd0903fec4370f9e4e2 with x0, x6, x5 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H10.
The subproof is completed by applying H12.
Assume H12: ∃ x7 . and (x7 ∈ x6) (∃ x8 . and (x8 ∈ x0) (and (1 ∈ x8) (SetAdjoin x5 (Sing x0) = SetAdjoin x7 (Sing x8)))).
Apply H12 with False.
Let x7 of type ι be given.
Assume H13: (λ x8 . and (x8 ∈ x6) (∃ x9 . and (x9 ∈ x0) (and (1 ∈ x9) (SetAdjoin x5 (Sing x0) = SetAdjoin x8 (Sing x9))))) x7.
Apply H13 with False.
Assume H14: x7 ∈ x6.
Assume H15: ∃ x8 . and (x8 ∈ x0) (and (1 ∈ x8) (SetAdjoin x5 (Sing x0) = SetAdjoin x7 (Sing x8))).
Apply H15 with False.
Let x8 of type ι be given.
Assume H16: (λ x9 . and (x9 ∈ x0) (and (1 ∈ x9) (SetAdjoin x5 (Sing x0) = SetAdjoin x7 (Sing x9)))) x8.
Apply H16 with False.
Assume H17: x8 ∈ x0.
Assume H18: and (1 ∈ x8) (SetAdjoin x5 (Sing x0) = ...).
...
...
■