Search for blocks/addresses/...

Proofgold Proof

pf
Apply SNoLev_ind3 with λ x0 x1 x2 . add_SNo x0 (add_SNo x1 x2) = add_SNo (add_SNo x0 x1) x2.
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Assume H2: SNo x2.
Assume H3: ∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ (λ x4 x5 x6 . add_SNo x4 (add_SNo x5 x6) = add_SNo (add_SNo x4 x5) x6) x3 x1 x2.
Assume H4: ∀ x3 . x3 ∈ SNoS_ (SNoLev x1) ⟶ (λ x4 x5 x6 . add_SNo x4 (add_SNo x5 x6) = add_SNo (add_SNo x4 x5) x6) x0 x3 x2.
Assume H5: ∀ x3 . x3 ∈ SNoS_ (SNoLev x2) ⟶ (λ x4 x5 x6 . add_SNo x4 (add_SNo x5 x6) = add_SNo (add_SNo x4 x5) x6) x0 x1 x3.
Assume H6: ∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x4 . x4 ∈ SNoS_ (SNoLev x1) ⟶ (λ x5 x6 x7 . add_SNo x5 (add_SNo x6 x7) = add_SNo (add_SNo x5 x6) x7) x3 x4 x2.
Assume H7: ∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x4 . x4 ∈ SNoS_ (SNoLev x2) ⟶ (λ x5 x6 x7 . add_SNo x5 (add_SNo x6 x7) = add_SNo (add_SNo x5 x6) x7) x3 x1 x4.
Assume H8: ∀ x3 . x3 ∈ SNoS_ (SNoLev x1) ⟶ ∀ x4 . x4 ∈ SNoS_ (SNoLev x2) ⟶ (λ x5 x6 x7 . add_SNo x5 (add_SNo x6 x7) = add_SNo (add_SNo x5 x6) x7) x0 x3 x4.
Assume H9: ∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x4 . x4 ∈ SNoS_ (SNoLev x1) ⟶ ∀ x5 . x5 ∈ SNoS_ (SNoLev x2) ⟶ (λ x6 x7 x8 . add_SNo x6 (add_SNo x7 x8) = add_SNo (add_SNo x6 x7) x8) x3 x4 x5.
Claim L10: ...
...
Claim L11: ...
...
Apply add_SNo_eq with x0, add_SNo x1 x2, λ x3 x4 . x4 = add_SNo (add_SNo x0 x1) x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L11.
Apply add_SNo_eq with add_SNo x0 x1, x2, λ x3 x4 . SNoCut (binunion {add_SNo x5 (add_SNo x1 x2)|x5 ∈ SNoL x0} (prim5 (SNoL (add_SNo x1 x2)) (add_SNo x0))) (binunion {add_SNo x5 (add_SNo x1 x2)|x5 ∈ SNoR x0} (prim5 (SNoR (add_SNo x1 x2)) (add_SNo x0))) = x4 leaving 3 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying H2.
Claim L12: ...
...
Claim L13: ...
...
Apply SNoCut_ext with binunion {add_SNo x3 (add_SNo x1 x2)|x3 ∈ SNoL x0} ..., ..., ..., ... leaving 6 subgoals.
...
...
...
...
...
...
■