Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: nat_p x1.
Assume H1: nat_p x2.
Assume H2: ∀ x3 . x3 ∈ u20 ⟶ x0 x3 ∈ u12.
Assume H3: ∀ x3 . x3 ∈ u12 ⟶ or (equip {x4 ∈ u20|x0 x4 = x3} u1) (equip {x4 ∈ u20|x0 x4 = x3} u2).
Assume H4: equip {x3 ∈ u12|equip {x4 ∈ u20|x0 x4 = x3} u1} x1.
Assume H5: equip {x3 ∈ u12|equip {x4 ∈ u20|x0 x4 = x3} u2} x2.
Claim L6: add_nat x1 x2 = u12
Apply unknownprop_f10dcd7fbb5d0ac7aa02fb2a6b46a812452e218eb463a09c49ae7c7e43e46aeb with u20, u12, x0, u1, u2, x1, x2 leaving 9 subgoals.
The subproof is completed by applying nat_12.
The subproof is completed by applying nat_1.
The subproof is completed by applying nat_2.
The subproof is completed by applying neq_1_2.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Claim L7: add_nat (mul_nat x1 u1) (mul_nat x2 u2) = u20
Apply unknownprop_619654e445bf94903b3150722e4c33db1f3d60b6501f8ce2ef5b168354da5373 with u20, u12, x0, u1, u2, x1, x2 leaving 10 subgoals.
The subproof is completed by applying unknownprop_07ad204b3b4fc2b51cd8392b0e6a88916124d7f0f3dbf696bec5a683b0ea9dae.
The subproof is completed by applying nat_1.
The subproof is completed by applying nat_2.
The subproof is completed by applying neq_1_2.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply unknownprop_40c2c43e78124d0e22923fdd03fd951892d7b7de789b8ca1d0fd7cf9a886764e with x1, x2 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply add_nat_add_SNo with x1, x2, λ x3 x4 . x3 = u12 leaving 3 subgoals.
Apply nat_p_omega with x1.
The subproof is completed by applying H0.
Apply nat_p_omega with x2.
The subproof is completed by applying H1.
The subproof is completed by applying L6.
Apply mul_SNo_oneR with x1, λ x3 x4 . add_SNo x3 (mul_SNo u2 x2) = u20 leaving 2 subgoals.
Apply nat_p_SNo with x1.
The subproof is completed by applying H0.
Apply mul_SNo_com with u2, x2, λ x3 x4 . add_SNo (mul_SNo x1 1) x4 = u20 leaving 3 subgoals.
Apply nat_p_SNo with u2.
The subproof is completed by applying nat_2.
Apply nat_p_SNo with x2.
The subproof is completed by applying H1.
Apply mul_nat_mul_SNo with x1, u1, λ x3 x4 . add_SNo x3 (mul_SNo x2 u2) = u20 leaving 3 subgoals.
Apply nat_p_omega with x1.
The subproof is completed by applying H0.
Apply nat_p_omega with u1.
The subproof is completed by applying nat_1.
Apply mul_nat_mul_SNo with x2, u2, λ x3 x4 . add_SNo (mul_nat x1 u1) x3 = u20 leaving 3 subgoals.
Apply nat_p_omega with x2.
The subproof is completed by applying H1.
Apply nat_p_omega with u2.
The subproof is completed by applying nat_2.
Apply add_nat_add_SNo with mul_nat x1 u1, mul_nat x2 u2, λ x3 x4 . x3 = u20 leaving 3 subgoals.
Apply nat_p_omega with mul_nat x1 u1.
Apply mul_nat_p with x1, u1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying nat_1.
Apply nat_p_omega with mul_nat x2 u2.
Apply mul_nat_p with x2, u2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying nat_2.
The subproof is completed by applying L7.
■