Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ιι be given.
Let x2 of type ιι be given.
Let x3 of type ιι be given.
Assume H0: infinite x0.
Assume H1: ∀ x4 . x4x0infinite x4and (x1 x4x4) (infinite (x1 x4)).
Assume H2: ∀ x4 . x4x0infinite x4and (x2 x4x4) (nIn (x2 x4) (x1 x4)).
Assume H3: x3 0 = x1 x0.
Assume H4: ∀ x4 . nat_p x4x3 (ordsucc x4) = x1 (x3 x4).
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ∀ x4 . x4omega∀ x5 . x5x4x2 (x3 x5) = x2 (x3 x4)∀ x6 : ο . x6
Let x4 of type ι be given.
Assume H7: x4omega.
Let x5 of type ι be given.
Assume H8: x5x4.
Assume H9: x2 (x3 x5) = x2 (x3 x4).
Claim L10: ...
...
Apply L5 with x4, False leaving 2 subgoals.
Apply omega_nat_p with x4.
The subproof is completed by applying H7.
Assume H11: x3 x4x0.
Assume H12: infinite (x3 x4).
Apply H2 with x3 x4, False leaving 3 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
Assume H13: x2 (x3 x4)x3 x4.
Assume H14: nIn (x2 (x3 x4)) (x1 (x3 x4)).
Apply L5 with x5, False leaving 2 subgoals.
The subproof is completed by applying L10.
Assume H15: x3 x5x0.
Assume H16: infinite (x3 x5).
Apply H2 with x3 x5, False leaving 3 subgoals.
The subproof is completed by applying H15.
The subproof is completed by applying H16.
Assume H17: x2 (x3 x5)x3 x5.
Assume H18: nIn (x2 (x3 x5)) (x1 (x3 x5)).
Apply H18.
Apply H9 with λ x6 x7 . x7x1 (x3 x5).
Apply H4 with x5, λ x6 x7 . x3 x4x6, x2 (x3 x4) leaving 3 subgoals.
The subproof is completed by applying L10.
Apply L6 with ordsucc x5, x4 leaving 3 subgoals.
Apply omega_ordsucc with x5.
Apply nat_p_omega with x5.
The subproof is completed by applying L10.
The subproof is completed by applying H7.
Apply ordinal_ordsucc_In_Subq with x4, x5 leaving 2 subgoals.
Apply nat_p_ordinal with x4.
Apply omega_nat_p with x4.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H13.
Apply and3I with ∀ x4 . nat_p x4and (x3 x4x0) (infinite (x3 x4)), ∀ x4 . x4omega∀ x5 . x5omegax4x5x3 x5x3 x4, ∀ x4 . x4omega∀ x5 . x5omegax2 (x3 x4) = x2 (x3 x5)x4 = x5 leaving 3 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L6.
Let x4 of type ι be given.
Assume H8: x4omega.
Let x5 of type ι be given.
Assume H9: x5omega.
Assume H10: x2 (x3 x4) = x2 (x3 x5).
Apply ordinal_trichotomy_or_impred with x4, x5, x4 = x5 leaving 5 subgoals.
Apply nat_p_ordinal with x4.
Apply omega_nat_p with x4.
The subproof is completed by applying H8.
Apply nat_p_ordinal with x5.
Apply omega_nat_p with x5.
The subproof is completed by applying H9.
Assume H11: x4x5.
Apply FalseE with x4 = x5.
Apply L7 with x5, x4 leaving 3 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H11.
The subproof is completed by applying H10.
Assume H11: x4 = x5.
The subproof is completed by applying H11.
Assume H11: x5x4.
Apply FalseE with x4 = x5.
Apply L7 with x4, x5 leaving 3 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H11.
Let x6 of type ιιο be given.
The subproof is completed by applying H10 with λ x7 x8 . x6 x8 x7.