Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H1: even_nat x1.
Assume H2: even_nat x2.
Assume H3: even_nat x3.
Assume H4: odd_nat x4.
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))).
Apply even_nat_not_odd_nat with 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))) leaving 2 subgoals.
Apply H5 with λ x5 x6 . even_nat x5.
Apply even_nat_2x with x0.
Apply nat_p_omega with x0.
The subproof is completed by applying H0.
Apply unknownprop_eb94885c32cd12e81f83ccb7ba570bbc0dad23181f98524f12836a62517814c9 with (λ 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)) leaving 2 subgoals.
Apply unknownprop_d15c8fe3790d38a2c5c4fcf918bf86438c7693aae8649d50aac4b80bc517da5f with x1.
The subproof is completed by applying H1.
Apply unknownprop_eb94885c32cd12e81f83ccb7ba570bbc0dad23181f98524f12836a62517814c9 with (λ x5 . mul_SNo x5 x5) x2, add_SNo ((λ x5 . mul_SNo x5 x5) x3) ((λ x5 . mul_SNo x5 x5) x4) leaving 2 subgoals.
Apply unknownprop_d15c8fe3790d38a2c5c4fcf918bf86438c7693aae8649d50aac4b80bc517da5f with x2.
The subproof is completed by applying H2.
Apply unknownprop_eb94885c32cd12e81f83ccb7ba570bbc0dad23181f98524f12836a62517814c9 with (λ x5 . mul_SNo x5 x5) x3, (λ x5 . mul_SNo x5 x5) x4 leaving 2 subgoals.
Apply unknownprop_d15c8fe3790d38a2c5c4fcf918bf86438c7693aae8649d50aac4b80bc517da5f with x3.
The subproof is completed by applying H3.
Apply unknownprop_4ac09f490c7c01c72dab0c22b9909ba5dc5a9a068881dbdcb9a856aafed3adf1 with x4.
The subproof is completed by applying H4.
■