Search for blocks/addresses/...

Proofgold Proof

pf
Apply SNoLev_ind with λ x0 . add_SNo (minus_SNo x0) x0 = 0.
Let x0 of type ι be given.
Assume H0: SNo x0.
Assume H1: ∀ x1 . x1 ∈ SNoS_ (SNoLev x0) ⟶ add_SNo (minus_SNo x1) x1 = 0.
Claim L2: ...
...
Apply add_SNo_eq with minus_SNo x0, x0, λ x1 x2 . x2 = 0 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H0.
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Apply L5 with SNoCut (binunion {add_SNo x1 x0|x1 ∈ SNoL (minus_SNo x0)} {add_SNo (minus_SNo x0) x1|x1 ∈ SNoL x0}) (binunion {add_SNo x1 x0|x1 ∈ SNoR (minus_SNo x0)} {add_SNo (minus_SNo x0) x1|x1 ∈ SNoR x0}) = 0.
Assume H6: SNoLev (SNoCut (binunion {add_SNo x1 x0|x1 ∈ SNoL (minus_SNo x0)} {add_SNo (minus_SNo x0) x1|x1 ∈ SNoL x0}) (binunion {add_SNo x1 x0|x1 ∈ SNoR (minus_SNo x0)} {add_SNo (minus_SNo x0) x1|x1 ∈ SNoR x0})) ⊆ SNoLev 0.
Assume H7: SNoEq_ (SNoLev (SNoCut (binunion {add_SNo x1 x0|x1 ∈ SNoL (minus_SNo x0)} {add_SNo (minus_SNo x0) x1|x1 ∈ SNoL x0}) (binunion {add_SNo x1 x0|x1 ∈ SNoR (minus_SNo x0)} {add_SNo (minus_SNo x0) x1|x1 ∈ SNoR x0}))) (SNoCut (binunion {add_SNo x1 x0|x1 ∈ SNoL (minus_SNo x0)} {add_SNo (minus_SNo x0) x1|x1 ∈ SNoL x0}) (binunion {add_SNo x1 x0|x1 ∈ SNoR (minus_SNo x0)} {add_SNo (minus_SNo x0) x1|x1 ∈ SNoR x0})) 0.
Apply SNo_eq with SNoCut (binunion {add_SNo x1 x0|x1 ∈ SNoL (minus_SNo x0)} {add_SNo (minus_SNo x0) x1|x1 ∈ SNoL x0}) (binunion {add_SNo x1 x0|x1 ∈ SNoR (minus_SNo x0)} {add_SNo (minus_SNo x0) x1|x1 ∈ SNoR x0}), 0 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying SNo_0.
Apply set_ext with SNoLev (SNoCut (binunion {add_SNo x1 x0|x1 ∈ SNoL (minus_SNo x0)} {add_SNo (minus_SNo x0) x1|x1 ∈ SNoL x0}) (binunion {add_SNo x1 x0|x1 ∈ SNoR (minus_SNo x0)} {add_SNo (minus_SNo x0) x1|x1 ∈ SNoR x0})), SNoLev 0 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply ordinal_SNoLev with 0, λ x1 x2 . x2 ⊆ SNoLev (SNoCut (binunion {add_SNo x3 x0|x3 ∈ SNoL (minus_SNo x0)} {add_SNo (minus_SNo x0) x3|x3 ∈ SNoL x0}) (binunion {add_SNo x3 x0|x3 ∈ SNoR (minus_SNo x0)} {add_SNo (minus_SNo x0) x3|x3 ∈ SNoR x0})) leaving 2 subgoals.
The subproof is completed by applying ordinal_Empty.
The subproof is completed by applying Subq_Empty with SNoLev ....
...
■