Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x1 ∈ int.
Let x2 of type ι be given.
Assume H1: x2 ∈ int.
Assume H2: divides_int x0 (add_SNo x1 (minus_SNo x2)).
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Claim L8: mul_SNo (add_SNo x1 (minus_SNo x2)) (add_SNo x1 x2) = add_SNo (mul_SNo x1 x1) (minus_SNo (mul_SNo x2 x2))
Apply mul_SNo_distrR with x1, minus_SNo x2, add_SNo x1 x2, λ x3 x4 . x4 = add_SNo (mul_SNo x1 x1) (minus_SNo (mul_SNo x2 x2)) leaving 4 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L5.
The subproof is completed by applying L7.
Apply mul_SNo_distrL with x1, x1, x2, λ x3 x4 . add_SNo x4 (mul_SNo (minus_SNo x2) (add_SNo x1 x2)) = add_SNo (mul_SNo x1 x1) (minus_SNo (mul_SNo x2 x2)) leaving 4 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Apply mul_SNo_distrL with minus_SNo x2, x1, x2, λ x3 x4 . add_SNo (add_SNo (mul_SNo x1 x1) (mul_SNo x1 x2)) x4 = add_SNo (mul_SNo x1 x1) (minus_SNo (mul_SNo x2 x2)) leaving 4 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Apply add_SNo_com with mul_SNo x1 x1, mul_SNo x1 x2, λ x3 x4 . add_SNo x4 (add_SNo (mul_SNo (minus_SNo x2) x1) (mul_SNo (minus_SNo x2) x2)) = add_SNo (mul_SNo x1 x1) (minus_SNo (mul_SNo x2 x2)) leaving 3 subgoals.
Apply SNo_mul_SNo with x1, x1 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L3.
Apply SNo_mul_SNo with x1, x2 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Apply add_SNo_com_4_inner_mid with mul_SNo x1 x2, mul_SNo x1 x1, mul_SNo (minus_SNo x2) x1, mul_SNo (minus_SNo x2) x2, λ x3 x4 . x4 = add_SNo (mul_SNo x1 x1) (minus_SNo (mul_SNo x2 x2)) leaving 5 subgoals.
Apply SNo_mul_SNo with x1, x2 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Apply SNo_mul_SNo with x1, x1 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L3.
Apply SNo_mul_SNo with minus_SNo x2, x1 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L3.
Apply SNo_mul_SNo with minus_SNo x2, x2 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L4.
Apply mul_SNo_minus_distrL with x2, x1, λ x3 x4 . add_SNo (add_SNo (mul_SNo x1 x2) x4) (add_SNo (mul_SNo x1 x1) (mul_SNo (minus_SNo x2) x2)) = add_SNo (mul_SNo x1 x1) (minus_SNo (mul_SNo x2 x2)) leaving 3 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L3.
Apply mul_SNo_com with x1, x2, λ x3 x4 . add_SNo (add_SNo x4 (minus_SNo (mul_SNo x2 x1))) (add_SNo (mul_SNo x1 x1) (mul_SNo (minus_SNo x2) x2)) = add_SNo (mul_SNo x1 x1) (minus_SNo (mul_SNo x2 x2)) leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Apply add_SNo_minus_SNo_rinv with mul_SNo x2 x1, λ x3 x4 . add_SNo x4 (add_SNo (mul_SNo x1 x1) (mul_SNo (minus_SNo x2) x2)) = add_SNo (mul_SNo x1 x1) (minus_SNo (mul_SNo x2 x2)) leaving 2 subgoals.
Apply SNo_mul_SNo with x2, x1 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L3.
Apply add_SNo_0L with add_SNo (mul_SNo x1 x1) (mul_SNo (minus_SNo ...) ...), ... leaving 2 subgoals.
...
...
Apply L8 with λ x3 x4 . divides_int x0 x3.
Apply divides_int_mul_SNo_L with x0, add_SNo x1 (minus_SNo x2), add_SNo x1 x2 leaving 2 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying H2.
■