HomeHome Metamath Proof Explorer
Theorem List (p. 231 of 313)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-21423)
  Hilbert Space Explorer  Hilbert Space Explorer
(21424-22946)
  Users' Mathboxes  Users' Mathboxes
(22947-31284)
 

Theorem List for Metamath Proof Explorer - 23001-23100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremballotlemieq 23001* If two countings share the same first tie, they also have the same swap function. (Contributed by Thierry Arnoux, 18-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  D  e.  ( O  \  E )  /\  ( I `  C )  =  ( I `  D ) )  ->  ( S `  C )  =  ( S `  D ) )
 
Theoremballotlemrval 23002* Value of  R. (Contributed by Thierry Arnoux, 14-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( R `  C )  =  ( ( S `
  C ) " C ) )
 
Theoremballotlemscr 23003* The image of  ( R `  C ) by  ( S `  C ) (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( ( S `  C ) " ( R `  C ) )  =  C )
 
Theoremballotlemrv 23004* Value of  R evaluated at  J. (Contributed by Thierry Arnoux, 17-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( M  +  N ) ) ) 
 ->  ( J  e.  ( R `  C )  <->  if ( J  <_  ( I `  C ) ,  ( ( ( I `  C )  +  1 )  -  J ) ,  J )  e.  C )
 )
 
Theoremballotlemrv1 23005* Value of  R before the tie. (Contributed by Thierry Arnoux, 11-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( M  +  N ) )  /\  J  <_  ( I `  C ) )  ->  ( J  e.  ( R `  C )  <->  ( ( ( I `  C )  +  1 )  -  J )  e.  C ) )
 
Theoremballotlemrv2 23006* Value of  R after the tie. (Contributed by Thierry Arnoux, 11-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( M  +  N ) )  /\  ( I `  C )  <  J )  ->  ( J  e.  ( R `  C )  <->  J  e.  C ) )
 
Theoremballotlemro 23007* Range of  R is included in  O. (Contributed by Thierry Arnoux, 17-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( R `  C )  e.  O )
 
Theoremballotlemgval 23008* Expand the value of  .^. (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( ( U  e.  Fin  /\  V  e.  Fin )  ->  ( U  .^  V )  =  ( ( # `
  ( V  i^i  U ) )  -  ( # `
  ( V  \  U ) ) ) )
 
Theoremballotlemgun 23009* A property of the defined  .^ operator (Contributed by Thierry Arnoux, 26-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   &    |-  ( ph  ->  U  e.  Fin )   &    |-  ( ph  ->  V  e.  Fin )   &    |-  ( ph  ->  W  e.  Fin )   &    |-  ( ph  ->  ( V  i^i  W )  =  (/) )   =>    |-  ( ph  ->  ( U  .^  ( V  u.  W ) )  =  ( ( U  .^  V )  +  ( U  .^  W ) ) )
 
Theoremballotlemfg 23010* Express the value of  ( F `  C
) in terms of  .^. (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 0 ... ( M  +  N ) ) ) 
 ->  ( ( F `  C ) `  J )  =  ( C  .^  ( 1 ... J ) ) )
 
Theoremballotlemfrc 23011* Express the value of  ( F `  ( R `  C )
) in terms of the newly defined  .^. (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( I `  C ) ) ) 
 ->  ( ( F `  ( R `  C ) ) `  J )  =  ( C  .^  ( ( ( S `
  C ) `  J ) ... ( I `  C ) ) ) )
 
Theoremballotlemfrci 23012* Reverse counting preserves a tie at the first tie. (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( ( F `  ( R `  C ) ) `  ( I `
  C ) )  =  0 )
 
