Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Let x1 of type ι be given.
Assume H1: x1 ∈ omega.
Let x2 of type ι be given.
Assume H2: x2 ∈ omega.
Let x3 of type ι be given.
Assume H3: x3 ∈ omega.
Let x4 of type ι be given.
Assume H4: x4 ∈ omega.
Assume H5: mul_SNo 2 x0 = add_SNo ((λ x5 . mul_SNo x5 x5) x1) (add_SNo ((λ x5 . mul_SNo x5 x5) x2) (add_SNo ((λ x5 . mul_SNo x5 x5) x3) ((λ x5 . mul_SNo x5 x5) x4))).
Let x5 of type ο be given.
Assume H6: ∀ x6 . x6 ∈ omega ⟶ ∀ x7 . x7 ∈ omega ⟶ ∀ x8 . x8 ∈ omega ⟶ ∀ x9 . x9 ∈ omega ⟶ x0 = add_SNo ((λ x10 . mul_SNo x10 x10) x6) (add_SNo ((λ x10 . mul_SNo x10 x10) x7) (add_SNo ((λ x10 . mul_SNo x10 x10) x8) ((λ x10 . mul_SNo x10 x10) x9))) ⟶ x5.
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Claim L13: ...
...
Claim L14: ...
...
Claim L15: ...
...
Claim L16: ...
...
Apply even_nat_or_odd_nat with x1, x5 leaving 3 subgoals.
Apply omega_nat_p with x1.
The subproof is completed by applying H1.
Assume H17: even_nat x1.
Apply even_nat_or_odd_nat with x2, x5 leaving 3 subgoals.
Apply omega_nat_p with x2.
The subproof is completed by applying H2.
Assume H18: even_nat x2.
Apply even_nat_or_odd_nat with x3, x5 leaving 3 subgoals.
The subproof is completed by applying L7.
Assume H19: even_nat x3.
Apply even_nat_or_odd_nat with x4, x5 leaving 3 subgoals.
The subproof is completed by applying L8.
Assume H20: even_nat x4.
Apply unknownprop_28ef4a29aab7f65f5e756b07f4566632a9f4d0e0caf7e4886d17fa81153ec666 with x0, x1, x2, x3, x4, x5 leaving 7 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H17.
The subproof is completed by applying H18.
The subproof is completed by applying H19.
The subproof is completed by applying H20.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Assume H20: odd_nat x4.
Apply FalseE with x5.
Apply unknownprop_a6bd07609511a03f53c525f75c06c05dd78fc761a44980055ae84b1f2a63cbad with x0, x1, x2, x3, x4 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H17.
The subproof is completed by applying H18.
The subproof is completed by applying H19.
The subproof is completed by applying H20.
The subproof is completed by applying H5.
Assume H19: odd_nat x3.
Apply even_nat_or_odd_nat with x4, x5 leaving 3 subgoals.
The subproof is completed by applying L8.
Assume H20: even_nat x4.
Apply FalseE with x5.
Apply unknownprop_a6bd07609511a03f53c525f75c06c05dd78fc761a44980055ae84b1f2a63cbad with x0, x1, x2, x4, x3 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H17.
The subproof is completed by applying H18.
The subproof is completed by applying H20.
The subproof is completed by applying H19.
Apply add_SNo_com with (λ x6 . mul_SNo x6 x6) x4, (λ x6 . mul_SNo x6 x6) x3, λ x6 x7 . mul_SNo 2 x0 = add_SNo ((λ x8 . mul_SNo x8 x8) x1) (add_SNo ((λ x8 . mul_SNo x8 x8) x2) x7) leaving 3 subgoals.
Apply L13 with x4.
The subproof is completed by applying L12.
Apply L13 with x3.
The subproof is completed by applying L11.
The subproof is completed by applying H5.
Assume H20: odd_nat x4.
Apply unknownprop_951d00d741b7abf7c66e67829a46882dfb5c88e67b6c4dc8becb105826e54154 with x0, x1, x2, x3, x4, x5 leaving 7 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H17.
The subproof is completed by applying H18.
The subproof is completed by applying H19.
The subproof is completed by applying H20.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Assume H18: odd_nat x2.
Apply even_nat_or_odd_nat with x3, x5 leaving 3 subgoals.
The subproof is completed by applying L7.
Assume H19: even_nat x3.
Apply even_nat_or_odd_nat with x4, x5 leaving 3 subgoals.
The subproof is completed by applying L8.
Assume H20: even_nat x4.
Apply FalseE with x5.
Apply unknownprop_a6bd07609511a03f53c525f75c06c05dd78fc761a44980055ae84b1f2a63cbad with x0, x1, x3, x4, x2 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H17.
The subproof is completed by applying H19.
The subproof is completed by applying H20.
The subproof is completed by applying H18.
Apply add_SNo_rotate_3_1 with (λ x6 . mul_SNo x6 x6) x3, (λ x6 . mul_SNo x6 x6) x4, (λ x6 . mul_SNo x6 x6) x2, λ x6 x7 . mul_SNo 2 x0 = add_SNo ((λ x8 . mul_SNo x8 x8) x1) x7 leaving 4 subgoals.
Apply L13 with x3.
The subproof is completed by applying L11.
Apply L13 with x4.
The subproof is completed by applying L12.
Apply L13 with x2.
The subproof is completed by applying L10.
The subproof is completed by applying H5.
Assume H20: odd_nat x4.
Apply unknownprop_951d00d741b7abf7c66e67829a46882dfb5c88e67b6c4dc8becb105826e54154 with x0, x1, x3, x2, x4, x5 leaving 7 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H17.
The subproof is completed by applying H19.
The subproof is completed by applying H18.
The subproof is completed by applying H20.
Apply add_SNo_com_3_0_1 with (λ x6 . mul_SNo x6 x6) x2, (λ x6 . mul_SNo x6 x6) x3, (λ x6 . mul_SNo x6 x6) x4, λ x6 x7 . mul_SNo 2 ... = ... leaving 4 subgoals.
...
...
...
...
...
...
...
■