Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: ∀ x0 x1 x2 x3 x4 . (∀ x5 . x5 ∈ x1 ⟶ SNo x5) ⟶ SNo (SNoCut x0 x1) ⟶ (∀ x5 . x5 ∈ x1 ⟶ SNoLt (SNoCut x0 x1) x5) ⟶ (∀ x5 . SNo x5 ⟶ (∀ x6 . x6 ∈ x0 ⟶ SNoLt x6 x5) ⟶ (∀ x6 . x6 ∈ x1 ⟶ SNoLt x5 x6) ⟶ and (SNoLev (SNoCut x0 x1) ⊆ SNoLev x5) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x5)) ⟶ SNo x4 ⟶ SNoLt x4 (SNoCut x0 x1) ⟶ (∀ x5 . x5 ∈ x0 ⟶ SNoLt x5 x4) ⟶ not (∀ x5 . x5 ∈ x1 ⟶ SNoLt x4 x5).
Claim L1: ...
...
Claim L2: ...
...
Claim L3: ∀ x0 . ... ⟶ SNoLt (SNoCut 0 0) ...
...
Claim L4: ∀ x0 . SNo x0 ⟶ (∀ x1 . x1 ∈ 0 ⟶ SNoLt x1 x0) ⟶ (∀ x1 . x1 ∈ 0 ⟶ SNoLt x0 x1) ⟶ and (SNoLev (SNoCut 0 0) ⊆ SNoLev x0) (SNoEq_ (SNoLev (SNoCut 0 0)) (SNoCut 0 0) x0)
Let x0 of type ι be given.
Assume H4: SNo x0.
Assume H5: ∀ x1 . x1 ∈ 0 ⟶ SNoLt x1 x0.
Assume H6: ∀ x1 . x1 ∈ 0 ⟶ SNoLt x0 x1.
Apply SNoCut_0_0 with λ x1 x2 . and (SNoLev x2 ⊆ SNoLev x0) (SNoEq_ (SNoLev x2) x2 x0).
Apply SNoLev_0 with λ x1 x2 . and (x2 ⊆ SNoLev x0) (SNoEq_ x2 0 x0).
Apply andI with 0 ⊆ SNoLev x0, SNoEq_ 0 0 x0 leaving 2 subgoals.
The subproof is completed by applying Subq_Empty with SNoLev x0.
Let x1 of type ι be given.
Assume H7: x1 ∈ 0.
Apply EmptyE with x1, iff (x1 ∈ 0) (x1 ∈ x0).
The subproof is completed by applying H7.
Claim L5: SNo (minus_SNo 1)
Apply SNo_minus_SNo with 1.
The subproof is completed by applying SNo_1.
Claim L6: SNoLt (minus_SNo 1) (SNoCut 0 0)
Apply SNoCut_0_0 with λ x0 x1 . SNoLt (minus_SNo 1) x1.
Apply minus_SNo_Lt_contra1 with 0, 1 leaving 3 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNo_1.
Apply minus_SNo_0 with λ x0 x1 . SNoLt x1 1.
The subproof is completed by applying SNoLt_0_1.
Claim L7: ∀ x0 . x0 ∈ 0 ⟶ SNoLt x0 (minus_SNo 1)
Let x0 of type ι be given.
Assume H7: x0 ∈ 0.
Apply EmptyE with x0, SNoLt x0 (minus_SNo 1).
The subproof is completed by applying H7.
Claim L8: not (not (∀ x0 . x0 ∈ 0 ⟶ SNoLt (minus_SNo 1) x0))
Assume H8: not (∀ x0 . x0 ∈ 0 ⟶ SNoLt (minus_SNo 1) x0).
Apply H8.
Let x0 of type ι be given.
Assume H9: x0 ∈ 0.
Apply EmptyE with x0, SNoLt (minus_SNo 1) x0.
The subproof is completed by applying H9.
Apply L8.
Apply H0 with 0, 0, 0, 0, minus_SNo 1 leaving 7 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
■