Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H1: even_nat x1.
Assume H2: even_nat x2.
Assume H3: even_nat x3.
Assume H4: even_nat x4.
Assume H5: SNoLe x1 x2.
Assume H6: SNoLe x3 x4.
Assume H7: mul_SNo 2 x0 = add_SNo ((λ x5 . mul_SNo x5 x5) x1) (add_SNo ((λ x5 . mul_SNo x5 x5) x2) (add_SNo ((λ x5 . mul_SNo x5 x5) x3) ((λ x5 . mul_SNo x5 x5) x4))).
Let x5 of type ο be given.
Assume H8: ∀ x6 . x6 ∈ omega ⟶ ∀ x7 . x7 ∈ omega ⟶ ∀ x8 . x8 ∈ omega ⟶ ∀ x9 . x9 ∈ omega ⟶ x0 = add_SNo ((λ x10 . mul_SNo x10 x10) x6) (add_SNo ((λ x10 . mul_SNo x10 x10) x7) (add_SNo ((λ x10 . mul_SNo x10 x10) x8) ((λ x10 . mul_SNo x10 x10) x9))) ⟶ x5.
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Claim L13: ...
...
Apply unknownprop_0b973640ded967ccca7ae90b9a0ad1cbab8b72d7d8e77d5564f2ebb33a0b2952 with x2, x1, x5 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Assume H14: add_SNo x2 x1 ∈ omega.
Assume H15: ∃ x6 . and (x6 ∈ omega) (add_SNo x2 x1 = mul_nat 2 x6).
Apply H15 with x5.
Let x6 of type ι be given.
Assume H16: (λ x7 . and (x7 ∈ omega) (add_SNo x2 x1 = mul_nat 2 x7)) x6.
Apply H16 with x5.
Assume H17: x6 ∈ omega.
Apply mul_nat_mul_SNo with 2, x6, λ x7 x8 . add_SNo x2 x1 = x8 ⟶ x5 leaving 3 subgoals.
Apply nat_p_omega with 2.
The subproof is completed by applying nat_2.
The subproof is completed by applying H17.
Assume H18: add_SNo x2 x1 = mul_SNo 2 x6.
Apply unknownprop_b904ca8f031fe3500fb61ac5d204ed355ea35cee98fb2afe49bf33c64a4c7f22 with x1, x2, x5 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H5.
Assume H19: add_SNo x2 (minus_SNo x1) ∈ omega.
Assume H20: ∃ x7 . and (x7 ∈ omega) (add_SNo x2 (minus_SNo x1) = mul_nat 2 x7).
Apply H20 with x5.
Let x7 of type ι be given.
Assume H21: (λ x8 . and (x8 ∈ omega) (add_SNo x2 (minus_SNo x1) = mul_nat 2 x8)) x7.
Apply H21 with x5.
Assume H22: x7 ∈ omega.
Apply mul_nat_mul_SNo with 2, x7, λ x8 x9 . add_SNo x2 (minus_SNo x1) = x9 ⟶ x5 leaving 3 subgoals.
Apply nat_p_omega with 2.
The subproof is completed by applying nat_2.
The subproof is completed by applying H22.
Assume H23: add_SNo x2 (minus_SNo x1) = mul_SNo 2 x7.
Apply unknownprop_0b973640ded967ccca7ae90b9a0ad1cbab8b72d7d8e77d5564f2ebb33a0b2952 with x4, x3, x5 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H3.
Assume H24: add_SNo x4 x3 ∈ omega.
Assume H25: ∃ x8 . and (x8 ∈ omega) (add_SNo x4 x3 = mul_nat 2 x8).
Apply H25 with x5.
Let x8 of type ι be given.
Assume H26: (λ x9 . and (x9 ∈ omega) (add_SNo x4 x3 = mul_nat 2 x9)) x8.
Apply H26 with x5.
Assume H27: x8 ∈ omega.
Apply mul_nat_mul_SNo with 2, x8, λ x9 x10 . add_SNo x4 x3 = x10 ⟶ x5 leaving 3 subgoals.
Apply nat_p_omega with 2.
The subproof is completed by applying nat_2.
The subproof is completed by applying H27.
...
■