Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_b35032c81ea06ad673f8a0490d5be4e7b984453ec9378fed4adde429c2b88d75 with λ x0 . ∀ x1 . nat_p x1mul_nat x1 x0 = x1(x1 = 0∀ x2 : ο . x2)x0 = 1 leaving 3 subgoals.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Apply mul_nat_0R with x0, λ x1 x2 . x2 = x0(x0 = 0∀ x3 : ο . x3)0 = 1.
Assume H1: 0 = x0.
Assume H2: x0 = 0∀ x1 : ο . x1.
Apply FalseE with 0 = 1.
Apply H2.
Let x1 of type ιιο be given.
The subproof is completed by applying H1 with λ x2 x3 . x1 x3 x2.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: mul_nat x0 1 = x0.
Assume H2: x0 = 0∀ x1 : ο . x1.
Let x1 of type ιιο be given.
Assume H3: x1 1 1.
The subproof is completed by applying H3.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Let x1 of type ι be given.
Assume H1: nat_p x1.
Apply mul_nat_SR with x1, ordsucc x0, λ x2 x3 . x3 = x1(x1 = 0∀ x4 : ο . x4)ordsucc (ordsucc x0) = 1 leaving 2 subgoals.
Apply nat_ordsucc with x0.
The subproof is completed by applying H0.
Apply mul_nat_SR with x1, x0, λ x2 x3 . add_nat x1 x3 = x1(x1 = 0∀ x4 : ο . x4)ordsucc (ordsucc x0) = 1 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H2: add_nat x1 (add_nat x1 (mul_nat x1 x0)) = x1.
Assume H3: x1 = 0∀ x2 : ο . x2.
Apply FalseE with ordsucc (ordsucc x0) = 1.
Claim L4: add_nat (add_nat x1 (mul_nat x1 x0)) x1 = x1
Apply add_nat_com with add_nat x1 (mul_nat x1 x0), x1, λ x2 x3 . x3 = x1 leaving 3 subgoals.
Apply add_nat_p with x1, mul_nat x1 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply mul_nat_p with x1, x0 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Claim L5: add_nat x1 (mul_nat x1 x0) = 0
Apply unknownprop_986be96dc315caaba0467a55e70dc4d242dfd7d790ce55390e38a5d935288972 with add_nat x1 (mul_nat x1 x0), x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L4.
Apply unknownprop_6983d26e930e4f29d8bfcdef860e7bdda90fb8cfa66e4db9cfa2a0c77f2e095e with x1, mul_nat x1 x0, False leaving 3 subgoals.
Apply mul_nat_p with x1, x0 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying L5.
Assume H6: x1 = 0.
Apply FalseE with mul_nat x1 x0 = 0False.
Apply H3.
The subproof is completed by applying H6.