Theoremballotlemfrceq 23013* Value of  F for a reverse counting  ( R `  C ). (Contributed by Thierry Arnoux, 27-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( I `  C ) ) ) 
 ->  ( ( F `  C ) `  (
 ( ( S `  C ) `  J )  -  1 ) )  =  -u ( ( F `
  ( R `  C ) ) `  J ) )
 
Theoremballotlemfrcn0 23014* Value of  F for a reversed counting  ( R `  C ), before the first tie, cannot be zero . (Contributed by Thierry Arnoux, 25-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( M  +  N ) )  /\  J  <  ( I `  C ) )  ->  ( ( F `  ( R `  C ) ) `  J )  =/=  0 )
 
Theoremballotlemrc 23015* Range of  R. (Contributed by Thierry Arnoux, 19-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( R `  C )  e.  ( O  \  E ) )
 
Theoremballotlemirc 23016* Applying  R does not change first ties. (Contributed by Thierry Arnoux, 19-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( I `  ( R `
  C ) )  =  ( I `  C ) )
 
Theoremballotlemrinv0 23017* Lemma for ballotlemrinv 23018. (Contributed by Thierry Arnoux, 18-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  D  =  ( ( S `  C ) " C ) ) 
 ->  ( D  e.  ( O  \  E )  /\  C  =  ( ( S `  D ) " D ) ) )
 
Theoremballotlemrinv 23018*  R is its own inverse : it is an involution. (Contributed by Thierry Arnoux, 10-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  `' R  =  R
 
Theoremballotlem1ri 23019* When the vote on the first tie is for A, the first vote is also for A on the reverse counting. (Contributed by Thierry Arnoux, 18-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( 1  e.  ( R `  C )  <->  ( I `  C )  e.  C ) )
 
Theoremballotlem7 23020*  R is a bijection between two subsets of  ( O  \  E
): one where a vote for A is picked first, and one where a vote for B is picked first (Contributed by Thierry Arnoux, 12-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( R  |`  { c  e.  ( O  \  E )  |  1  e.  c } ) : {
 c  e.  ( O 
 \  E )  |  1  e.  c } -1-1-onto-> {
 c  e.  ( O 
 \  E )  |  -.  1  e.  c }
 
Theoremballotlem8 23021* There are as many countings with ties starting with a ballot for A as there are starting with a ballot for B. (Contributed by Thierry Arnoux, 7-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( # `  { c  e.  ( O  \  E )  |  1  e.  c } )  =  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } )
 
Theoremballotth 23022* Bertrand's ballot problem : the probability that A is ahead throughout the counting. (Contributed by Thierry Arnoux, 7-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( P `  E )  =  ( ( M  -  N )  /  ( M  +  N ) )
 
16.4  Mathbox for Mario Carneiro
 
16.4.1  Miscellaneous stuff
 
Theoremquartfull 23023 The quartic equation, written out in full. This actually makes a fairly good Metamath stress test. Note that the length of this formula could be shortened significantly if the intermediate expressions were expanded and simplified, but it's not like this theorem will be used anyway. (Contributed by Mario Carneiro, 6-May-2015.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   &    |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  ( ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) )  =/=  0 )   &    |-  ( ph  ->  -u ( ( ( ( 2  x.  ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) )  +  ( ( ( ( ( -u (
 2  x.  ( ( B  -  ( ( 3  /  8 )  x.  ( A ^
 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 )  =/=  0 )   =>    |-  ( ph  ->  ( ( ( ( X ^ 4
 )  +  ( A  x.  ( X ^
 3 ) ) )  +  ( ( B  x.  ( X ^
 2 ) )  +  ( ( C  x.  X )  +  D ) ) )  =  0  <->  ( ( X  =  ( ( -u ( A  /  4
 )  -  ( ( sqr `  -u ( ( ( ( 2  x.  ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) )  +  ( sqr `  ( ( -u ( ( ( sqr `  -u ( ( ( ( 2  x.  ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) )  +  ( ( ( ( ( -u (
 2  x.  ( ( B  -  ( ( 3  /  8 )  x.  ( A ^
 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) ^ 2 )  -  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  / 
 2 ) )  +  ( ( ( ( C  -  ( ( A  x.  B ) 
 /  2 ) )  +  ( ( A ^ 3 )  / 
 8 ) )  / 
 4 )  /  (
 ( sqr `  -u ( ( ( ( 2  x.  ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) ) ) ) )  \/  X  =  ( ( -u ( A  /  4 )  -  ( ( sqr `  -u (
 ( ( ( 2  x.  ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) )  -  ( sqr `  ( ( -u ( ( ( sqr `  -u ( ( ( ( 2  x.  ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) )  +  ( ( ( ( ( -u (
 2  x.  ( ( B  -  ( ( 3  /  8 )  x.  ( A ^
 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) ^ 2 )  -  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  / 
 2 ) )  +  ( ( ( ( C  -  ( ( A  x.  B ) 
 /  2 ) )  +  ( ( A ^ 3 )  / 
 8 ) )  / 
 4 )  /  (
 ( sqr `  -u ( ( ( ( 2  x.  ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) ) ) ) ) )  \/  ( X  =  ( ( -u ( A  /  4
 )  +  ( ( sqr `  -u ( ( ( ( 2  x.  ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) )  +  ( sqr `  ( ( -u ( ( ( sqr `  -u ( ( ( ( 2  x.  ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) )  +  ( ( ( ( ( -u (
 2  x.  ( ( B  -  ( ( 3  /  8 )  x.  ( A ^
 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) ^ 2 )  -  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  / 
 2 ) )  -  ( ( ( ( C  -  ( ( A  x.  B ) 
 /  2 ) )  +  ( ( A ^ 3 )  / 
 8 ) )  / 
 4 )  /  (
 ( sqr `  -u ( ( ( ( 2  x.  ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) ) ) ) )  \/  X  =  ( ( -u ( A  /  4 )  +  ( ( sqr `  -u (
 ( ( ( 2  x.  ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( (