Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 74e69.. x0.
Claim L1: ...
...
Let x1 of type ο be given.
Assume H2: ∀ x2 . and (762f0.. x2 (a3eb9.. x0 x0) (a3eb9.. x0 x0)) (∀ x3 : ι → ο . 858ff.. x0 x3∀ x4 x5 . c0709.. x3 x3 x45dc8b.. x4 x5d7d78.. x2 x4 x5)x1.
Apply H2 with 6b90c.. (f9341.. c4def.. c9248..) (3e00e.. (1fa6d.. (2fe34.. c4def..)) (1fa6d.. (a6e19.. c4def..))).
Apply andI with 762f0.. (6b90c.. (f9341.. c4def.. c9248..) (3e00e.. (1fa6d.. (2fe34.. c4def..)) (1fa6d.. (a6e19.. c4def..)))) (a3eb9.. x0 x0) (a3eb9.. x0 x0), ∀ x2 : ι → ο . 858ff.. x0 x2∀ x3 x4 . c0709.. x2 x2 x35dc8b.. x3 x4d7d78.. (6b90c.. (f9341.. c4def.. c9248..) (3e00e.. (1fa6d.. (2fe34.. c4def..)) (1fa6d.. (a6e19.. c4def..)))) x3 x4 leaving 2 subgoals.
Apply unknownprop_91d92016e9d9449b22c74055c672ab1eb06568e089f26cc1ad9725e31f12c706 with a3eb9.. x0 x0, bf68c.. (a3eb9.. x0 x0) 5e331.., a3eb9.. x0 x0, f9341.. c4def.. c9248.., 3e00e.. (1fa6d.. (2fe34.. c4def..)) (1fa6d.. (a6e19.. c4def..)) leaving 2 subgoals.
Apply unknownprop_5910e12cee1a5b2d159f4ee4e69ffaceb372c34b85593967cc3cc192cad48cea with a3eb9.. x0 x0, a3eb9.. x0 x0, 5e331.., c4def.., c9248.. leaving 2 subgoals.
Apply unknownprop_60842d1ccb7d3d5b26c08ad699db295c00ad2967f73d4694f4f350cb6d20eb5b with a3eb9.. x0 x0.
The subproof is completed by applying L1.
Apply unknownprop_c4d4b89cf7ba6a39c156cfa03f780b783af47e6e6e7093374af2765ddeb6594d with a3eb9.. x0 x0.
The subproof is completed by applying L1.
Apply unknownprop_e7a22c51178d8f0f7026aeda0c750fc4973d4211507751855a9a347426e4ef8c with x0, x0, 5e331.., a3eb9.. x0 x0, 1fa6d.. (2fe34.. c4def..), 1fa6d.. (a6e19.. c4def..) leaving 2 subgoals.
Apply unknownprop_ba131486bc61d00940f38c734de6fce9eae84b9ea0e8e9c4ef1eac30849d0397 with x0, 5e331.., a3eb9.. x0 x0, 2fe34.. c4def.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_2889540f2161c9537dc388d6c2702e3891e2b8722a023eec016fa2e08ac47609.
Apply unknownprop_3379cf7ef3eb29eac12edea556cf0b0d9c92a6995c440aebae09bbe305dd13dd with x0, x0, x0, c4def.. leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_60842d1ccb7d3d5b26c08ad699db295c00ad2967f73d4694f4f350cb6d20eb5b with x0.
The subproof is completed by applying H0.
Apply unknownprop_ba131486bc61d00940f38c734de6fce9eae84b9ea0e8e9c4ef1eac30849d0397 with x0, 5e331.., a3eb9.. x0 x0, a6e19.. c4def.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_2889540f2161c9537dc388d6c2702e3891e2b8722a023eec016fa2e08ac47609.
Apply unknownprop_bc486661cb01188dd417f1af75be751e81c6543f67aae690c07ce1c3d5e551fd with x0, x0, x0, c4def.. leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_60842d1ccb7d3d5b26c08ad699db295c00ad2967f73d4694f4f350cb6d20eb5b with x0.
The subproof is completed by applying H0.
Let x2 of type ιο be given.
Assume H3: 858ff.. x0 x2.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H4: c0709.. x2 x2 x3.
Apply unknownprop_a5b271614b343123a717eec1affb554f571caa8da7ec2eb38b2a4124da681f35 with x2, x2, x3, λ x5 . 5dc8b.. x5 x4d7d78.. (6b90c.. (f9341.. c4def.. c9248..) (3e00e.. (1fa6d.. (2fe34.. c4def..)) (1fa6d.. (a6e19.. c4def..)))) x5 x4 leaving 3 subgoals.
The subproof is completed by applying H4.
Let x5 of type ι be given.
Assume H5: x2 x5.
Assume H6: 5dc8b.. (0b8ef.. x5) x4.
Claim L7: x4 = 6c5f4.. x5
Apply H6 with x4 = 6c5f4.. x5.
Assume H7: ∀ x6 . 0b8ef.. x5 = 0b8ef.. x6x4 = 6c5f4.. x6.
...
Apply unknownprop_3cd0715532a3265d361db53d355c139475311b1f2d82646fd4590d7e789e43e9 with f9341.. c4def.. c9248.., 3e00e.. (1fa6d.. (2fe34.. c4def..)) (1fa6d.. (a6e19.. c4def..)), 0b8ef.. x5, cfc98.. (0b8ef.. x5) 236c6.., x4 leaving 2 subgoals.
Apply unknownprop_d52bc478effa3bcc528439e2b8f77beb0fe8312413b730398a6df08292fdc86f with c4def.., c9248.., 0b8ef.. x5, 0b8ef.. x5, 236c6.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_7952446787e7ec87974d8b0564aec0660f9849ef8699aeee5e2d5d268814fd9d with 0b8ef.. x5.
The subproof is completed by applying unknownprop_53761669a36bbbd1a31b2934eda38089c33e08dbd0d93aaab2f4ef7246c6b583 with 0b8ef.. x5.
Apply unknownprop_46e4c58bc345eebd7d8dacb0dd258160854f634df9e25dffce87f176f442893d with 1fa6d.. (2fe34.. c4def..), 1fa6d.. (a6e19.. c4def..), x5, 236c6.., x4 leaving 2 subgoals.
Apply unknownprop_de997f3dea338bdea395be4ca3cb97eb524cbb5ce75355345273e4eaa0c35110 with a6e19.. c4def...
Apply unknownprop_4c282b9faa87cf98ec755257bbb7d88a24943ff260debf59b7c422310bade2ae with c4def...
The subproof is completed by applying unknownprop_a866da150736a63955bc6564d827f7c01bae2a20c456de9663c4ff93bd67f424.
Apply unknownprop_768846bee590072393edcb418ed13c2ad80ba15c56ef6f8524df152f3dcda94b with 2fe34.. c4def.., x5, 236c6.., x4.
Apply L7 with λ x6 x7 . d7d78.. (2fe34.. c4def..) x5 x7.
Apply unknownprop_43e178cdfe01b60455674b24d88021e9fd03bf63b4a4ef1646d60f6afa13968c with c4def.., x5, x5.
The subproof is completed by applying unknownprop_7952446787e7ec87974d8b0564aec0660f9849ef8699aeee5e2d5d268814fd9d with x5.
...