Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι be given.
Assume H1: ordinal x1.
Claim L2: ...
...
Claim L3: ...
...
Apply add_SNo_eq with x0, x1, λ x2 x3 . x3 = SNoCut (binunion {add_SNo x4 x1|x4 ∈ SNoS_ x0} {add_SNo x0 x4|x4 ∈ SNoS_ x1}) 0 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply ordinal_SNoL with x0, λ x2 x3 . SNoCut (binunion {add_SNo x4 x1|x4 ∈ x3} {add_SNo x0 x4|x4 ∈ SNoL x1}) (binunion {add_SNo x4 x1|x4 ∈ SNoR x0} {add_SNo x0 x4|x4 ∈ SNoR x1}) = SNoCut (binunion {add_SNo x4 x1|x4 ∈ SNoS_ x0} {add_SNo x0 x4|x4 ∈ SNoS_ x1}) 0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply ordinal_SNoL with x1, λ x2 x3 . SNoCut (binunion {add_SNo x4 x1|x4 ∈ SNoS_ x0} {add_SNo x0 x4|x4 ∈ x3}) (binunion {add_SNo x4 x1|x4 ∈ SNoR x0} {add_SNo x0 x4|x4 ∈ SNoR x1}) = SNoCut (binunion {add_SNo x4 x1|x4 ∈ SNoS_ x0} {add_SNo x0 x4|x4 ∈ SNoS_ x1}) 0 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply ordinal_SNoR with x0, λ x2 x3 . SNoCut (binunion {add_SNo x4 x1|x4 ∈ SNoS_ x0} {add_SNo x0 x4|x4 ∈ SNoS_ x1}) (binunion {add_SNo x4 x1|x4 ∈ x3} {add_SNo x0 x4|x4 ∈ SNoR x1}) = SNoCut (binunion {add_SNo x4 x1|x4 ∈ SNoS_ x0} {add_SNo x0 x4|x4 ∈ SNoS_ x1}) 0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply ordinal_SNoR with x1, λ x2 x3 . SNoCut (binunion {add_SNo x4 x1|x4 ∈ SNoS_ x0} {add_SNo x0 x4|x4 ∈ SNoS_ x1}) (binunion {add_SNo x4 x1|x4 ∈ 0} {add_SNo x0 x4|x4 ∈ x3}) = SNoCut (binunion {add_SNo x4 x1|x4 ∈ SNoS_ x0} {add_SNo x0 x4|x4 ∈ SNoS_ x1}) 0 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply Repl_Empty with λ x2 . add_SNo x2 x1, λ x2 x3 . SNoCut (binunion {add_SNo x4 x1|x4 ∈ SNoS_ x0} {add_SNo x0 x4|x4 ∈ SNoS_ x1}) (binunion x3 {add_SNo x0 x4|x4 ∈ 0}) = SNoCut (binunion {add_SNo x4 x1|x4 ∈ SNoS_ x0} {add_SNo x0 x4|x4 ∈ SNoS_ x1}) 0.
Apply Repl_Empty with λ x2 . add_SNo x0 x2, λ x2 x3 . SNoCut (binunion {add_SNo x4 x1|x4 ∈ SNoS_ x0} {add_SNo x0 x4|x4 ∈ SNoS_ x1}) (binunion 0 x3) = SNoCut (binunion {add_SNo ... ...|x4 ∈ SNoS_ x0} ...) 0.
...
■