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_cc98097463596822ee898799e3d575e97f4d301507d1aca5bf428b8056270a60 with f4b0e.. x0 x1 x2 x3, e5fe3.. (f4b0e.. x0 x1 x2 x3) = x1 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 (e5fe3.. (f4b0e.. x0 x1 x2 x3)).
Assume H5: ∃ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) (e5fe3.. (f4b0e.. x0 x1 x2 x3)) x4 x5)).
Apply H5 with e5fe3.. (f4b0e.. x0 x1 x2 x3) = x1.
Let x4 of type ι be given.
Assume H6: (λ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) (e5fe3.. (f4b0e.. x0 x1 x2 x3)) x5 x6))) x4.
Apply H6 with e5fe3.. (f4b0e.. x0 x1 x2 x3) = x1.
Assume H7: SNo x4.
Assume H8: ∃ x5 . and (SNo x5) (f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) (e5fe3.. (f4b0e.. x0 x1 x2 x3)) x4 x5).
Apply H8 with e5fe3.. (f4b0e.. x0 x1 x2 x3) = x1.
Let x5 of type ι be given.
Assume H9: (λ x6 . and (SNo x6) (f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) (e5fe3.. (f4b0e.. x0 x1 x2 x3)) x4 x6)) x5.
Apply H9 with e5fe3.. (f4b0e.. x0 x1 x2 x3) = x1.
Assume H10: SNo x5.
Assume H11: f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) (e5fe3.. (f4b0e.. x0 x1 x2 x3)) x4 x5.
Let x6 of type ι → ι → ο be given.
Apply unknownprop_a3a33ccb0071c2878f92a1cae7afeb2b106a5eb10ab63f1d0d9582d703abc2a9 with x0, x1, x2, x3, 6b27d.. (f4b0e.. x0 x1 x2 x3), e5fe3.. (f4b0e.. x0 x1 x2 x3), x4, x5, λ x7 x8 . x6 x8 x7 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.
The subproof is completed by applying H7.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
■