Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Apply SNoCutP_SNoCut_impred with Sing x0, SNoR x0, SNo_extend1 x0 = SNoCut (Sing x0) (SNoR x0) leaving 2 subgoals.
Apply unknownprop_d513e1fa055b07c519f2449ae6db6528e4c0b356ddbfd75ad29f8540a234c901 with x0.
The subproof is completed by applying H0.
Assume H1: SNo (SNoCut (Sing x0) (SNoR x0)).
Assume H2: SNoLev (SNoCut (Sing x0) (SNoR x0)) ∈ ordsucc (binunion (famunion (Sing x0) (λ x1 . ordsucc (SNoLev x1))) (famunion (SNoR x0) (λ x1 . ordsucc (SNoLev x1)))).
Assume H3: ∀ x1 . x1 ∈ Sing x0 ⟶ SNoLt x1 (SNoCut (Sing x0) (SNoR x0)).
Assume H4: ∀ x1 . x1 ∈ SNoR x0 ⟶ SNoLt (SNoCut (Sing x0) (SNoR x0)) x1.
Assume H5: ∀ x1 . SNo x1 ⟶ (∀ x2 . x2 ∈ Sing x0 ⟶ SNoLt x2 x1) ⟶ (∀ x2 . x2 ∈ SNoR x0 ⟶ SNoLt x1 x2) ⟶ and (SNoLev (SNoCut (Sing x0) (SNoR x0)) ⊆ SNoLev x1) (SNoEq_ (SNoLev (SNoCut (Sing x0) (SNoR x0))) (SNoCut (Sing x0) (SNoR x0)) x1).
Apply H5 with SNo_extend1 x0, SNo_extend1 x0 = SNoCut (Sing x0) (SNoR x0) leaving 4 subgoals.
Apply SNo_extend1_SNo with x0.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H6: x1 ∈ Sing x0.
Apply SingE with x0, x1, λ x2 x3 . SNoLt x3 (SNo_extend1 x0) leaving 2 subgoals.
The subproof is completed by applying H6.
Apply SNo_extend1_Gt with x0.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H6: x1 ∈ SNoR x0.
Apply SNoR_E with x0, x1, SNoLt (SNo_extend1 x0) x1 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 x0 x1.
Apply SNoLtE with x0, x1, SNoLt (SNo_extend1 x0) x1 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H7.
The subproof is completed by applying H9.
Let x2 of type ι be given.
Assume H10: SNo x2.
Assume H11: SNoLev x2 ∈ binintersect (SNoLev x0) (SNoLev x1).
Assume H12: SNoEq_ (SNoLev x2) x2 x0.
Assume H13: SNoEq_ (SNoLev x2) x2 x1.
Assume H14: SNoLt x0 x2.
Assume H15: SNoLt x2 x1.
Assume H16: nIn (SNoLev x2) x0.
Assume H17: SNoLev x2 ∈ x1.
Apply SNoLt_tra with SNo_extend1 x0, x2, x1 leaving 5 subgoals.
Apply SNo_extend1_SNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H10.
The subproof is completed by applying H7.
Claim L18: SNoLev x2 ∈ ...
...
Apply SNoLtI3 with SNo_extend1 x0, x2 leaving 3 subgoals.
Apply SNo_extend1_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, SNo_extend1 x0, x0, x2 leaving 2 subgoals.
Apply SNoEq_antimon_ with SNoLev x0, SNoLev x2, SNo_extend1 x0, x0 leaving 3 subgoals.
Apply SNoLev_ordinal with x0.
The subproof is completed by applying H0.
The subproof is completed by applying L18.
Apply SNo_extend1_SNoEq with x0.
The subproof is completed by applying H0.
Apply SNoEq_sym_ with SNoLev x2, x2, x0.
The subproof is completed by applying H12.
Assume H19: SNoLev x2 ∈ SNo_extend1 x0.
Apply H16.
Apply SNoEq_E1 with SNoLev x0, SNo_extend1 x0, x0, SNoLev x2 leaving 3 subgoals.
Apply SNo_extend1_SNoEq with x0.
The subproof is completed by applying H0.
The subproof is completed by applying L18.
The subproof is completed by applying H19.
...
...
...
...
■