Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Let x7 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNo x1.

Assume H2: SNo x2.

Assume H3: SNo x3.

Assume H4: SNo x4.

Assume H5: SNo x5.

Assume H6: SNo x6.

Assume H7: SNo x7.

Assume H8: SNoLt (add_SNo x4 (add_SNo x5 (add_SNo x6 x7))) 0.

Assume H9: SNoLe (add_SNo x1 (minus_SNo x0)) x4.

Assume H10: SNoLe (add_SNo x2 (minus_SNo x1)) x5.

Assume H11: SNoLe (add_SNo x3 (minus_SNo x2)) x6.

Assume H12: SNoLe (add_SNo x0 (minus_SNo x3)) x7.

Apply SNoLt_irref with 0.

Apply SNoLeLt_tra with 0, add_SNo x4 (add_SNo x5 (add_SNo x6 x7)), 0 leaving 5 subgoals.

The subproof is completed by applying SNo_0.

Apply SNo_add_SNo_4 with x4, x5, x6, x7 leaving 4 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

The subproof is completed by applying H6.

The subproof is completed by applying H7.

The subproof is completed by applying SNo_0.

Claim L13: ...

...

Apply L13 with λ x8 x9 . SNoLe 0 x9.

Apply SNo_idl_cycle_nonneg with 3, λ x8 . ap (lam 5 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 x0))))) x8, λ x8 . ap (lam 4 (λ x9 . If_i (x9 = 0) x4 (If_i (x9 = 1) x5 (If_i (x9 = 2) x6 x7)))) x8 leaving 5 subgoals.

The subproof is completed by applying nat_3.

Let x8 of type ι be given.

Assume H14: x8 ∈ 4.

Apply cases_4 with x8, λ x9 . SNo ((λ x10 . ap (lam 5 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) x1 (If_i (x11 = 2) x2 (If_i (x11 = 3) x3 x0))))) x10) x9) leaving 5 subgoals.

The subproof is completed by applying H14.

Apply tuple_5_0_eq with x0, x1, x2, x3, x0, λ x9 x10 . SNo x10.

The subproof is completed by applying H0.

Apply tuple_5_1_eq with x0, x1, x2, x3, x0, λ x9 x10 . SNo x10.

The subproof is completed by applying H1.

Apply tuple_5_2_eq with x0, x1, x2, x3, x0, λ x9 x10 . SNo x10.

The subproof is completed by applying H2.

Apply tuple_5_3_eq with x0, x1, x2, x3, x0, λ x9 x10 . SNo x10.

The subproof is completed by applying H3.

Let x8 of type ι be given.

Assume H14: x8 ∈ 4.

Apply cases_4 with x8, λ x9 . SNo ((λ x10 . ap (lam 4 (λ x11 . If_i (x11 = 0) x4 (If_i (x11 = 1) x5 (If_i (x11 = 2) x6 x7)))) x10) x9) leaving 5 subgoals.

The subproof is completed by applying H14.

Apply tuple_4_0_eq with x4, x5, x6, x7, λ x9 x10 . SNo x10.

The subproof is completed by applying H4.

Apply tuple_4_1_eq with x4, x5, x6, x7, λ x9 x10 . SNo x10.

The subproof is completed by applying H5.

Apply tuple_4_2_eq with x4, x5, x6, x7, λ x9 x10 . SNo x10.

The subproof is completed by applying H6.

Apply tuple_4_3_eq with x4, x5, x6, x7, λ x9 x10 . SNo x10.

The subproof is completed by applying H7.

Apply tuple_5_0_eq with x0, x1, x2, x3, x0, λ x8 x9 . ap (lam 5 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i ... ... ...)))) 4 = ....

...

■

Proofgold Proof