Let x and y be given.
We prove the intermediate
claim Lxy:
SNo (x + y).
An
exact proof term for the current goal is
SNo_add_SNo x y Hx Hy.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hy.
rewrite the current goal using
add_SNo_eq x Hx y Hy (from left to right).
We prove the intermediate
claim L1:
SNoCutP (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2).
Assume _ _ _.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Let w be given.
rewrite the current goal using Huw (from left to right).
Apply SNoL_E x Hx w Hw to the current goal.
An
exact proof term for the current goal is
SNoL_SNoS_ x w Hw.
An exact proof term for the current goal is Hp w Lw Huw.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Let w be given.
rewrite the current goal using Huw (from left to right).
Apply SNoL_E y Hy w Hw to the current goal.
An
exact proof term for the current goal is
SNoL_SNoS_ y w Hw.
An exact proof term for the current goal is Hp w Lw Huw.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Let w be given.
rewrite the current goal using Huw (from left to right).
Apply SNoR_E x Hx w Hw to the current goal.
An
exact proof term for the current goal is
SNoR_SNoS_ x w Hw.
An exact proof term for the current goal is Hp w Lw Huw.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Let w be given.
rewrite the current goal using Huw (from left to right).
Apply SNoR_E y Hy w Hw to the current goal.
An
exact proof term for the current goal is
SNoR_SNoS_ y w Hw.
An exact proof term for the current goal is Hp w Lw Huw.
We prove the intermediate
claim Lxy1E2:
∀u ∈ Lxy1, SNo u.
Let u be given.
Assume Hu.
Apply Lxy1E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5.
We will
prove SNo (w + y).
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hy.
We prove the intermediate
claim Lxy2E2:
∀u ∈ Lxy2, SNo u.
Let u be given.
Assume Hu.
Apply Lxy2E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5.
We will
prove SNo (x + w).
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hw3.
We prove the intermediate
claim Rxy1E2:
∀u ∈ Rxy1, SNo u.
Let u be given.
Assume Hu.
Apply Rxy1E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5.
We will
prove SNo (w + y).
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hy.
We prove the intermediate
claim Rxy2E2:
∀u ∈ Rxy2, SNo u.
Let u be given.
Assume Hu.
Apply Rxy2E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5.
We will
prove SNo (x + w).
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hw3.
Let u be given.
Apply binunionE Lxy1 Lxy2 u Hu to the current goal.
Assume Hu.
An exact proof term for the current goal is Lxy1E2 u Hu.
Assume Hu.
An exact proof term for the current goal is Lxy2E2 u Hu.
Let u be given.
Apply binunionE Rxy1 Rxy2 u Hu to the current goal.
Assume Hu.
An exact proof term for the current goal is Rxy1E2 u Hu.
Assume Hu.
An exact proof term for the current goal is Rxy2E2 u Hu.
Apply L2 to the current goal.
Assume H _.
An exact proof term for the current goal is H.
An exact proof term for the current goal is H2.
Let v be given.
Let u be given.
Apply binunionE Lxy1 Lxy2 u Hu to the current goal.
Apply Lxy1E u Hu to the current goal.
Let w be given.
We prove the intermediate
claim Lv:
ordinal v.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw6.
An exact proof term for the current goal is H1.
Apply IH1 to the current goal.
An exact proof term for the current goal is Hw1.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw4.
Apply LLxLy to the current goal.
Assume H _.
An
exact proof term for the current goal is
H (SNoLev w + SNoLev y) L4a.
We prove the intermediate
claim L4c:
v ⊆ SNoLev (w + y).
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H2.
Apply LIHw to the current goal.
Apply L4c to the current goal.
Apply H1 to the current goal.
An exact proof term for the current goal is L4a.
Apply Lxy2E u Hu to the current goal.
Let w be given.
We prove the intermediate
claim Lv:
ordinal v.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hw6.
An exact proof term for the current goal is H1.
Apply IH2 to the current goal.
An exact proof term for the current goal is Hw1.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw4.
Apply LLxLy to the current goal.
Assume H _.
An
exact proof term for the current goal is
H (SNoLev x + SNoLev w) L4a.
We prove the intermediate
claim L4c:
v ⊆ SNoLev (x + w).
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H2.
Apply LIHw to the current goal.
Apply L4c to the current goal.
Apply H1 to the current goal.
An exact proof term for the current goal is L4a.
Let v be given.
Let u be given.
Apply binunionE Rxy1 Rxy2 u Hu to the current goal.
Apply Rxy1E u Hu to the current goal.
Let w be given.
We prove the intermediate
claim Lv:
ordinal v.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw6.
An exact proof term for the current goal is H1.
Apply IH1 to the current goal.
An exact proof term for the current goal is Hw1.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw4.
Apply LLxLy to the current goal.
Assume H _.
An
exact proof term for the current goal is
H (SNoLev w + SNoLev y) L4a.
We prove the intermediate
claim L4c:
v ⊆ SNoLev (w + y).
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H2.
Apply LIHw to the current goal.
Apply L4c to the current goal.
Apply H1 to the current goal.
An exact proof term for the current goal is L4a.
Apply Rxy2E u Hu to the current goal.
Let w be given.
We prove the intermediate
claim Lv:
ordinal v.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hw6.
An exact proof term for the current goal is H1.
Apply IH2 to the current goal.
An exact proof term for the current goal is Hw1.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw4.
Apply LLxLy to the current goal.
Assume H _.
An
exact proof term for the current goal is
H (SNoLev x + SNoLev w) L4a.
We prove the intermediate
claim L4c:
v ⊆ SNoLev (x + w).
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H2.
Apply LIHw to the current goal.
Apply L4c to the current goal.
Apply H1 to the current goal.
An exact proof term for the current goal is L4a.
∎