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.
Let x4 of type ι → ι → ο be given.
Assume H0: ∀ x5 x6 . x0 x5 x6 ⟶ x2 x5 x6.
Assume H1: ∀ x5 x6 . x1 x5 x6 ⟶ x3 x5 x6.
Let x5 of type ι be given.
Let x6 of type ι be given.
Assume H2: 6fe8d.. x0 x1 x4 x5 x6.
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ∀ x7 : ι → ι → ο . 6fe8d.. x2 x3 x7 ... ...
...
Claim L6: ∀ x7 : ι → ι → ο . ∀ x8 x9 . ∀ x10 : ι → ι . f6435.. x8 ⟶ 6fe8d.. x2 x3 x7 x9 32d20.. ⟶ (∀ x11 . 6fe8d.. x2 x3 (a603a.. x7 x11 x9) (x10 x11) x8) ⟶ 6fe8d.. x2 x3 x7 (d7cf0.. x9 x10) x8
The subproof is completed by applying unknownprop_2e4c9e9bb00a1e00d61dddf5b93521d4a44a5cf34a5d77eca45d066a0b32082a with x2, x3.
Claim L7: ∀ x7 : ι → ι → ο . ∀ x8 x9 x10 . ∀ x11 : ι → ι . 6fe8d.. x2 x3 x7 x8 (d7cf0.. x10 x11) ⟶ 6fe8d.. x2 x3 x7 x9 x10 ⟶ 6fe8d.. x2 x3 x7 (57d6a.. x8 x9) (x11 x9)
The subproof is completed by applying unknownprop_8456f035593e381677ad0ec884ea2dfed6273d70a1e5efa2af3d3eb450e5586f with x2, x3.
Claim L8: ∀ x7 : ι → ι → ο . ∀ x8 x9 . ∀ x10 x11 : ι → ι . f6435.. x8 ⟶ 6fe8d.. x2 x3 x7 (d7cf0.. x9 x11) x8 ⟶ (∀ x12 . 6fe8d.. x2 x3 (a603a.. x7 x12 x9) (x10 x12) (x11 x12)) ⟶ 6fe8d.. x2 x3 x7 (bcddf.. 236c6.. x10) (d7cf0.. x9 x11)
The subproof is completed by applying unknownprop_510808a11832070bcf15607bc572170af8cf979aa4f3ab5b88c733f81d69907f with x2, x3.
Claim L9: ∀ x7 : ι → ι → ο . ∀ x8 x9 . ∀ x10 x11 : ι → ι . f6435.. x8 ⟶ 6fe8d.. x2 x3 x7 (d7cf0.. x9 x11) x8 ⟶ (∀ x12 . 6fe8d.. x2 x3 (a603a.. x7 x12 x9) (x10 x12) (x11 x12)) ⟶ 6fe8d.. x2 x3 x7 (bcddf.. x9 x10) (d7cf0.. x9 x11)
The subproof is completed by applying unknownprop_bc2f57b276f298274cf2467348663bf105d56ef092df4833d27c4f6de3d5dc24 with x2, x3.
Claim L10: ∀ x7 : ι → ι → ο . ∀ x8 x9 x10 x11 x12 . f6435.. x8 ⟶ 6fe8d.. x2 x3 x7 x9 x10 ⟶ 6fe8d.. x2 x3 x7 x11 x8 ⟶ d3ec1.. x1 x10 x12 ⟶ d3ec1.. x1 x11 x12 ⟶ 6fe8d.. x2 x3 x7 x9 x11
Let x7 of type ι → ι → ο be given.
Let x8 of type ι be given.
Let x9 of type ι be given.
Let x10 of type ι be given.
Let x11 of type ι be given.
Let x12 of type ι be given.
Assume H10: f6435.. x8.
Assume H11: 6fe8d.. x2 x3 x7 x9 x10.
Assume H12: 6fe8d.. x2 x3 x7 x11 x8.
Assume H13: d3ec1.. x1 x10 x12.
Assume H14: d3ec1.. x1 x11 x12.
Apply unknownprop_fb66be13bb3f2fcbd6d949f930019a20c7e8bbd93b3cab6ec1631b1b17f0580c with x2, x3, x7, x8, x9, x10, x11, x12 leaving 5 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
Apply unknownprop_8b6292ae7b987f16990c98fbd5484910269e872c05a77fc4d674d658d1f6ddb6 with x1, x3, x10, x12 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H13.
Apply unknownprop_8b6292ae7b987f16990c98fbd5484910269e872c05a77fc4d674d658d1f6ddb6 with x1, x3, x11, x12 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H14.
Apply H2 with 6fe8d.. x2 x3 leaving 8 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
The subproof is completed by applying L8.
The subproof is completed by applying L9.
The subproof is completed by applying L10.
■