Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0omega.
Apply unknownprop_513c07ab8c4a322509acfbace4471c9db9e0c1f3fed5cccfa0919534f9c289bd with x0, ∃ x1 . and (x1omega) (∃ x2 . and (x2omega) (∃ x3 . and (x3omega) (∃ x4 . and (x4omega) (x0 = add_nat (mul_nat x1 x1) (add_nat (mul_nat x2 x2) (add_nat (mul_nat x3 x3) (mul_nat x4 x4))))))) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H1: (λ x2 . and (x2omega) (∃ x3 . and (x3omega) (∃ x4 . and (x4omega) (∃ x5 . and (x5omega) (x0 = add_SNo (mul_SNo x2 x2) (add_SNo (mul_SNo x3 x3) (add_SNo (mul_SNo x4 x4) (mul_SNo x5 x5)))))))) x1.
Apply H1 with ∃ x2 . and (x2omega) (∃ x3 . and (x3omega) (∃ x4 . and (x4omega) (∃ x5 . and (x5omega) (x0 = add_nat (mul_nat x2 x2) (add_nat (mul_nat x3 x3) (add_nat (mul_nat x4 x4) (mul_nat x5 x5))))))).
Assume H2: x1omega.
Assume H3: ∃ x2 . and (x2omega) (∃ x3 . and (x3omega) (∃ x4 . and (x4omega) (x0 = add_SNo (mul_SNo x1 x1) (add_SNo (mul_SNo x2 x2) (add_SNo (mul_SNo x3 x3) (mul_SNo x4 x4)))))).
Apply H3 with ∃ x2 . and (x2omega) (∃ x3 . and (x3omega) (∃ x4 . and (x4omega) (∃ x5 . and (x5omega) (x0 = add_nat (mul_nat x2 x2) (add_nat (mul_nat x3 x3) (add_nat (mul_nat x4 x4) (mul_nat x5 x5))))))).
Let x2 of type ι be given.
Assume H4: (λ x3 . and (x3omega) (∃ x4 . and (x4omega) (∃ x5 . and (x5omega) (x0 = add_SNo (mul_SNo x1 x1) (add_SNo (mul_SNo x3 x3) (add_SNo (mul_SNo x4 x4) (mul_SNo x5 x5))))))) x2.
Apply H4 with ∃ x3 . and (x3omega) (∃ x4 . and (x4omega) (∃ x5 . and (x5omega) (∃ x6 . and (x6omega) (x0 = add_nat (mul_nat x3 x3) (add_nat (mul_nat x4 x4) (add_nat (mul_nat x5 x5) (mul_nat x6 x6))))))).
Assume H5: x2omega.
Assume H6: ∃ x3 . and (......) ....
...