Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: nat_p x0.
Assume H1: nat_p x1.
Let x2 of type ι be given.
Assume H2: In x2 x0.
Let x3 of type ι be given.
Assume H3: In x3 x1.
Apply unknownprop_848c2653fe5dd0e3543ddb9ea13019248651d179f1aa533a232a0f3f6ad0ef06 with x1, x3, λ x4 . In (add_nat x2 (mul_nat x3 x0)) (mul_nat x0 x4) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Let x4 of type ι be given.
Assume H4: nat_p x4.
Assume H5: x1 = ordsucc x4.
Apply unknownprop_3defe724d02ba276d9730f9f5a87e86e6bc0e48da350a99bdaaf13f339867dcf with x0, x4, λ x5 x6 . In (add_nat x2 (mul_nat x3 x0)) x6 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_dd5df7669a233e3d5e134397e0a0943dece6dcd81d988e2d3c963c02c7bcf901 with x0, x4, λ x5 x6 . In (add_nat x2 (mul_nat x3 x0)) (add_nat x0 x6) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Claim L6: nat_p x3
Apply unknownprop_3069c6fa8dbd033f1c94555c93d580ac5c2fd979807cb20dbdb8dc4cc9b1517f with x1, x3 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Claim L7: In x3 (ordsucc x4)
Apply H5 with λ x5 x6 . In x3 x5.
The subproof is completed by applying H3.
Claim L8: Subq (mul_nat x3 x0) (mul_nat x4 x0)
Apply unknownprop_f30a739e8afbcceddcf7416407d2fb53c7a0b07746a8e26223dddaa1c90261dd with x3, x4, x0 leaving 4 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying H4.
Apply unknownprop_84fe37a922385756a4e0826a593defb788cadbe4bdc9a7fe6b519ea49f509df5 with x4, x3, Subq x3 x4 leaving 3 subgoals.
The subproof is completed by applying L7.
Assume H8: In x3 x4.
Apply unknownprop_92b4103b83752522eb6c235601eefa2912e3f6395a346e3a7eb52bb5e37ede81 with x4, x3 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
Assume H8: x3 = x4.
Apply H8 with λ x5 x6 . Subq x6 x4.
The subproof is completed by applying unknownprop_d889823a5c975ad2d68f484964233a1e69e7d67f0888aa5b83d962eeca107acd with x4.
The subproof is completed by applying H0.
Claim L9: Subq (add_nat x0 (mul_nat x3 x0)) (add_nat x0 (mul_nat x4 x0))
Apply unknownprop_ced5c14ac643c8a50a5e307d612d5bf57f5a5f18e947e825398ee5fec940398b with x0, mul_nat x3 x0, mul_nat x4 x0 leaving 4 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_0b229518762ed7010020950c24a2d0fe47c44c7a7b255cdddc862baf12395763 with x3, x0 leaving 2 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying H0.
Apply unknownprop_0b229518762ed7010020950c24a2d0fe47c44c7a7b255cdddc862baf12395763 with x4, x0 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H0.
The subproof is completed by applying L8.
Claim L10: In (add_nat x2 (mul_nat x3 x0)) (add_nat x0 (mul_nat x3 x0))
Apply unknownprop_4091ebd6d94cd2a61820d5e9e5b329a35ceeb943e078c5c25a4c8d631106573d with x0, x2, mul_nat x3 x0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_0b229518762ed7010020950c24a2d0fe47c44c7a7b255cdddc862baf12395763 with x3, x0 leaving 2 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying H0.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with add_nat x0 (mul_nat x3 x0), add_nat x0 (mul_nat x4 x0), add_nat x2 (mul_nat x3 x0) leaving 2 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying L10.
■