Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: infinite x0.
Apply nat_ind with λ x1 . ∃ x2 . and (x2x0) (equip x2 x1) leaving 2 subgoals.
Let x1 of type ο be given.
Assume H1: ∀ x2 . and (x2x0) (equip x2 0)x1.
Apply H1 with 0.
Apply andI with 0x0, equip 0 0 leaving 2 subgoals.
The subproof is completed by applying Subq_Empty with x0.
The subproof is completed by applying equip_ref with 0.
Let x1 of type ι be given.
Assume H1: nat_p x1.
Assume H2: ∃ x2 . and (x2x0) (equip x2 x1).
Apply H2 with ∃ x2 . and (x2x0) (equip x2 (ordsucc x1)).
Let x2 of type ι be given.
Assume H3: (λ x3 . and (x3x0) (equip x3 x1)) x2.
Apply H3 with ∃ x3 . and (x3x0) (equip x3 (ordsucc x1)).
Assume H4: x2x0.
Assume H5: equip x2 x1.
Apply H5 with ∃ x3 . and (x3x0) (equip x3 (ordsucc x1)).
Let x3 of type ιι be given.
Assume H6: bij x2 x1 x3.
Apply H6 with ∃ x4 . and (x4x0) (equip x4 (ordsucc x1)).
Assume H7: and (∀ x4 . x4x2x3 x4x1) (∀ x4 . x4x2∀ x5 . x5x2x3 x4 = x3 x5x4 = x5).
Apply H7 with (∀ x4 . x4x1∃ x5 . and (x5x2) (x3 x5 = x4))∃ x4 . and (x4x0) (equip x4 (ordsucc x1)).
Assume H8: ∀ x4 . x4x2x3 x4x1.
Assume H9: ∀ x4 . x4x2∀ x5 . x5x2x3 x4 = x3 x5x4 = x5.
Assume H10: ∀ x4 . x4x1∃ x5 . and (x5x2) (x3 x5 = x4).
Apply dneg with ∃ x4 . and (x4x0) (nIn x4 x2), ∃ x4 . and (x4x0) (equip x4 (ordsucc x1)) leaving 2 subgoals.
Assume H11: not (∃ x4 . and (x4x0) (nIn x4 x2)).
Apply H0.
Let x4 of type ο be given.
Assume H12: ∀ x5 . and (x5omega) (equip x0 x5)x4.
Apply H12 with x1.
Apply andI with x1omega, equip x0 x1 leaving 2 subgoals.
Apply nat_p_omega with x1.
The subproof is completed by applying H1.
Apply set_ext with x2, x0, λ x5 x6 . equip x5 x1 leaving 3 subgoals.
The subproof is completed by applying H4.
Let x5 of type ι be given.
Assume H13: x5x0.
Apply dneg with x5x2.
Assume H14: nIn x5 x2.
Apply H11.
Let x6 of type ο be given.
Assume H15: ∀ x7 . and (x7x0) (nIn x7 x2)x6.
Apply H15 with x5.
Apply andI with x5x0, nIn x5 x2 leaving 2 subgoals.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
The subproof is completed by applying H5.
...