Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Apply SNoCutP_SNoCut_impred with SNoL x0, Sing x0, SNo_extend0 x0 = SNoCut (SNoL x0) (Sing x0) leaving 2 subgoals.
Apply unknownprop_21fcbb02f8b347d28567534e691cc39dcd7545295c025757bc8e2c9893ad0787 with x0.
The subproof is completed by applying H0.
Assume H1: SNo (SNoCut (SNoL x0) (Sing x0)).
Assume H2: SNoLev (SNoCut (SNoL x0) (Sing x0)) ∈ ordsucc (binunion (famunion (SNoL x0) (λ x1 . ordsucc (SNoLev x1))) (famunion (Sing x0) (λ x1 . ordsucc (SNoLev x1)))).
Assume H3: ∀ x1 . x1 ∈ SNoL x0 ⟶ SNoLt x1 (SNoCut (SNoL x0) (Sing x0)).
Assume H4: ∀ x1 . x1 ∈ Sing x0 ⟶ SNoLt (SNoCut (SNoL x0) (Sing x0)) x1.
Assume H5: ∀ x1 . SNo x1 ⟶ (∀ x2 . x2 ∈ SNoL x0 ⟶ SNoLt x2 x1) ⟶ (∀ x2 . x2 ∈ Sing x0 ⟶ SNoLt x1 x2) ⟶ and (SNoLev (SNoCut (SNoL x0) (Sing x0)) ⊆ SNoLev x1) (SNoEq_ (SNoLev (SNoCut (SNoL x0) (Sing x0))) (SNoCut (SNoL x0) (Sing x0)) x1).
Apply H5 with SNo_extend0 x0, SNo_extend0 x0 = SNoCut (SNoL x0) (Sing x0) leaving 4 subgoals.
Apply SNo_extend0_SNo with x0.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H6: x1 ∈ SNoL x0.
Apply SNoL_E with x0, x1, SNoLt x1 (SNo_extend0 x0) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
Assume H7: SNo x1.
Assume H8: SNoLev x1 ∈ SNoLev x0.
Assume H9: SNoLt x1 x0.
Apply SNoLtE with x1, x0, SNoLt x1 (SNo_extend0 x0) leaving 6 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H0.
The subproof is completed by applying H9.
Let x2 of type ι be given.
Assume H10: SNo x2.
Assume H11: SNoLev x2 ∈ binintersect (SNoLev x1) (SNoLev x0).
Assume H12: SNoEq_ (SNoLev x2) x2 x1.
Assume H13: SNoEq_ (SNoLev x2) x2 x0.
Assume H14: SNoLt x1 x2.
Assume H15: SNoLt x2 x0.
Assume H16: nIn (SNoLev x2) x1.
Assume H17: SNoLev x2 ∈ x0.
Apply SNoLt_tra with x1, x2, SNo_extend0 x0 leaving 5 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H10.
Apply SNo_extend0_SNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H14.
Claim L18: SNoLev x2 ∈ SNoLev x0
Apply binintersectE2 with SNoLev x1, SNoLev x0, SNoLev x2.
The subproof is completed by applying H11.
Apply SNoLtI2 with x2, SNo_extend0 x0 leaving 3 subgoals.
Apply SNo_extend0_SNoLev with x0, λ x3 x4 . SNoLev x2 ∈ x4 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply ordsuccI1 with SNoLev x0, SNoLev x2.
The subproof is completed by applying L18.
Apply SNoEq_tra_ with SNoLev x2, x2, x0, SNo_extend0 x0 leaving 2 subgoals.
The subproof is completed by applying H13.
Apply SNoEq_antimon_ with SNoLev x0, SNoLev x2, x0, SNo_extend0 x0 leaving 3 subgoals.
Apply SNoLev_ordinal with x0.
The subproof is completed by applying H0.
The subproof is completed by applying L18.
Apply SNoEq_sym_ with SNoLev x0, SNo_extend0 x0, x0.
Apply SNo_extend0_SNoEq with x0.
The subproof is completed by applying H0.
Apply SNoEq_E2 with SNoLev x0, SNo_extend0 x0, x0, SNoLev x2 leaving 3 subgoals.
Apply SNo_extend0_SNoEq with x0.
The subproof is completed by applying H0.
The subproof is completed by applying L18.
The subproof is completed by applying H17.
Assume H10: SNoLev x1 ∈ SNoLev x0.
...
...
...
...
■