Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
set y4 to be ...
set y5 to be ...
Claim L12: ∀ x6 : ι → ο . x6 y5 ⟶ x6 y4
Let x6 of type ι → ο be given.
Apply add_SNo_minus_SNo_rinv with
x2,
λ x7 x8 . x3 = add_SNo x8 (add_SNo (mul_SNo 2 x3) (minus_SNo x3)),
λ x7 . x6 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply add_SNo_0L with
add_SNo (mul_SNo 2 x3) (minus_SNo x3),
λ x7 x8 . x3 = x8 leaving 2 subgoals.
The subproof is completed by applying L11.
Apply add_SNo_cancel_R with
x3,
x3,
add_SNo (mul_SNo 2 x3) (minus_SNo x3) leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
The subproof is completed by applying L11.
Apply add_SNo_assoc with
mul_SNo 2 x3,
minus_SNo x3,
x3,
λ x7 x8 . add_SNo x3 x3 = x7 leaving 4 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying L8.
The subproof is completed by applying H1.
Apply add_SNo_minus_SNo_linv with
x3,
λ x7 x8 . add_SNo x3 x3 = add_SNo (mul_SNo 2 x3) x8 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply add_SNo_0R with
mul_SNo 2 x3,
λ x7 x8 . add_SNo x3 x3 = x8 leaving 2 subgoals.
The subproof is completed by applying L9.
Let x7 of type ι → ι → ο be given.
Apply unknownprop_e5d031cf873471b22fe77dee36ebb6254dbd5df83fe741afd4ca8450323be464 with
...,
....
Let x6 of type ι → ι → ο be given.
Apply L12 with
λ x7 . x6 x7 y5 ⟶ x6 y5 x7.
Assume H13: x6 y5 y5.
The subproof is completed by applying H13.
Apply andI with
x1 = add_SNo x3 (minus_SNo x2),
x0 = add_SNo (mul_SNo 2 x2) (minus_SNo x3) leaving 2 subgoals.
The subproof is completed by applying L12.
Apply H4 with
λ x4 x5 . x0 = add_SNo (mul_SNo 2 x4) (minus_SNo x3).
Apply H5 with
λ x4 x5 . x0 = add_SNo (mul_SNo 2 (add_SNo x0 x1)) (minus_SNo x4).
Apply mul_SNo_distrL with
2,
x0,
x1,
λ x4 x5 . x0 = add_SNo x5 (minus_SNo (add_SNo x0 (mul_SNo 2 x1))) leaving 4 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply minus_add_SNo_distr with
x0,
mul_SNo 2 x1,
λ x4 x5 . x0 = add_SNo (add_SNo (mul_SNo 2 x0) (mul_SNo 2 x1)) x5 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L9.
Apply add_SNo_com_4_inner_mid with
mul_SNo 2 x0,
mul_SNo 2 x1,
minus_SNo x0,
minus_SNo (mul_SNo 2 x1),
λ x4 x5 . x0 = x5 leaving 5 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L9.
The subproof is completed by applying L6.
The subproof is completed by applying L10.
Apply add_SNo_minus_SNo_rinv with
mul_SNo 2 x1,
λ x4 x5 . x0 = add_SNo (add_SNo (mul_SNo 2 x0) (minus_SNo x0)) x5 leaving 2 subgoals.
The subproof is completed by applying L9.
Apply add_SNo_0R with
add_SNo (mul_SNo 2 x0) (minus_SNo x0),
λ x4 x5 . x0 = x5 leaving 2 subgoals.
Apply SNo_add_SNo with
mul_SNo 2 x0,
minus_SNo x0 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L6.
Apply add_SNo_cancel_R with
x0,
x0,
add_SNo (mul_SNo 2 x0) (minus_SNo x0) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
Apply SNo_add_SNo with
mul_SNo 2 x0,
minus_SNo x0 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L6.
Apply add_SNo_minus_R2' with
mul_SNo 2 x0,
x0,
λ x4 x5 . add_SNo x0 x0 = x5 leaving 3 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying H0.
Let x4 of type ι → ι → ο be given.
Apply unknownprop_e5d031cf873471b22fe77dee36ebb6254dbd5df83fe741afd4ca8450323be464 with
x0,
λ x5 x6 . x4 x6 x5.
The subproof is completed by applying H0.