Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNoLt 0 x0.
Assume H2: SNoLev x01.
Apply SNoLtE with 0, x0, x0 = 1 leaving 6 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H3: SNo x1.
Assume H4: SNoLev x1binintersect (SNoLev 0) (SNoLev x0).
Apply FalseE with SNoEq_ (SNoLev x1) x1 0SNoEq_ (SNoLev x1) x1 x0SNoLt 0 x1SNoLt x1 x0nIn (SNoLev x1) 0SNoLev x1x0x0 = 1.
Apply EmptyE with SNoLev x1.
Apply ordinal_SNoLev with 0, λ x2 x3 . SNoLev x1x2 leaving 2 subgoals.
The subproof is completed by applying ordinal_Empty.
Apply binintersectE1 with SNoLev 0, SNoLev x0, SNoLev x1.
The subproof is completed by applying H4.
Apply ordinal_SNoLev with 0, λ x1 x2 . x2SNoLev x0SNoEq_ x2 0 x0x2x0x0 = 1 leaving 2 subgoals.
The subproof is completed by applying ordinal_Empty.
Assume H3: 0SNoLev x0.
Assume H4: SNoEq_ 0 0 x0.
Assume H5: 0x0.
Claim L6: SNoLev x0 = 1
Apply set_ext with SNoLev x0, 1 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x1 of type ι be given.
Assume H6: x11.
Apply cases_1 with x1, λ x2 . x2SNoLev x0 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H3.
Apply SNo_eq with x0, 1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_1.
Apply ordinal_SNoLev with 1, λ x1 x2 . SNoLev x0 = x2 leaving 2 subgoals.
Apply nat_p_ordinal with 1.
The subproof is completed by applying nat_1.
The subproof is completed by applying L6.
Apply L6 with λ x1 x2 . SNoEq_ x2 x0 1.
Let x1 of type ι be given.
Assume H7: x11.
Apply cases_1 with x1, λ x2 . iff (x2x0) (x21) leaving 2 subgoals.
The subproof is completed by applying H7.
Apply iffI with 0x0, 01 leaving 2 subgoals.
Assume H8: 0x0.
The subproof is completed by applying In_0_1.
Assume H8: 01.
The subproof is completed by applying H5.
Assume H3: SNoLev x0SNoLev 0.
Apply FalseE with SNoEq_ (SNoLev x0) 0 x0nIn (SNoLev x0) 0x0 = 1.
Apply EmptyE with SNoLev x0.
Apply ordinal_SNoLev with 0, λ x1 x2 . SNoLev x0x1 leaving 2 subgoals.
The subproof is completed by applying ordinal_Empty.
The subproof is completed by applying H3.