Search for blocks/addresses/...

Proofgold Proof

pf
Apply SNoLev_ind2 with λ x0 x1 . SNoLev (add_SNo x0 x1) ⊆ add_SNo (SNoLev x0) (SNoLev x1).
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Claim L2: ...
...
Claim L3: ...
...
Assume H4: ∀ x2 . x2 ∈ SNoS_ (SNoLev x0) ⟶ (λ x3 x4 . SNoLev (add_SNo x3 x4) ⊆ add_SNo (SNoLev x3) (SNoLev x4)) x2 x1.
Assume H5: ∀ x2 . x2 ∈ SNoS_ (SNoLev x1) ⟶ (λ x3 x4 . SNoLev (add_SNo x3 x4) ⊆ add_SNo (SNoLev x3) (SNoLev x4)) x0 x2.
Assume H6: ∀ x2 . x2 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x3 . x3 ∈ SNoS_ (SNoLev x1) ⟶ (λ x4 x5 . SNoLev (add_SNo x4 x5) ⊆ add_SNo (SNoLev x4) (SNoLev x5)) x2 x3.
Apply add_SNo_eq with x0, x1, λ x2 x3 . SNoLev x3 ⊆ add_SNo (SNoLev x0) (SNoLev x1) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Claim L7: ...
...
Apply SNoCutP_SNoCut_impred with binunion {add_SNo x2 x1|x2 ∈ SNoL x0} {add_SNo x0 x2|x2 ∈ SNoL x1}, binunion {add_SNo x2 x1|x2 ∈ SNoR x0} {add_SNo x0 x2|x2 ∈ SNoR x1}, SNoLev (SNoCut (binunion {add_SNo x2 x1|x2 ∈ SNoL x0} {add_SNo x0 x2|x2 ∈ SNoL x1}) (binunion {add_SNo x2 x1|x2 ∈ SNoR x0} {add_SNo x0 x2|x2 ∈ SNoR x1})) ⊆ add_SNo (SNoLev x0) (SNoLev x1) leaving 2 subgoals.
The subproof is completed by applying L7.
Assume H8: SNo (SNoCut (binunion {add_SNo x2 x1|x2 ∈ SNoL x0} {add_SNo x0 x2|x2 ∈ SNoL x1}) (binunion {add_SNo x2 x1|x2 ∈ SNoR x0} {add_SNo x0 x2|x2 ∈ SNoR x1})).
Assume H9: SNoLev (SNoCut (binunion {add_SNo x2 x1|x2 ∈ SNoL x0} {add_SNo x0 x2|x2 ∈ SNoL x1}) (binunion {add_SNo x2 x1|x2 ∈ SNoR x0} {add_SNo x0 x2|x2 ∈ SNoR x1})) ∈ ordsucc (binunion (famunion (binunion {add_SNo x2 x1|x2 ∈ SNoL x0} {add_SNo x0 x2|x2 ∈ SNoL x1}) (λ x2 . ordsucc (SNoLev x2))) (famunion (binunion {add_SNo x2 x1|x2 ∈ SNoR x0} {add_SNo x0 x2|x2 ∈ SNoR x1}) (λ x2 . ordsucc (SNoLev x2)))).
Assume H10: ∀ x2 . ... ⟶ SNoLt x2 (SNoCut (binunion {add_SNo x3 x1|x3 ∈ SNoL x0} (prim5 (SNoL x1) (add_SNo x0))) (binunion {...|x3 ∈ SNoR ...} ...)).
...
■