Search for blocks/addresses/...

Proofgold Proof

pf
Apply nat_ind with λ x0 . ∀ x1 . nat_p x1 ⟶ mul_nat x0 x1 = 0 ⟶ or (x0 = 0) (x1 = 0) leaving 2 subgoals.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: mul_nat 0 x0 = 0.
Apply orIL with 0 = 0, x0 = 0.
Let x1 of type ι → ι → ο be given.
Assume H2: x1 0 0.
The subproof is completed by applying H2.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: ∀ x1 . nat_p x1 ⟶ mul_nat x0 x1 = 0 ⟶ or (x0 = 0) (x1 = 0).
Let x1 of type ι be given.
Assume H2: nat_p x1.
Apply mul_nat_SL with x0, x1, λ x2 x3 . x3 = 0 ⟶ or (ordsucc x0 = 0) (x1 = 0) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Assume H3: add_nat (mul_nat x0 x1) x1 = 0.
Apply orIR with ordsucc x0 = 0, x1 = 0.
Apply unknownprop_45596e78bba24517552f5da1105935f815723d1d00ef823b7fc87048c29f6c84 with mul_nat x0 x1, x1, x1 = 0 leaving 4 subgoals.
Apply mul_nat_p with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Assume H4: mul_nat x0 x1 = 0.
Assume H5: x1 = 0.
The subproof is completed by applying H5.
■