Let x and y be given.
We prove the intermediate
claim IHLx:
∀w ∈ SNoL x, w + y = y + w.
Let w be given.
Apply SNoL_E x Hx w Hw to the current goal.
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2.
An exact proof term for the current goal is IHx w Lw.
We prove the intermediate
claim IHRx:
∀w ∈ SNoR x, w + y = y + w.
Let w be given.
Apply SNoR_E x Hx w Hw to the current goal.
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2.
An exact proof term for the current goal is IHx w Lw.
We prove the intermediate
claim IHLy:
∀w ∈ SNoL y, x + w = w + x.
Let w be given.
Apply SNoL_E y Hy w Hw to the current goal.
An
exact proof term for the current goal is
SNoS_I2 w y Hw1 Hy Hw2.
An exact proof term for the current goal is IHy w Lw.
We prove the intermediate
claim IHRy:
∀w ∈ SNoR y, x + w = w + x.
Let w be given.
Apply SNoR_E y Hy w Hw to the current goal.
An
exact proof term for the current goal is
SNoS_I2 w y Hw1 Hy Hw2.
An exact proof term for the current goal is IHy w Lw.
We will
prove x + y = y + x.
rewrite the current goal using
add_SNo_eq x Hx y Hy (from left to right).
We will
prove (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2)) = y + x.
rewrite the current goal using
add_SNo_eq y Hy x Hx (from left to right).
We will
prove (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2)) = (SNoCut (Lyx1 ∪ Lyx2) (Ryx1 ∪ Ryx2)).
We prove the intermediate
claim Lxy1yx2:
Lxy1 = Lyx2.
Let w be given.
We will
prove w + y = y + w.
An exact proof term for the current goal is IHLx w Hw.
We prove the intermediate
claim Lxy2yx1:
Lxy2 = Lyx1.
Let w be given.
We will
prove x + w = w + x.
An exact proof term for the current goal is IHLy w Hw.
We prove the intermediate
claim Rxy1yx2:
Rxy1 = Ryx2.
Let w be given.
We will
prove w + y = y + w.
An exact proof term for the current goal is IHRx w Hw.
We prove the intermediate
claim Rxy2yx1:
Rxy2 = Ryx1.
Let w be given.
We will
prove x + w = w + x.
An exact proof term for the current goal is IHRy w Hw.
rewrite the current goal using Lxy1yx2 (from left to right).
rewrite the current goal using Lxy2yx1 (from left to right).
rewrite the current goal using Rxy1yx2 (from left to right).
rewrite the current goal using Rxy2yx1 (from left to right).
We will
prove (SNoCut (Lyx2 ∪ Lyx1) (Ryx2 ∪ Ryx1)) = (SNoCut (Lyx1 ∪ Lyx2) (Ryx1 ∪ Ryx2)).
rewrite the current goal using
binunion_com Lyx2 Lyx1 (from left to right).
rewrite the current goal using
binunion_com Ryx2 Ryx1 (from left to right).
Use reflexivity.
∎