Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι(ιο) → ο be given.
Let x1 of type ι(ιο) → ο be given.
Assume H0: PNoLt_pwise x0 x1.
Let x2 of type ι be given.
Assume H1: ordinal x2.
Apply H1 with PNo_lenbdd x2 x0PNo_lenbdd x2 x1∃ x3 . and (x3ordsucc x2) (∃ x4 : ι → ο . PNo_rel_strict_split_imv x0 x1 x3 x4).
Assume H2: TransSet x2.
Assume H3: ∀ x3 . x3x2TransSet x3.
Assume H4: PNo_lenbdd x2 x0.
Assume H5: PNo_lenbdd x2 x1.
Claim L6: ...
...
Apply PNo_rel_imv_ex with x0, x1, x2, ∃ x3 . and (x3ordsucc x2) (∃ x4 : ι → ο . PNo_rel_strict_split_imv x0 x1 x3 x4) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H7: ∃ x3 : ι → ο . PNo_rel_strict_uniq_imv x0 x1 x2 x3.
Apply H7 with ∃ x3 . and (x3ordsucc x2) (∃ x4 : ι → ο . PNo_rel_strict_split_imv x0 x1 x3 x4).
Let x3 of type ιο be given.
Assume H8: PNo_rel_strict_uniq_imv x0 x1 x2 x3.
Apply H8 with ∃ x4 . and (x4ordsucc x2) (∃ x5 : ι → ο . PNo_rel_strict_split_imv x0 x1 x4 x5).
Assume H9: PNo_rel_strict_imv x0 x1 x2 x3.
Apply H9 with (∀ x4 : ι → ο . PNo_rel_strict_imv x0 x1 x2 x4PNoEq_ x2 x3 x4)∃ x4 . and (x4ordsucc x2) (∃ x5 : ι → ο . PNo_rel_strict_split_imv x0 x1 x4 x5).
Assume H10: PNo_rel_strict_upperbd x0 x2 x3.
Assume H11: PNo_rel_strict_lowerbd x1 x2 x3.
Assume H12: ∀ x4 : ι → ο . PNo_rel_strict_imv x0 x1 x2 x4PNoEq_ x2 x3 x4.
Let x4 of type ο be given.
Assume H13: ∀ x5 . and (x5ordsucc x2) (∃ x6 : ι → ο . PNo_rel_strict_split_imv x0 x1 x5 x6)x4.
Apply H13 with x2.
Apply andI with x2ordsucc x2, ∃ x5 : ι → ο . PNo_rel_strict_split_imv x0 x1 x2 x5 leaving 2 subgoals.
The subproof is completed by applying ordsuccI2 with x2.
Let x5 of type ο be given.
Assume H14: ∀ x6 : ι → ο . PNo_rel_strict_split_imv x0 x1 x2 x6x5.
Apply H14 with x3.
Apply PNo_lenbdd_strict_imv_split with x0, x1, x2, x3 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H9.
Assume H7: ∃ x3 . and (x3x2) (∃ x4 : ι → ο . PNo_rel_strict_split_imv x0 x1 x3 x4).
Apply H7 with ∃ x3 . and (x3ordsucc x2) (∃ x4 : ι → ο . PNo_rel_strict_split_imv x0 x1 x3 x4).
Let x3 of type ι be given.
Assume H8: (λ x4 . and (x4x2) (∃ x5 : ι → ο . PNo_rel_strict_split_imv x0 x1 x4 x5)) x3.
Apply H8 with ∃ x4 . and (x4ordsucc x2) (∃ x5 : ι → ο . PNo_rel_strict_split_imv x0 x1 x4 x5).
Assume H9: x3x2.
Assume H10: ∃ x4 : ι → ο . PNo_rel_strict_split_imv x0 x1 x3 x4.
Let x4 of type ο be given.
Assume H11: ∀ x5 . and (x5ordsucc x2) (∃ x6 : ι → ο . PNo_rel_strict_split_imv x0 x1 x5 x6)x4.
Apply H11 with ....
...