Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
x0
∈
u16
.
Apply unknownprop_485b5a544f4a752392d62c01e55a5e36a8748d64fd7af6f27349bd2453284446 with
x0
,
λ x1 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x1
)
)
)
=
x1
leaving 17 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_ddfd049a99d8a8d08a5969e20f08be40e16f962ab49dd05ba7dcd1cfd68e7645 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
)
=
0
.
Apply unknownprop_3ce04bff2a395cf5fe0b94d0636cc8dbea0e46272d1360d7109558a625b43849 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
=
0
.
Apply unknownprop_2deda5cc0874f100e0fcd31fbab30140488390c1e46b9b2da484e79975ce6ae8 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
=
0
.
The subproof is completed by applying unknownprop_5f23a09617e395d3412bcd886825a830fcbca9dbfaa3bb762a6b0286bbba2699.
Apply unknownprop_3ce04bff2a395cf5fe0b94d0636cc8dbea0e46272d1360d7109558a625b43849 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
)
=
u1
.
Apply unknownprop_2deda5cc0874f100e0fcd31fbab30140488390c1e46b9b2da484e79975ce6ae8 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
=
u1
.
Apply unknownprop_5f23a09617e395d3412bcd886825a830fcbca9dbfaa3bb762a6b0286bbba2699 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
=
u1
.
The subproof is completed by applying unknownprop_ddfd049a99d8a8d08a5969e20f08be40e16f962ab49dd05ba7dcd1cfd68e7645.
Apply unknownprop_5f23a09617e395d3412bcd886825a830fcbca9dbfaa3bb762a6b0286bbba2699 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
)
=
u2
.
Apply unknownprop_ddfd049a99d8a8d08a5969e20f08be40e16f962ab49dd05ba7dcd1cfd68e7645 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
=
u2
.
Apply unknownprop_3ce04bff2a395cf5fe0b94d0636cc8dbea0e46272d1360d7109558a625b43849 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
=
u2
.
The subproof is completed by applying unknownprop_2deda5cc0874f100e0fcd31fbab30140488390c1e46b9b2da484e79975ce6ae8.
Apply unknownprop_2deda5cc0874f100e0fcd31fbab30140488390c1e46b9b2da484e79975ce6ae8 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
)
=
u3
.
Apply unknownprop_5f23a09617e395d3412bcd886825a830fcbca9dbfaa3bb762a6b0286bbba2699 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
=
u3
.
Apply unknownprop_ddfd049a99d8a8d08a5969e20f08be40e16f962ab49dd05ba7dcd1cfd68e7645 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
=
u3
.
The subproof is completed by applying unknownprop_3ce04bff2a395cf5fe0b94d0636cc8dbea0e46272d1360d7109558a625b43849.
Apply unknownprop_d02d672c88891239a2034f8db0a8f9c766e8b44a6127d48b08a622cce7dc65fa with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
)
=
u4
.
Apply unknownprop_b4b0b30bf8e5ff91ed4869311536b86e18ba1e4d9dcdabf73d46693ed9a5b67b with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
=
u4
.
Apply unknownprop_c0eb4e3448ef31f6408883194d369de2b67b2c3b8eb9ad88a4d52d9ee850a560 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
=
u4
.
The subproof is completed by applying unknownprop_8a85de05c64795068871a87d3b06ba1e5395c94812285b09588df3e01a1e0ea3.
Apply unknownprop_b4b0b30bf8e5ff91ed4869311536b86e18ba1e4d9dcdabf73d46693ed9a5b67b with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
)
=
u5
.
Apply unknownprop_c0eb4e3448ef31f6408883194d369de2b67b2c3b8eb9ad88a4d52d9ee850a560 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
=
u5
.
Apply unknownprop_8a85de05c64795068871a87d3b06ba1e5395c94812285b09588df3e01a1e0ea3 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
=
u5
.
The subproof is completed by applying unknownprop_d02d672c88891239a2034f8db0a8f9c766e8b44a6127d48b08a622cce7dc65fa.
Apply unknownprop_8a85de05c64795068871a87d3b06ba1e5395c94812285b09588df3e01a1e0ea3 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
)
=
u6
.
Apply unknownprop_d02d672c88891239a2034f8db0a8f9c766e8b44a6127d48b08a622cce7dc65fa with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
=
u6
.
Apply unknownprop_b4b0b30bf8e5ff91ed4869311536b86e18ba1e4d9dcdabf73d46693ed9a5b67b with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
=
u6
.
The subproof is completed by applying unknownprop_c0eb4e3448ef31f6408883194d369de2b67b2c3b8eb9ad88a4d52d9ee850a560.
Apply unknownprop_c0eb4e3448ef31f6408883194d369de2b67b2c3b8eb9ad88a4d52d9ee850a560 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
)
=
u7
.
Apply unknownprop_8a85de05c64795068871a87d3b06ba1e5395c94812285b09588df3e01a1e0ea3 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
=
u7
.
Apply unknownprop_d02d672c88891239a2034f8db0a8f9c766e8b44a6127d48b08a622cce7dc65fa with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
=
u7
.
The subproof is completed by applying unknownprop_b4b0b30bf8e5ff91ed4869311536b86e18ba1e4d9dcdabf73d46693ed9a5b67b.
Apply unknownprop_f74f5074ad12d57b1f85300d32210524157b09a0919ee38128acf015331c35f0 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
)
=
u8
.
Apply unknownprop_29ccb5c4e7950928d647b0941425c5e64d69ebaaed74cba3c055174a14ae4c5b with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
=
u8
.
Apply unknownprop_9b334a439f93d75505077dcc1fe4c60157a3105589338dee138085e931431815 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
=
u8
.
The subproof is completed by applying unknownprop_4e46240fa21fb39b84708f415e3b21cc616773a08b926976627048ab8fc29078.
Apply unknownprop_4e46240fa21fb39b84708f415e3b21cc616773a08b926976627048ab8fc29078 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
)
=
u9
.
Apply unknownprop_f74f5074ad12d57b1f85300d32210524157b09a0919ee38128acf015331c35f0 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
=
u9
.
Apply unknownprop_29ccb5c4e7950928d647b0941425c5e64d69ebaaed74cba3c055174a14ae4c5b with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
=
u9
.
The subproof is completed by applying unknownprop_9b334a439f93d75505077dcc1fe4c60157a3105589338dee138085e931431815.
Apply unknownprop_29ccb5c4e7950928d647b0941425c5e64d69ebaaed74cba3c055174a14ae4c5b with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
)
=
u10
.
Apply unknownprop_9b334a439f93d75505077dcc1fe4c60157a3105589338dee138085e931431815 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
=
u10
.
Apply unknownprop_4e46240fa21fb39b84708f415e3b21cc616773a08b926976627048ab8fc29078 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
=
u10
.
The subproof is completed by applying unknownprop_f74f5074ad12d57b1f85300d32210524157b09a0919ee38128acf015331c35f0.
Apply unknownprop_9b334a439f93d75505077dcc1fe4c60157a3105589338dee138085e931431815 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
)
=
u11
.
Apply unknownprop_4e46240fa21fb39b84708f415e3b21cc616773a08b926976627048ab8fc29078 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
=
u11
.
Apply unknownprop_f74f5074ad12d57b1f85300d32210524157b09a0919ee38128acf015331c35f0 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
=
u11
.
The subproof is completed by applying unknownprop_29ccb5c4e7950928d647b0941425c5e64d69ebaaed74cba3c055174a14ae4c5b.
Apply unknownprop_c21ba5695b1d95da76a10179e8a88254ffe230dfdf6a6df2f9b5ee9d0562acd5 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
)
=
u12
.
Apply unknownprop_ffb148d18f258a6f2e8b9af29fd6bea695bdd737e09f02c9ed6ace715b49951e with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
=
u12
.
Apply unknownprop_5236a0eac529d064f7d4286c27876c5cf1e6aa8482e677668f1eb521e10e6be9 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
=
u12
.
The subproof is completed by applying unknownprop_991646d91cf5e2f3eac2db7f6827c54bc2cbba5f33c26bd9a4d54268790991f8.
Apply unknownprop_ffb148d18f258a6f2e8b9af29fd6bea695bdd737e09f02c9ed6ace715b49951e with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
)
=
u13
.
Apply unknownprop_5236a0eac529d064f7d4286c27876c5cf1e6aa8482e677668f1eb521e10e6be9 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
(
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
)
=
u13
.
Apply unknownprop_991646d91cf5e2f3eac2db7f6827c54bc2cbba5f33c26bd9a4d54268790991f8 with
λ x1 x2 .
u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12
x2
=
u13
.
The subproof is completed by applying unknownprop_c21ba5695b1d95da76a10179e8a88254ffe230dfdf6a6df2f9b5ee9d0562acd5.
...
...
■