| pf |
|---|
Apply mul_nat_SR with u5, u4, λ x0 x1 . x1 = u25 leaving 2 subgoals.
The subproof is completed by applying nat_4.
Apply mul_nat_SR with u5, u3, λ x0 x1 . add_nat u5 x1 = u25 leaving 2 subgoals.
The subproof is completed by applying nat_3.
Apply mul_nat_SR with u5, u2, λ x0 x1 . add_nat u5 (add_nat u5 x1) = u25 leaving 2 subgoals.
The subproof is completed by applying nat_2.
Apply mul_nat_SR with u5, u1, λ x0 x1 . add_nat u5 (add_nat u5 (add_nat u5 x1)) = u25 leaving 2 subgoals.
The subproof is completed by applying nat_1.
Apply mul_nat_1R with u5, λ x0 x1 . add_nat u5 (add_nat u5 (add_nat u5 (add_nat u5 x1))) = u25.
Apply unknownprop_566d903739470afda40d64020ac73735d543ec3209342e2b92a42fa9f217751d with λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 x1)))), λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 x1)))), λ x0 x1 . add_nat u5 (add_nat u5 (add_nat u5 x0)) = u25 leaving 3 subgoals.
The subproof is completed by applying unknownprop_d5dbeec732ea01f927877e2420b51cb5c68f473bf98d93e8571ddfd3f7adea18.
The subproof is completed by applying unknownprop_d5dbeec732ea01f927877e2420b51cb5c68f473bf98d93e8571ddfd3f7adea18.
Apply unknownprop_566d903739470afda40d64020ac73735d543ec3209342e2b92a42fa9f217751d with λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 x1)))), λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))))), λ x0 x1 . add_nat u5 (add_nat u5 x0) = u25 leaving 3 subgoals.
The subproof is completed by applying unknownprop_d5dbeec732ea01f927877e2420b51cb5c68f473bf98d93e8571ddfd3f7adea18.
The subproof is completed by applying unknownprop_127246c57adc93f5032e352a4463561387a9b3b9f04766e1c57313b7a93b14ff.
Apply unknownprop_566d903739470afda40d64020ac73735d543ec3209342e2b92a42fa9f217751d with λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 x1)))), λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))))), λ x0 x1 . add_nat u5 x0 = u25 leaving 3 subgoals.
The subproof is completed by applying unknownprop_d5dbeec732ea01f927877e2420b51cb5c68f473bf98d93e8571ddfd3f7adea18.
The subproof is completed by applying unknownprop_b69aeea3b10b846ee5e419c1b471f03ef85ead2b77c13f4aa8b04c94af6c6775.
Let x0 of type ι → ι → ο be given.
Apply unknownprop_566d903739470afda40d64020ac73735d543ec3209342e2b92a42fa9f217751d with λ x1 : ι → ι . λ x2 . x1 (x1 (x1 (x1 (x1 x2)))), λ x1 : ι → ι . λ x2 . x1 (x1 (x1 (x1 (x1 (x1 (x1 (x1 (x1 (x1 (x1 (x1 (x1 (x1 (x1 (x1 (x1 (x1 (x1 (x1 x2))))))))))))))))))), λ x1 x2 . x0 x2 x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_d5dbeec732ea01f927877e2420b51cb5c68f473bf98d93e8571ddfd3f7adea18.
The subproof is completed by applying unknownprop_44091bde3786efbd683bdef95eb60f243ec6edb4d9a52a061406d636da2c7f68.
■ |
|