Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCit../945c6..
PUKcE../edae9..
vout
PrCit../89642.. 2.72 bars
TMNRm../8f8ff.. ownership of 033e1.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHNa../5e651.. ownership of 6edd5.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNHB../42260.. ownership of 25794.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTM9../e49d4.. ownership of 8fc73.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMV6s../26e11.. ownership of 62d9a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMY7g../1133a.. ownership of df033.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMJfe../1c51a.. ownership of 728cd.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZ1q../48a4d.. ownership of 2e156.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMVdR../dfbcb.. ownership of 4b75a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMS2b../65794.. ownership of c0a93.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKVz../5dc56.. ownership of 0733b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMFQc../17916.. ownership of bcc57.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMVoz../fcf8b.. ownership of 2bc58.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMV59../b2c2f.. ownership of 47c9d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMWEb../c531f.. ownership of c9b7d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMG7F../56a12.. ownership of 5b18f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTbc../f9a9a.. ownership of ae354.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMJ2H../19c36.. ownership of 5dd30.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMYg9../b12b2.. ownership of 2a49e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTT5../57374.. ownership of aa60e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKKf../9818c.. ownership of 53b4c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMEms../7d6e1.. ownership of 1ec6e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKXu../689dc.. ownership of aed67.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMaZU../3ad56.. ownership of 0e29e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXGR../6beef.. ownership of d1f46.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMSTu../01ff6.. ownership of a9bd9.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMLcc../794d1.. ownership of 00b44.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMJ2Z../6328c.. ownership of 77b56.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPUw../d5689.. ownership of ac29e.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMWKC../a3b87.. ownership of 5c9a4.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZ58../db152.. ownership of 71717.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTD1../7a2af.. ownership of bfd23.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMmT../a63c3.. ownership of 41e30.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRg2../2ca78.. ownership of f7041.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdj7../5486a.. ownership of b45a2.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMJeW../5d5af.. ownership of 946c6.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMbRL../4c974.. ownership of d8424.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMUBT../bb822.. ownership of 0f943.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMLki../50783.. ownership of 4a24e.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMarZ../eb31c.. ownership of ce56f.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNGF../683f1.. ownership of baafa.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXdK../bd816.. ownership of 311d3.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMk5../d75d5.. ownership of b2a9d.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMJ8Y../c0120.. ownership of e66e6.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMGFS../c3e3e.. ownership of a7092.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNVn../4dc82.. ownership of 5f61b.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXFD../592fe.. ownership of 0ee54.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMaf5../88e89.. ownership of 5571f.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMT5f../24fc7.. ownership of 967cf.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKxR../b11d5.. ownership of 61857.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMFJN../51bca.. ownership of eecee.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMcJF../8050a.. ownership of f4cfa.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
PUfmE../9e68f.. doc published by Pr4zB..
Param 4006a.. : (ιιο) → ιιιιιιιιιο
Param fc090.. : (ιιο) → ιιιιιιιιιο
Param 07c0f.. : (ιιο) → ιιιιιιιιιο
Param 0076f.. : (ιιο) → ιιιιιιιιιο
Param adf05.. : (ιιο) → ιιιιιιιιιο
Param d5d69.. : (ιιο) → ιιιιιιιιιο
Param 3f98b.. : (ιιο) → ιιιιιιιιιο
Param 96c31.. : (ιιο) → ιιιιιιιιιο
Param 54c7d.. : (ιιο) → ιιιιιιιιιο
Param 130d9.. : (ιιο) → ιιιιιιιιιο
Param 4e6fe.. : (ιιο) → ιιιιιιιιιο
Param a62c3.. : (ιιο) → ιιιιιιιιιο
Param ceccf.. : (ιιο) → ιιιιιιιιιο
Param eb506.. : (ιιο) → ιιιιιιιιιο
Param 70755.. : (ιιο) → ιιιιιιιιιο
Param 97793.. : (ιιο) → ιιιιιιιιιο
Param aa64f.. : (ιιο) → ιιιιιιιιιο
Param 83aec.. : (ιιο) → ιιιιιιιιιο
Param 446f4.. : (ιιο) → ιιιιιιιιιο
Definition eecee.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04006a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0fc090.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x007c0f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x00076f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0adf05.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d5d69.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x03f98b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x096c31.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x054c7d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0130d9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04e6fe.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a62c3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ceccf.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0eb506.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x070755.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x097793.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0aa64f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x083aec.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0446f4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)x2
Param ba015.. : (ιιο) → ιιιιιιιιιο
Param 286f8.. : (ιιο) → ιιιιιιιιιο
Param 2c550.. : (ιιο) → ιιιιιιιιιο
Param f842a.. : (ιιο) → ιιιιιιιιιο
Param e9fc9.. : (ιιο) → ιιιιιιιιιο
Param 010eb.. : (ιιο) → ιιιιιιιιιο
Param fa0f3.. : (ιιο) → ιιιιιιιιιο
Param c7001.. : (ιιο) → ιιιιιιιιιο
Param 58722.. : (ιιο) → ιιιιιιιιιο
Param 84d91.. : (ιιο) → ιιιιιιιιιο
Param 90d0e.. : (ιιο) → ιιιιιιιιιο
Param 81d98.. : (ιιο) → ιιιιιιιιιο
Definition 967cf.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ba015.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x007c0f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x00076f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0286f8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02c550.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f842a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e9fc9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0010eb.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0130d9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04e6fe.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0fa0f3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a62c3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0c7001.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x058722.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x084d91.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x090d0e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ceccf.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x081d98.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x070755.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)x2
Param 30a11.. : (ιιο) → ιιιιιιιιιο
Param 076b3.. : (ιιο) → ιιιιιιιιιο
Param 3d3e7.. : (ιιο) → ιιιιιιιιιο
Param 14be0.. : (ιιο) → ιιιιιιιιιο
Param 4e91d.. : (ιιο) → ιιιιιιιιιο
Param 23b40.. : (ιιο) → ιιιιιιιιιο
Param 1a9fd.. : (ιιο) → ιιιιιιιιιο
Param e2ec9.. : (ιιο) → ιιιιιιιιιο
Param c480f.. : (ιιο) → ιιιιιιιιιο
Param 0db75.. : (ιιο) → ιιιιιιιιιο
Param 02471.. : (ιιο) → ιιιιιιιιιο
Param 1cf57.. : (ιιο) → ιιιιιιιιιο
Param 23926.. : (ιιο) → ιιιιιιιιιο
Param b19dd.. : (ιιο) → ιιιιιιιιιο
Param 2eb4b.. : (ιιο) → ιιιιιιιιιο
Param bce5f.. : (ιιο) → ιιιιιιιιιο
Param 73f36.. : (ιιο) → ιιιιιιιιιο
Param 94ee4.. : (ιιο) → ιιιιιιιιιο
Definition 0ee54.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x030a11.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0076b3.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x03d3e7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x014be0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04e91d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x023b40.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x01a9fd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e2ec9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0c480f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x00db75.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x002471.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x01cf57.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x023926.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b19dd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02eb4b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0bce5f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x073f36.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x094ee4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)x2
Param 811c0.. : (ιιο) → ιιιιιιιιιο
Param 96162.. : (ιιο) → ιιιιιιιιιο
Param 0768d.. : (ιιο) → ιιιιιιιιιο
Param 70a3c.. : (ιιο) → ιιιιιιιιιο
Param 2122d.. : (ιιο) → ιιιιιιιιιο
Param 39c17.. : (ιιο) → ιιιιιιιιιο
Param ee5b5.. : (ιιο) → ιιιιιιιιιο
Param 61b2a.. : (ιιο) → ιιιιιιιιιο
Param abda1.. : (ιιο) → ιιιιιιιιιο
Param 858d1.. : (ιιο) → ιιιιιιιιιο
Definition a7092.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0811c0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x096162.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04e91d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0c480f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x00db75.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x002471.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x00768d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x070a3c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02122d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x039c17.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ee5b5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x061b2a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02eb4b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0bce5f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0abda1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x073f36.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x094ee4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0858d1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)x2
Param 22b3a.. : (ιιο) → ιιιιιιιιιο
Param 723e0.. : (ιιο) → ιιιιιιιιιο
Param 1ecf8.. : (ιιο) → ιιιιιιιιιο
Param 915dd.. : (ιιο) → ιιιιιιιιιο
Param 58208.. : (ιιο) → ιιιιιιιιιο
Param b571f.. : (ιιο) → ιιιιιιιιιο
Param 7e5de.. : (ιιο) → ιιιιιιιιιο
Param a3794.. : (ιιο) → ιιιιιιιιιο
Param 093ca.. : (ιιο) → ιιιιιιιιιο
Param 34ae8.. : (ιιο) → ιιιιιιιιιο
Param 65996.. : (ιιο) → ιιιιιιιιιο
Param 45286.. : (ιιο) → ιιιιιιιιιο
Param b7a83.. : (ιιο) → ιιιιιιιιιο
Param 72d65.. : (ιιο) → ιιιιιιιιιο
Param b7e1a.. : (ιιο) → ιιιιιιιιιο
Param 4b4dd.. : (ιιο) → ιιιιιιιιιο
Param f4940.. : (ιιο) → ιιιιιιιιιο
Definition b2a9d.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x022b3a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0723e0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x01ecf8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0915dd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x058208.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b571f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x07e5de.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a3794.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0093ca.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x034ae8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x065996.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x045286.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b7a83.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x072d65.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b7e1a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04b4dd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f4940.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)x2
Param 682ac.. : (ιιο) → ιιιιιιιιιο
Param 5f6ee.. : (ιιο) → ιιιιιιιιιο
Param a2b8b.. : (ιιο) → ιιιιιιιιιο
Param e2fd7.. : (ιιο) → ιιιιιιιιιο
Param 05a8c.. : (ιιο) → ιιιιιιιιιο
Param f5da9.. : (ιιο) → ιιιιιιιιιο
Param de118.. : (ιιο) → ιιιιιιιιιο
Param b43ab.. : (ιιο) → ιιιιιιιιιο
Param 627df.. : (ιιο) → ιιιιιιιιιο
Param c2e8a.. : (ιιο) → ιιιιιιιιιο
Param aa358.. : (ιιο) → ιιιιιιιιιο
Param 093ad.. : (ιιο) → ιιιιιιιιιο
Param bacd8.. : (ιιο) → ιιιιιιιιιο
Param 2bb2a.. : (ιιο) → ιιιιιιιιιο
Definition baafa.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0682ac.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x05f6ee.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a2b8b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e2fd7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x005a8c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f5da9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0de118.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b43ab.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0627df.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0c2e8a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0aa358.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0093ad.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0bacd8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02bb2a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)x2
Param 803e1.. : (ιιο) → ιιιιιιιιιο
Param f9a67.. : (ιιο) → ιιιιιιιιιο
Param 76a6c.. : (ιιο) → ιιιιιιιιιο
Param 7f17b.. : (ιιο) → ιιιιιιιιιο
Param cc7e8.. : (ιιο) → ιιιιιιιιιο
Param 3a6bc.. : (ιιο) → ιιιιιιιιιο
Param ad740.. : (ιιο) → ιιιιιιιιιο
Param 9aef0.. : (ιιο) → ιιιιιιιιιο
Param 30182.. : (ιιο) → ιιιιιιιιιο
Param d2a2c.. : (ιιο) → ιιιιιιιιιο
Param a94a5.. : (ιιο) → ιιιιιιιιιο
Param 92dea.. : (ιιο) → ιιιιιιιιιο
Param 8be9f.. : (ιιο) → ιιιιιιιιιο
Param 4e4f8.. : (ιιο) → ιιιιιιιιιο
Definition 4a24e.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0803e1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f9a67.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x076a6c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x07f17b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0cc7e8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x03a6bc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ad740.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x09aef0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x030182.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d2a2c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a94a5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x092dea.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x08be9f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x04e4f8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)x2
Param 37e04.. : (ιιο) → ιιιιιιιιιο
Param f7902.. : (ιιο) → ιιιιιιιιιο
Param ab042.. : (ιιο) → ιιιιιιιιιο
Param a2064.. : (ιιο) → ιιιιιιιιιο
Param 8c9ed.. : (ιιο) → ιιιιιιιιιο
Param ee649.. : (ιιο) → ιιιιιιιιιο
Param 61fc8.. : (ιιο) → ιιιιιιιιιο
Param ed012.. : (ιιο) → ιιιιιιιιιο
Param d68bd.. : (ιιο) → ιιιιιιιιιο
Param d0e1f.. : (ιιο) → ιιιιιιιιιο
Param 1e021.. : (ιιο) → ιιιιιιιιιο
Param 989b4.. : (ιιο) → ιιιιιιιιιο
Definition d8424.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x037e04.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f7902.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ab042.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a2064.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x08c9ed.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ee649.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x061fc8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ed012.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d68bd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d0e1f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x01e021.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0989b4.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)x2
Param 6e051.. : (ιιο) → ιιιιιιιιιο
Param d92ce.. : (ιιο) → ιιιιιιιιιο
Param e5063.. : (ιιο) → ιιιιιιιιιο
Param 228c9.. : (ιιο) → ιιιιιιιιιο
Param a3e51.. : (ιιο) → ιιιιιιιιιο
Param c705c.. : (ιιο) → ιιιιιιιιιο
Param 38793.. : (ιιο) → ιιιιιιιιιο
Param e13e5.. : (ιιο) → ιιιιιιιιιο
Param ef237.. : (ιιο) → ιιιιιιιιιο
Param 3c50c.. : (ιιο) → ιιιιιιιιιο
Definition b45a2.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x06e051.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0d92ce.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x061fc8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ed012.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e5063.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0228c9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a3e51.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0c705c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x038793.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e13e5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ef237.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x03c50c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)x2
Param 7cafd.. : (ιιο) → ιιιιιιιιιο
Param 72e0a.. : (ιιο) → ιιιιιιιιιο
Param a4abc.. : (ιιο) → ιιιιιιιιιο
Param a40ae.. : (ιιο) → ιιιιιιιιιο
Param b1702.. : (ιιο) → ιιιιιιιιιο
Param f444d.. : (ιιο) → ιιιιιιιιιο
Param 55a3e.. : (ιιο) → ιιιιιιιιιο
Param 8c70b.. : (ιιο) → ιιιιιιιιιο
Param 17819.. : (ιιο) → ιιιιιιιιιο
Param 53f52.. : (ιιο) → ιιιιιιιιιο
Param 07fce.. : (ιιο) → ιιιιιιιιιο
Param 86fe8.. : (ιιο) → ιιιιιιιιιο
Definition 41e30.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x07cafd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x072e0a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a4abc.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a40ae.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b1702.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f444d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x055a3e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x08c70b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x017819.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x053f52.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x007fce.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x086fe8.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)x2
Param fb47b.. : (ιιο) → ιιιιιιιιιο
Param 055d9.. : (ιιο) → ιιιιιιιιιο
Param 13b7c.. : (ιιο) → ιιιιιιιιιο
Param 2bf4d.. : (ιιο) → ιιιιιιιιιο
Param cf078.. : (ιιο) → ιιιιιιιιιο
Param a0d70.. : (ιιο) → ιιιιιιιιιο
Param 2e1d5.. : (ιιο) → ιιιιιιιιιο
Param 729bd.. : (ιιο) → ιιιιιιιιιο
Param e1aab.. : (ιιο) → ιιιιιιιιιο
Param 241b0.. : (ιιο) → ιιιιιιιιιο
Param 8fbce.. : (ιιο) → ιιιιιιιιιο
Param 6661c.. : (ιιο) → ιιιιιιιιιο
Definition 71717.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0fb47b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0055d9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x013b7c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02bf4d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0cf078.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a0d70.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x02e1d5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0729bd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e1aab.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0241b0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x08fbce.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x06661c.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)x2
Param a9907.. : (ιιο) → ιιιιιιιιιο
Param 824ef.. : (ιιο) → ιιιιιιιιιο
Param 8f55d.. : (ιιο) → ιιιιιιιιιο
Param 22bb5.. : (ιιο) → ιιιιιιιιιο
Param 654b9.. : (ιιο) → ιιιιιιιιιο
Param 53286.. : (ιιο) → ιιιιιιιιιο
Param b8d2a.. : (ιιο) → ιιιιιιιιιο
Param e5024.. : (ιιο) → ιιιιιιιιιο
Param f0823.. : (ιιο) → ιιιιιιιιιο
Definition ac29e.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0a9907.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0824ef.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x08f55d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x022bb5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0654b9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x053286.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0b8d2a.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0e5024.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0f0823.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)x2
Param 62e18.. : (ιιο) → ιιιιιιιιιο
Param 49901.. : (ιιο) → ιιιιιιιιιο
Param dc830.. : (ιιο) → ιιιιιιιιιο
Param ed1c7.. : (ιιο) → ιιιιιιιιιο
Param df50d.. : (ιιο) → ιιιιιιιιιο
Param 176ba.. : (ιιο) → ιιιιιιιιιο
Param 9f93b.. : (ιιο) → ιιιιιιιιιο
Param 91ca0.. : (ιιο) → ιιιιιιιιιο
Param 23b03.. : (ιιο) → ιιιιιιιιιο
Definition 00b44.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x062e18.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x049901.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0dc830.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0ed1c7.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0df50d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0176ba.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x09f93b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x091ca0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x023b03.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11x2)x2
Param 496a0.. : (ιιο) → ιιιιιιιιιο
Param 2ffc8.. : (ιιο) → ιιιιιιιιιο
Param e8ba7.. : (ιιο) → ιιιιιιιιιο
Param b4c31.. : (ιιο) → ιιιιιιιιιο
Param 1a9c5.. : (ιιο) → ιιιιιιιιιο
Param bfd4f.. : (ιιο) → ιιιιιιιιιο
Param d0980.. : (ιιο) → ιιιιιιιιιο
Param bc2c6.. : (ιιο) → ιιιιιιιιιο
Param 06d7e.. : (ιιο) → ιιιιιιιιιο
Param b0749.. : (ιιο) → ιιιιιιιιιο
Param 87273.. : (ιιο) → ιιιιιιιιιο
Param b0e38.. : (ιιο) → ιιιιιιιιιο
Param f3db6.. : (ιιο) → ιιιιιιιιιο
Param 21189.. : (ιιο) → ιιιιιιιιιο
Param d0e7c.. : (ιιο) → ιιιιιιιιιο
Param f630d.. : (ιιο) → ιιιιιιιιιο
Param 9a66e.. : (ιιο) → ιιιιιιιιιο
Param 93f0f.. : (ιιο) → ιιιιιιιιιο
Param 2dac5.. : (ιιο) → ιιιιιιιιιο
Param 3fca5.. : (ιιο) → ιιιιιιιιιο
Param ef324.. : (ιιο) → ιιιιιιιιιο
Param c4d5c.. : (ιιο) → ιιιιιιιιιο
Param dcb32.. : (ιιο) → ιιιιιιιιιο
Param d3618.. : (ιιο) → ιιιιιιιιιο
Param dbf71.. : (ιιο) → ιιιιιιιιιο
Param e37fb.. : (ιιο) → ιιιιιιιιιο
Param 78a44.. : (ιιο) → ιιιιιιιιιο
Param af5b6.. : (ιιο) → ιιιιιιιιιο
Param a7e88.. : (ιιο) → ιιιιιιιιιο
Param 59632.. : (ιιο) → ιιιιιιιιιο
Param 79ee1.. : (ιιο) → ιιιιιιιιιο
Param f6312.. : (ιιο) → ιιιιιιιιιο
Param fa2d0.. : (ιιο) → ιιιιιιιιιο
Param dd43e.. : (ιιο) → ιιιιιιιιιο
Param 4818f.. : (ιιο) → ιιιιιιιιιο
Param 4d3d7.. : (ιιο) → ιιιιιιιιιο
Param a1497.. : (ιιο) → ιιιιιιιιιο
Param 4086f.. : (ιιο) → ιιιιιιιιιο
Param 44916.. : (ιιο) → ιιιιιιιιιο
Param 8acce.. : (ιιο) → ιιιιιιιιιο
Param b47d4.. : (ιιο) → ιιιιιιιιιο
Param 74622.. : (ιιο) → ιιιιιιιιιο
Param 0788d.. : (ιιο) → ιιιιιιιιιο
Param fa661.. : (ιιο) → ιιιιιιιιιο
Param 255f4.. : (ιιο) → ιιιιιιιιιο
Param c8a3f.. : (ιιο) → ιιιιιιιιιο
Param 2bad0.. : (ιιο) → ιιιιιιιιιο
Param d2e51.. : (ιιο) → ιιιιιιιιιο
Param 76e3a.. : (ιιο) → ιιιιιιιιιο
Param 9eede.. : (ιιο) → ιιιιιιιιιο
Param ba960.. : (ιιο) → ιιιιιιιιιο
Param 74a95.. : (ιιο) → ιιιιιιιιιο
Param 59a16.. : (ιιο) → ιιιιιιιιιο
Param 94f0c.. : (ιιο) → ιιιιιιιιιο
Param 923e2.. : (ιιο) → ιιιιιιιιιο
Param 1b69c.. : (ιιο) → ιιιιιιιιιο
Param cec27.. : (ιιο) → ιιιιιιιιιο
Param 889b5.. : (ιιο) → ιιιιιιιιιο
Param 71ae3.. : (ιιο) → ιιιιιιιιιο
Param df026.. : (ιιο) → ιιιιιιιιιο
Param 6bc75.. : (ιιο) → ιιιιιιιιιο
Param 43a9d.. : (ιιο) → ιιιιιιιιιο
Param 4402e.. : ι(ιιο) → ο
Param cf2df.. : ι(ιιο) → ο
Param SubqSubq : ιιο
Param setminussetminus : ιιι
Param SingSing : ιι
Param 5bab1.. : ι(ιιο) → ο
Known 70d6f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x34006a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 5e8a4.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3fc090.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 629c2.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x307c0f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 58605.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x00076f.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12∀ x13 : ο . x13
Known 176e1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3adf05.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 13c6c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3d5d69.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 158a2.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x33f98b.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 0a416.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x396c31.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 3d567.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x354c7d.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known be036.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3130d9.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 6110e.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x34e6fe.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 1b89c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3a62c3.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known bf274.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3ceccf.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known d3d64.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3eb506.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 79b20.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x370755.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 86d7f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x397793.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 4ee2c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3aa64f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 53ca8.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x383aec.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 7cfa2.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3446f4.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Theorem d1f46.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)eecee.. x3 x15bab1.. x0 x1 (proof)
Known 5f7f8.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3ba015.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 3bdc3.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3286f8.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known b5e39.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x32c550.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known b5546.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3f842a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known fbeda.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3e9fc9.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known d4e03.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3010eb.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 2bcde.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3fa0f3.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 3701a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3c7001.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known c6ec1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x358722.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 43aa1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x384d91.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known f056c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x390d0e.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known cc277.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x381d98.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Theorem aed67.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)967cf.. x3 x15bab1.. x0 x1 (proof)
Known 93821.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x330a11.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known c0ca2.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3076b3.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 30b69.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x33d3e7.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 8896c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x314be0.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 5fe79.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x34e91d.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 73125.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x323b40.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 501e3.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x31a9fd.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known dda92.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3e2ec9.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 890d1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3c480f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 6c8b0.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x30db75.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 7b02f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x302471.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 01e8a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x31cf57.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 6ef3d.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x023926.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12∀ x13 : ο . x13
Known 33589.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3b19dd.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 610e2.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x32eb4b.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 3603f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3bce5f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known c97cd.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x373f36.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 03628.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x394ee4.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Theorem 53b4c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)0ee54.. x3 x15bab1.. x0 x1 (proof)
Known d9493.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3811c0.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 2ab05.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x396162.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 8311a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x30768d.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 5c6d8.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x370a3c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 8dd80.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x32122d.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 4eecf.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x339c17.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 45a6b.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3ee5b5.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 1a30f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x361b2a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 60271.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3abda1.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 10aef.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3858d1.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Theorem 2a49e.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)a7092.. x3 x15bab1.. x0 x1 (proof)
Known 48184.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x322b3a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known c2b39.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3723e0.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 2609f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x31ecf8.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 601fe.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3915dd.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known ee62a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x358208.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 7751a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3b571f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known bfd15.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x37e5de.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 49425.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3a3794.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known f59a2.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3093ca.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known a215a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x334ae8.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known fbefa.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x365996.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 3128c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x345286.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known c85e7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3b7a83.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 8ac5c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x372d65.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known a2a87.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3b7e1a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 25eec.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x34b4dd.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known e1218.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3f4940.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Theorem ae354.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)b2a9d.. x3 x15bab1.. x0 x1 (proof)
Known 7c684.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3682ac.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known cd34a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x35f6ee.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known abb14.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3a2b8b.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 5b367.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3e2fd7.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known eb730.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x305a8c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 34f71.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3f5da9.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 76878.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3de118.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 10e7e.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3b43ab.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known b611a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3627df.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 20343.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3c2e8a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 33bd7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3aa358.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known bdaf9.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3093ad.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 6b571.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3bacd8.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known b257d.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x32bb2a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Theorem c9b7d.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)baafa.. x3 x15bab1.. x0 x1 (proof)
Known bec8c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3803e1.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known cfa25.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0f9a67.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12∀ x13 : ο . x13
Known 71413.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x376a6c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known dabf4.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x37f17b.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 37e36.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0cc7e8.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12∀ x13 : ο . x13
Known e4093.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x33a6bc.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 09b2e.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3ad740.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known e2fb1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x39aef0.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 9f530.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x330182.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known e8ce3.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3d2a2c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known ec1a1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3a94a5.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 858e2.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x392dea.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known ba3e4.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x38be9f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 3a6fa.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x34e4f8.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Theorem 2bc58.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)4a24e.. x3 x15bab1.. x0 x1 (proof)
Known 9efdc.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x337e04.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 2b542.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3f7902.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known dba82.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3ab042.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 65889.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3a2064.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known cbc05.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x38c9ed.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 9ae9f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3ee649.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 29dfb.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x361fc8.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 79a4a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3ed012.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known fd91f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3d68bd.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 9ce00.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3d0e1f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known d030a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x31e021.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known c4aa8.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3989b4.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Theorem 0733b.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)d8424.. x3 x15bab1.. x0 x1 (proof)
Known 2d870.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x36e051.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 5e6fc.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3d92ce.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 909ba.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3e5063.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known ee588.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3228c9.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 586ac.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3a3e51.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 12ea2.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3c705c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known c2878.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x338793.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 08dcf.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3e13e5.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 39b5d.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3ef237.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 232fb.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x33c50c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Theorem 4b75a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)b45a2.. x3 x15bab1.. x0 x1 (proof)
Known 2c539.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x37cafd.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 5d08d.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x372e0a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 96398.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3a4abc.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 75d70.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3a40ae.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known ff971.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3b1702.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 5d299.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3f444d.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 53960.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x355a3e.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known c89cc.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x38c70b.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known c0798.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x317819.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 58d86.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x353f52.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known b5648.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x307fce.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 35f3a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x386fe8.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Theorem 728cd.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)41e30.. x3 x15bab1.. x0 x1 (proof)
Known d9009.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3fb47b.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known ef619.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3055d9.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known cf092.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x313b7c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 275da.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x32bf4d.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 366b5.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3cf078.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 6bfe2.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3a0d70.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 17f14.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x32e1d5.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known a13e6.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3729bd.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 3104d.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3e1aab.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 0bc50.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3241b0.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known a0ecc.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x38fbce.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 4fc57.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x36661c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Theorem 62d9a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)71717.. x3 x15bab1.. x0 x1 (proof)
Known 73bf7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3a9907.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known f116f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3824ef.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 6f2ec.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x38f55d.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 2e3f7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x322bb5.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 8513d.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3654b9.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known bdbea.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x353286.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known a72a1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3b8d2a.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 684fa.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3e5024.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known ad3e5.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3f0823.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Theorem 25794.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)ac29e.. x3 x15bab1.. x0 x1 (proof)
Known 7a927.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x362e18.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 4de8c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x349901.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 64b81.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3dc830.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known f43e6.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ed1c7.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12∀ x13 : ο . x13
Known 3acb2.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3df50d.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known cd9af.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3176ba.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known afd8e.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x39f93b.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 4e454.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x391ca0.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 68054.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x323b03.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Theorem 033e1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)00b44.. x3 x15bab1.. x0 x1 (proof)
Known 75ae5.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3496a0.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 774bc.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x32ffc8.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 128ce.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3e8ba7.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 22120.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3b4c31.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known d08d7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x31a9c5.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 8fa6b.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3bfd4f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 9ce91.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3d0980.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1
Known 09417.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3bc2c6.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x125bab1.. x0 x1