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.
Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with setprod x0 x1, mul_nat x0 x1, λ x2 . add_nat (ap x2 0) (mul_nat (ap x2 1) x0).
Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with setprod x0 x1, mul_nat x0 x1, λ x2 . add_nat (ap x2 0) (mul_nat (ap x2 1) x0) leaving 2 subgoals.
Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with setprod x0 x1, mul_nat x0 x1, λ x2 . add_nat (ap x2 0) (mul_nat (ap x2 1) x0) leaving 2 subgoals.
Let x2 of type ι be given.
Assume H2: In x2 (setprod x0 x1).
Apply unknownprop_93c24336ed9a458e05555de7c7a3407dc357f9415f0c4c32510868a84b67a19c with x0, x1, ap x2 0, ap x2 1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_26337cd699263e77254a7b2e43af09adb0c0b7e817e9fd85214368b3be0c84e7 with x0, x1, x2.
The subproof is completed by applying H2.
Apply unknownprop_0c483673c500001048f0ff6e6fe91698a638688868a14870f05d1f3234619c8f with x0, x1, x2.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Assume H2: In x2 (setprod x0 x1).
Let x3 of type ι be given.
Assume H3: In x3 (setprod x0 x1).
Assume H4: (λ x4 . add_nat (ap x4 0) (mul_nat (ap x4 1) x0)) x2 = (λ x4 . add_nat (ap x4 0) (mul_nat (ap x4 1) x0)) x3.
Claim L5: ...
...
Apply unknownprop_eb1632dc203a2238c00e7d58771c8849d9640f6740a5ca53be1fb0b2479289ef with x0, x1, (λ x4 . add_nat (ap x4 0) (mul_nat (ap x4 1) x0)) x2, x2 = x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying L5.
Let x4 of type ι be given.
Assume H6: In x4 x0.
Let x5 of type ι be given.
Assume H7: In x5 x1.
Assume H8: (λ x6 . add_nat (ap x6 0) (mul_nat (ap x6 1) x0)) x2 = add_nat x4 (mul_nat x5 x0).
Assume H9: ∀ x6 . In x6 x0 ⟶ ∀ x7 . In x7 x1 ⟶ (λ x8 . add_nat (ap x8 0) (mul_nat (ap x8 1) x0)) x2 = add_nat x6 (mul_nat x7 x0) ⟶ and (x6 = x4) (x7 = x5).
Claim L10: ...
...
Claim L11: ...
...
Apply andE with ap x2 0 = x4, ap x2 1 = x5, x2 = x3 leaving 2 subgoals.
The subproof is completed by applying L10.
Assume H12: ap x2 0 = x4.
Assume H13: ap x2 1 = x5.
Apply andE with ap x3 0 = x4, ap x3 1 = x5, x2 = x3 leaving 2 subgoals.
The subproof is completed by applying L11.
Assume H14: ap x3 0 = x4.
Assume H15: ap x3 1 = x5.
Apply unknownprop_25d0316470b9bdc33df1b5827718337aefe32f6ee5207178fa8d15f5c0f986af with x0, x1, x2, λ x6 x7 . x6 = x3 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply H12 with λ x6 x7 . lam 2 (λ x8 . If_i (x8 = 0) x7 (ap x2 1)) = x3.
Apply H13 with λ x6 x7 . lam 2 (λ x8 . If_i (x8 = 0) x4 x7) = x3.
Apply H14 with λ x6 x7 . ... = ....
...
...
■