| pf |
|---|
Apply mul_nat_SR with u5, u3, λ x0 x1 . x1 = u20 leaving 2 subgoals.
The subproof is completed by applying nat_3.
Apply mul_nat_SR with u5, u2, λ x0 x1 . add_nat u5 x1 = u20 leaving 2 subgoals.
The subproof is completed by applying nat_2.
Apply mul_nat_com with u5, u2, λ x0 x1 . add_nat u5 (add_nat u5 x1) = u20 leaving 3 subgoals.
The subproof is completed by applying nat_5.
The subproof is completed by applying nat_2.
Apply unknownprop_463ff37e0f5b1f0c9f9e5bd24ebf02eb01188a79277f3c1f714af19504beaaf2 with u5, λ x0 x1 . add_nat u5 (add_nat u5 x1) = u20 leaving 2 subgoals.
The subproof is completed by applying nat_5.
Apply unknownprop_b16b8ddc32d5fc23481ba2f31c61c76c3a79b038dbad216e5323fff084cd3179 with λ x0 x1 . add_nat u5 (add_nat u5 x1) = u20.
Apply unknownprop_a1a90410c1f7a71f7d8f787285d01a9a8ef9f6791ae58e1afd4fbb66c81ce5cd with λ x0 x1 . add_nat u5 x1 = u20.
The subproof is completed by applying unknownprop_f861a301470f23b9d5d06eb1b63de4c2f6123eb7b7ddb7f8ac60ef985e76d12d.
■ |
|