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.
Let x3 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Assume H2: SNo x2.
Assume H3: SNo x3.
Apply unknownprop_e1da79ad2238fc685b3e4f7de09c0d965538bebf8c87c6f411479674dad88ab7 with f4b0e.. x0 x1 x2 x3, e47cc.. (f4b0e.. x0 x1 x2 x3) = x2 leaving 2 subgoals.
Apply unknownprop_1c4b77a1bdf71ac8c46772d8b01bd6609e54ee74070e16498c4800adfe13c5ca with x0, x1, x2, x3 leaving 4 subgoals.
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.
Assume H4: SNo (e47cc.. (f4b0e.. x0 x1 x2 x3)).
Assume H5: ∃ x4 . and (SNo x4) (f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) (e5fe3.. (f4b0e.. x0 x1 x2 x3)) (e47cc.. (f4b0e.. x0 x1 x2 x3)) x4).
Apply H5 with e47cc.. (f4b0e.. x0 x1 x2 x3) = x2.
Let x4 of type ι be given.
Assume H6: (λ x5 . and (SNo x5) (f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) (e5fe3.. (f4b0e.. x0 x1 x2 x3)) (e47cc.. (f4b0e.. x0 x1 x2 x3)) x5)) x4.
Apply H6 with e47cc.. (f4b0e.. x0 x1 x2 x3) = x2.
Assume H7: SNo x4.
Assume H8: f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) (e5fe3.. (f4b0e.. x0 x1 x2 x3)) (e47cc.. (f4b0e.. x0 x1 x2 x3)) x4.
Let x5 of type ι → ι → ο be given.
Apply unknownprop_99f23fd81225bd29ee42dc62a4d6e5b57a541a40a9b9a933a59c939aaf96ffc9 with x0, x1, x2, x3, 6b27d.. (f4b0e.. x0 x1 x2 x3), e5fe3.. (f4b0e.. x0 x1 x2 x3), e47cc.. (f4b0e.. x0 x1 x2 x3), x4, λ x6 x7 . x5 x7 x6 leaving 9 subgoals.
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.
Apply unknownprop_d490e9b67b13d1ef9389d3ace4e99a44b8ce86dd1d81aca7dab87729606ec525 with f4b0e.. x0 x1 x2 x3.
Apply unknownprop_1c4b77a1bdf71ac8c46772d8b01bd6609e54ee74070e16498c4800adfe13c5ca with x0, x1, x2, x3 leaving 4 subgoals.
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.
Apply unknownprop_221fdb669888182bab57f3018210dac7aa6f39893e1d9c3490c39bcf8bddffeb with f4b0e.. x0 x1 x2 x3.
Apply unknownprop_1c4b77a1bdf71ac8c46772d8b01bd6609e54ee74070e16498c4800adfe13c5ca with x0, x1, x2, x3 leaving 4 subgoals.
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.
Apply unknownprop_8c3e941e183588bb9845a8e92af7c2409f09ad8e12d04378912de4f735a7c469 with f4b0e.. x0 x1 x2 x3.
Apply unknownprop_1c4b77a1bdf71ac8c46772d8b01bd6609e54ee74070e16498c4800adfe13c5ca with x0, x1, x2, x3 leaving 4 subgoals.
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 H7.
The subproof is completed by applying H8.
■