Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ u16.
Let x1 of type ι be given.
Apply unknownprop_485b5a544f4a752392d62c01e55a5e36a8748d64fd7af6f27349bd2453284446 with x0, λ x2 . x1 ∈ x2 ⟶ u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x2 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x1 ⟶ ∀ x3 : ο . x3 leaving 17 subgoals.
The subproof is completed by applying H0.
Assume H1: x1 ∈ 0.
Apply FalseE with u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 0 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x1 ⟶ ∀ x2 : ο . x2.
Apply EmptyE with x1.
The subproof is completed by applying H1.
Assume H1: x1 ∈ u1.
Apply cases_1 with x1, λ x2 . u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u1 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x2 ⟶ ∀ x3 : ο . x3 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_3ce04bff2a395cf5fe0b94d0636cc8dbea0e46272d1360d7109558a625b43849 with λ x2 x3 . x3 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 0 ⟶ ∀ x4 : ο . x4.
Apply unknownprop_ddfd049a99d8a8d08a5969e20f08be40e16f962ab49dd05ba7dcd1cfd68e7645 with λ x2 x3 . u3 = x3 ⟶ ∀ x4 : ο . x4.
The subproof is completed by applying neq_3_1.
Assume H1: x1 ∈ u2.
Apply cases_2 with x1, λ x2 . u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u2 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x2 ⟶ ∀ x3 : ο . x3 leaving 3 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_5f23a09617e395d3412bcd886825a830fcbca9dbfaa3bb762a6b0286bbba2699 with λ x2 x3 . x3 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 0 ⟶ ∀ x4 : ο . x4.
Apply unknownprop_ddfd049a99d8a8d08a5969e20f08be40e16f962ab49dd05ba7dcd1cfd68e7645 with λ x2 x3 . 0 = x3 ⟶ ∀ x4 : ο . x4.
Assume H2: 0 = u1.
Apply neq_1_0.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H2 with λ x3 x4 . x2 x4 x3.
Apply unknownprop_5f23a09617e395d3412bcd886825a830fcbca9dbfaa3bb762a6b0286bbba2699 with λ x2 x3 . x3 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 1 ⟶ ∀ x4 : ο . x4.
Apply unknownprop_3ce04bff2a395cf5fe0b94d0636cc8dbea0e46272d1360d7109558a625b43849 with λ x2 x3 . 0 = x3 ⟶ ∀ x4 : ο . x4.
Assume H2: 0 = u3.
Apply neq_3_0.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H2 with λ x3 x4 . x2 x4 x3.
Assume H1: x1 ∈ u3.
Apply cases_3 with x1, λ x2 . u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u3 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x2 ⟶ ∀ x3 : ο . x3 leaving 4 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_2deda5cc0874f100e0fcd31fbab30140488390c1e46b9b2da484e79975ce6ae8 with λ x2 x3 . x3 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 0 ⟶ ∀ x4 : ο . x4.
Apply unknownprop_ddfd049a99d8a8d08a5969e20f08be40e16f962ab49dd05ba7dcd1cfd68e7645 with λ x2 x3 . u2 = x3 ⟶ ∀ x4 : ο . x4.
The subproof is completed by applying neq_2_1.
Apply unknownprop_2deda5cc0874f100e0fcd31fbab30140488390c1e46b9b2da484e79975ce6ae8 with λ x2 x3 . x3 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 1 ⟶ ∀ x4 : ο . x4.
Apply unknownprop_3ce04bff2a395cf5fe0b94d0636cc8dbea0e46272d1360d7109558a625b43849 with λ x2 x3 . u2 = x3 ⟶ ∀ x4 : ο . x4.
Assume H2: u2 = u3.
Apply neq_3_2.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H2 with λ x3 x4 . x2 x4 x3.
Apply unknownprop_2deda5cc0874f100e0fcd31fbab30140488390c1e46b9b2da484e79975ce6ae8 with λ x2 x3 . x3 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 2 ⟶ ∀ x4 : ο . x4.
Apply unknownprop_5f23a09617e395d3412bcd886825a830fcbca9dbfaa3bb762a6b0286bbba2699 with λ x2 x3 . u2 = x3 ⟶ ∀ x4 : ο . x4.
The subproof is completed by applying neq_2_0.
Assume H1: x1 ∈ u4.
Apply cases_4 with x1, λ x2 . u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u4 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x2 ⟶ ∀ x3 : ο . x3 leaving 5 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_d02d672c88891239a2034f8db0a8f9c766e8b44a6127d48b08a622cce7dc65fa with λ x2 x3 . x3 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 0 ⟶ ∀ x4 : ο . x4.
Apply unknownprop_ddfd049a99d8a8d08a5969e20f08be40e16f962ab49dd05ba7dcd1cfd68e7645 with λ x2 x3 . u5 = x3 ⟶ ∀ x4 : ο . x4.
The subproof is completed by applying neq_5_1.
Apply unknownprop_d02d672c88891239a2034f8db0a8f9c766e8b44a6127d48b08a622cce7dc65fa with λ x2 x3 . x3 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 1 ⟶ ∀ x4 : ο . x4.
Apply unknownprop_3ce04bff2a395cf5fe0b94d0636cc8dbea0e46272d1360d7109558a625b43849 with λ x2 x3 . u5 = x3 ⟶ ∀ x4 : ο . x4.
The subproof is completed by applying neq_5_3.
Apply unknownprop_d02d672c88891239a2034f8db0a8f9c766e8b44a6127d48b08a622cce7dc65fa with λ x2 x3 . x3 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 2 ⟶ ∀ x4 : ο . x4.
Apply unknownprop_5f23a09617e395d3412bcd886825a830fcbca9dbfaa3bb762a6b0286bbba2699 with λ x2 x3 . u5 = x3 ⟶ ∀ x4 : ο . x4.
The subproof is completed by applying neq_5_0.
Apply unknownprop_d02d672c88891239a2034f8db0a8f9c766e8b44a6127d48b08a622cce7dc65fa with λ x2 x3 . x3 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 3 ⟶ ∀ x4 : ο . x4.
Apply unknownprop_2deda5cc0874f100e0fcd31fbab30140488390c1e46b9b2da484e79975ce6ae8 with λ x2 x3 . u5 = x3 ⟶ ∀ x4 : ο . x4.
The subproof is completed by applying neq_5_2.
Assume H1: x1 ∈ u5.
Apply cases_5 with x1, λ x2 . u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u5 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x2 ⟶ ∀ x3 : ο . x3 leaving 6 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_b4b0b30bf8e5ff91ed4869311536b86e18ba1e4d9dcdabf73d46693ed9a5b67b with λ x2 x3 . x3 = u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 0 ⟶ ∀ x4 : ο . x4.
Apply unknownprop_ddfd049a99d8a8d08a5969e20f08be40e16f962ab49dd05ba7dcd1cfd68e7645 with λ x2 x3 . u7 = x3 ⟶ ∀ x4 : ο . x4.
The subproof is completed by applying neq_7_1.
Apply unknownprop_b4b0b30bf8e5ff91ed4869311536b86e18ba1e4d9dcdabf73d46693ed9a5b67b with λ x2 x3 . ....
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■