((a0 = ":" & P5)
      & 
     (a0 = "p2" & P3) & 
     (a0 = "p1" & P3) & (a0 = "E" & P6)
      & (
     a0 = "=" & P6) & (a0 = "=/="
      & P0) & 
     (a0 = "<-" & P0)
      & 
     (a0 = "==" & P0) & 
     (a0 = "->" & P0) & (a0 = "v" & P0)
      & (
     a0 = "&" & P0) & (a0 = "Half"
      & P1) & 
     (a0 = "Two" & P1)
      & 
     (a0 = "Three" & P1) & 
     (a0 = "Projtwo" & P3) & 
     (a0 = "Si" & P3)
      & 
     (a0 = "Kpair" & P5) & 
     (a0 = "Couple" & P5) & 
     (a0 = "Sing" & P3)
      & 
     (a0 = "Union" & P5) & 
     (a0 = "Closure" & P5) & 
     (a0 = "Reals" & P1)
      & 
     (a0 = "Nat" & P1) & 
     (a0 = "Sup" & P3) & 
     (a0 = "Inv" & P3)
      & 
     (a0 = "Minus" & P3) & 
     (a0 = "*" & P5) & (a0 = "+" & P5)
      & (
     a0 = "One" & P1) & (
     a0 = "Zero" & P1) & (
     a0 = "An" & P3)
      & (
     a0 = "Sequence" & P4) & (
     a0 = "Function" & P6) & (
     a0 = "<=" & P6)
      & (
     a0 = "Equal" & P6) & (
     a0 = "<" & P6) & (a0 = "Real"
      & P4) & P0)
      & 
     (
     (a0 = "L" & P1) & (a0 = "" & P2)
      & (
     a0 = "E" & P0) & 
     (a0 = "A" & P0) & P0) & (
     (a0 = "Kpair" & P0) & 
     (a0 = "Couple" & P0)
      & 
     (a0 = "Union" & P0) & 
     (a0 = "Closure" & P0)
      & 
     (a0 = "*" & P2) & (a0 = "+" & P0)
      & (
     a0 = "=/=" & P0) & (a0 = "<-"
      & P4)
      & 
     (a0 = "==" & P0) & 
     (a0 = "->" & P4)
      & (a0 = "v" & P6) & (
     a0 = "&" & P8) & P0) & ((
     a0 = ":"
      & P0 & P0 & P1 & P0) & (
     a0 = ","
      & P0 & P0 & P0 & P0)
      & (
     a0 = "p2" & P0 & P0 & P0) & (
     a0 = "p1" & P0 & P0 & P0) & (
     a0 = "=" & P0 & P0 & P0) & (
     a0 = "E" & P0 & P1 & P0) & (
     a0 = "Half" & P0)
      & (
     a0 = "Two" & P0) & (
     a0 = "Three" & P0) & (
     a0 = "Projtwo" & P1 & P0) & (
     a0 = "Si" & P1 & P0) & (
     a0 = "Kpair"
      & P0 & P0 & P0)
      & (
     a0 = "Couple"
      & P0 & P0 & P0) & (
     a0 = "Sing" & P0 & P0) & (
     a0 = "Union"
      & P0 & P0 & P0) & (
     a0 = "Closure"
      & P0 & P1 & P0) & (
     a0 = "Sequence" & P1 & P0)
      & (
     a0 = "Reals" & P0) & (
     a0 = "Function"
      & P1 & P1 & P0) & (
     a0 = "Nat" & P0) & 
     (a0 = "<=" & 
     P0 & P0 & P0) & (a0 = "Equal"
      & P0 & P0 & P0)
      & (
     a0 = "Sup" & P0 & P1 & P0) & (
     a0 = "Inv" & P0 & P0 & P0) & (
     a0 = "Minus"
      & P0 & P0 & P0) & 
     (a0 = "<" & 
     P0 & P0 & P0) & 
     (a0 = "*" & P0
      & P0 & P0 & P0)
      & 
     (a0 = "+" & P0
      & P0 & P0 & P0) & 
     (a0 = "One" & P0 & P0) & (a0 = "Zero"
      & P0 & P0) & (a0 = "Real"
      & P0 & P0) & (a0 = "An" & P0
      & P1 & P0)
      & P0) & (
     (a0 = "" & P1 & P0
      & P0 & P0)
      & (a0 = "E"
      & P0 & P0 & P0) & 
     (a0 = "A" & 
     P0 & P0 & P0) & P0) & (
     a0 = "SUP2" & a0 = "SUP1"
      & a0 = "MTIMES" & 
     a0 = "MPLUS0"
      & a0 = "TRANS" & a0 = "TRI"
      & a0 = "IRR" & 
     a0 = "NONTRIV" & a0 = "INV"
      & a0 = "MINUS" & 
     a0 = "ITIMES" & a0 = "IPLUS"
      & a0 = "DIST" & 
     a0 = "ATIMES" & a0 = "APLUS"
      & a0 = "CTIMES" & 
     a0 = "CPLUS" & a0 = "RSUP"
      & a0 = "RINV" & 
     a0 = "RMINUS" & a0 = "RTIMES"
      & a0 = "RPLUS" & 
     a0 = "AN" & P0)
      & P0
\