formulaNormalisationRules.key

Sorts

G

\generic G;defined in: formulaNormalisationRules.key Line: 10 Offset :4

H

\generic H;defined in: formulaNormalisationRules.key Line: 11 Offset :4

I

\generic I;defined in: formulaNormalisationRules.key Line: 12 Offset :4

subG

\generic subG \extends G ;defined in: formulaNormalisationRules.key Line: 13 Offset :4

NonSingleton

\generic NonSingleton \oneof {int \generic NonSingleton \oneof {int , boolean \generic NonSingleton \oneof {int \generic NonSingleton \oneof {int , boolean };

defined in: formulaNormalisationRules.key Line: 14 Offset :4

Taclets

No choice condition specified

eq_imp

eq_imp  {
\find (                    phi ->                phi )
  \replacewith (                    true )
\heuristics  (concrete )

};

defined in: formulaNormalisationRules.key Line: 50 Offset :4

eq_and

eq_and  {
\find (                    phi &             phi )
  \replacewith (                    phi )
\heuristics  (concrete )

};

defined in: formulaNormalisationRules.key Line: 56 Offset :4

eq_and_2

eq_and_2  {
\find (                   (                   psi &             phi )&             phi )
  \replacewith (                    psi &             phi )
\heuristics  (concrete )

};

defined in: formulaNormalisationRules.key Line: 62 Offset :4

eq_or

eq_or  {
\find (                    phi |              phi )
  \replacewith (                    phi )
\heuristics  (concrete )

};

defined in: formulaNormalisationRules.key Line: 68 Offset :4

eq_or_2

eq_or_2  {
\find (                   (                   psi |              phi )|              phi )
  \replacewith (                    psi |              phi )
\heuristics  (concrete )

};

defined in: formulaNormalisationRules.key Line: 74 Offset :4

eq_eq

eq_eq  {
\find (                    phi <->                phi )
  \replacewith (                    true )
\heuristics  (concrete )

};

defined in: formulaNormalisationRules.key Line: 80 Offset :4

neq_and

neq_and  {
\find (                    phi &            (         !             phi ))
  \replacewith (                    false )
\heuristics  (concrete )

};

defined in: formulaNormalisationRules.key Line: 86 Offset :4

neq_and_2

neq_and_2  {
\find (                   (         !             phi )&             phi )
  \replacewith (                    false )
\heuristics  (concrete )

};

defined in: formulaNormalisationRules.key Line: 92 Offset :4

neq_and_3

neq_and_3  {
\find (                   (                   psi &             phi )&            (         !             phi ))
  \replacewith (                    false )
\heuristics  (concrete )

};

defined in: formulaNormalisationRules.key Line: 98 Offset :4

neq_and_4

neq_and_4  {
\find (                   (                   psi &            (         !             phi ))&             phi )
  \replacewith (                    false )
\heuristics  (concrete )

};

defined in: formulaNormalisationRules.key Line: 104 Offset :4

neq_or

neq_or  {
\find (                    phi |             (         !             phi ))
  \replacewith (                    true )
\heuristics  (concrete )

};

defined in: formulaNormalisationRules.key Line: 110 Offset :4

neq_or_2

neq_or_2  {
\find (                   (         !             phi )|              phi )
  \replacewith (                    true )
\heuristics  (concrete )

};

defined in: formulaNormalisationRules.key Line: 116 Offset :4

neq_or_3

neq_or_3  {
\find (                   (                   psi |              phi )|             (         !             phi ))
  \replacewith (                    true )
\heuristics  (concrete )

};

defined in: formulaNormalisationRules.key Line: 122 Offset :4

neq_or_4

neq_or_4  {
\find (                   (                   psi |             (         !             phi ))|              phi )
  \replacewith (                    true )
\heuristics  (concrete )

};

defined in: formulaNormalisationRules.key Line: 128 Offset :4

nnf_ex2all

nnf_ex2all  {
\find ( ==>           \exists    u ;             phi )
  \replacewith (          \forall    u ;            (         !             phi )==>  )
\heuristics  (moveQuantToLeft , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 136 Offset :4

nnf_imp2or

nnf_imp2or  {
\find (                    phi ->                psi )
  \replacewith (                   (         !             phi )|              psi )
\heuristics  (negationNormalForm , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 142 Offset :4

nnf_notAll

nnf_notAll  {
\find (          !            (         \forall    u ;             phi ))
  \replacewith (          \exists    u ;            (         !             phi ))
\heuristics  (negationNormalForm , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 148 Offset :4

nnf_notEx

nnf_notEx  {
\find (          !            (         \exists    u ;             phi ))
  \replacewith (          \forall    u ;            (         !             phi ))
\heuristics  (negationNormalForm , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 154 Offset :4

nnf_notOr

nnf_notOr  {
\find (          !            (                   phi |              psi ))
  \replacewith (                   (         !             phi )&            (         !             psi ))
\heuristics  (negationNormalForm , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 160 Offset :4

nnf_notAnd

nnf_notAnd  {
\find (          !            (                   phi &             psi ))
  \replacewith (                   (         !             phi )|             (         !             psi ))
\heuristics  (negationNormalForm , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 166 Offset :4

nnf_notEqv

nnf_notEqv  {
\find (          !            (                   phi <->                psi ))
  \replacewith (                    phi <->      !             psi )
\heuristics  (negationNormalForm , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 172 Offset :4

applyEq_and_gen0

applyEq_and_gen0  {
\find (                    applyEqLeft =           applyEqOther &             applyEqLeft =           applyEqRight )
  \replacewith (                    applyEqRight =           applyEqOther &             applyEqLeft =           applyEqRight )
\heuristics  (apply_equations_andOr )

};

defined in: formulaNormalisationRules.key Line: 180 Offset :4

applyEq_and_gen1

applyEq_and_gen1  {
\find (                   (                   b &             applyEqLeft =           applyEqOther )&             applyEqLeft =           applyEqRight )
  \replacewith (                   (                   b &             applyEqRight =           applyEqOther )&             applyEqLeft =           applyEqRight )
\heuristics  (apply_equations_andOr )

};

defined in: formulaNormalisationRules.key Line: 188 Offset :4

applyEq_and_gen2

applyEq_and_gen2  {
\find (                    applyEqLeft !=           applyEqOther &             applyEqLeft =           applyEqRight )
  \replacewith (                    applyEqRight !=           applyEqOther &             applyEqLeft =           applyEqRight )
\heuristics  (apply_equations_andOr )

};

defined in: formulaNormalisationRules.key Line: 196 Offset :4

applyEq_and_gen3

applyEq_and_gen3  {
\find (                   (                   b &             applyEqLeft !=           applyEqOther )&             applyEqLeft =           applyEqRight )
  \replacewith (                   (                   b &             applyEqRight !=           applyEqOther )&             applyEqLeft =           applyEqRight )
\heuristics  (apply_equations_andOr )

};

defined in: formulaNormalisationRules.key Line: 204 Offset :4

applyEq_or_gen0

applyEq_or_gen0  {
\find (                    applyEqLeft =           applyEqOther |              applyEqLeft !=           applyEqRight )
  \replacewith (                    applyEqRight =           applyEqOther |              applyEqLeft !=           applyEqRight )
\heuristics  (apply_equations_andOr )

};

defined in: formulaNormalisationRules.key Line: 212 Offset :4

applyEq_or_gen1

applyEq_or_gen1  {
\find (                   (                   b |              applyEqLeft =           applyEqOther )|              applyEqLeft !=           applyEqRight )
  \replacewith (                   (                   b |              applyEqRight =           applyEqOther )|              applyEqLeft !=           applyEqRight )
\heuristics  (apply_equations_andOr )

};

defined in: formulaNormalisationRules.key Line: 220 Offset :4

applyEq_or_gen2

applyEq_or_gen2  {
\find (                    applyEqLeft !=           applyEqOther |              applyEqLeft !=           applyEqRight )
  \replacewith (                    applyEqRight !=           applyEqOther |              applyEqLeft !=           applyEqRight )
\heuristics  (apply_equations_andOr )

};

defined in: formulaNormalisationRules.key Line: 228 Offset :4

applyEq_or_gen3

applyEq_or_gen3  {
\find (                   (                   b |              applyEqLeft !=           applyEqOther )|              applyEqLeft !=           applyEqRight )
  \replacewith (                   (                   b |              applyEqRight !=           applyEqOther )|              applyEqLeft !=           applyEqRight )
\heuristics  (apply_equations_andOr )

};

defined in: formulaNormalisationRules.key Line: 236 Offset :4

shift_paren_and

shift_paren_and  {
\find (                    assoc0 &            (                   assoc1 &             assoc2 ))
  \replacewith (                   (                   assoc0 &             assoc1 )&             assoc2 )
\heuristics  (conjNormalForm , cnf_andAssoc )

};

defined in: formulaNormalisationRules.key Line: 246 Offset :4

shift_paren_or

shift_paren_or  {
\find (                    assoc0 |             (                   assoc1 |              assoc2 ))
  \replacewith (                   (                   assoc0 |              assoc1 )|              assoc2 )
\heuristics  (conjNormalForm , cnf_orAssoc )

};

defined in: formulaNormalisationRules.key Line: 253 Offset :4

commute_and

commute_and  {
\find (                    commLeft &             commRight )
  \replacewith (                    commRight &             commLeft )
\heuristics  (conjNormalForm , cnf_andComm )

};

defined in: formulaNormalisationRules.key Line: 260 Offset :4

commute_and_2

commute_and_2  {
\find (                   (                   commResidue &             commLeft )&             commRight )
  \replacewith (                   (                   commResidue &             commRight )&             commLeft )
\heuristics  (conjNormalForm , cnf_andComm )

};

defined in: formulaNormalisationRules.key Line: 266 Offset :4

commute_or

commute_or  {
\find (                    commLeft |              commRight )
  \replacewith (                    commRight |              commLeft )
\heuristics  (conjNormalForm , cnf_orComm )

};

defined in: formulaNormalisationRules.key Line: 272 Offset :4

commute_or_2

commute_or_2  {
\find (                   (                   commResidue |              commLeft )|              commRight )
  \replacewith (                   (                   commResidue |              commRight )|              commLeft )
\heuristics  (conjNormalForm , cnf_orComm )

};

defined in: formulaNormalisationRules.key Line: 278 Offset :4

cnf_rightDist

cnf_rightDist  {
\find (                    distLeft |             (                   distRight0 &             distRight1 ))
  \replacewith (                   (                   distLeft |              distRight0 )&            (                   distRight1 |              distLeft ))
\heuristics  (conjNormalForm , cnf_dist )

};

defined in: formulaNormalisationRules.key Line: 284 Offset :4

local_cut

local_cut  {
\find (                    phi )
  \replacewith (                   (         !             psi |              phi )&            (                   psi |              phi ))

};

defined in: formulaNormalisationRules.key Line: 291 Offset :4

cnf_eqv

cnf_eqv  {
\find (                    phi <->                psi )
  \replacewith (                   (                   phi |    !             psi )&            (         !             phi |              psi ))
\heuristics  (conjNormalForm , cnf_expandIfThenElse , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 296 Offset :4

ifthenelse_to_or_left

ifthenelse_to_or_left  {
\find (                   \if (                   phi )\then (                   then )\else (                   else )=           t )
  \replacewith (                   (         !             phi |              then =           t )&            (                   phi |              else =           t ))
\heuristics  (conjNormalForm , cnf_expandIfThenElse , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 303 Offset :4

ifthenelse_to_or_left2

ifthenelse_to_or_left2  {
\find (                   \if (                   phi )\then (                   then )\else (                   else )!=           t )
  \replacewith (                   (         !             phi |              then !=           t )&            (                   phi |              else !=           t ))
\heuristics  (conjNormalForm , cnf_expandIfThenElse , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 309 Offset :4

ifthenelse_to_or_right

ifthenelse_to_or_right  {
\find (                    t =          \if (                   phi )\then (                   then )\else (                   else ))
  \replacewith (                   (         !             phi |              t =           then )&            (                   phi |              t =           else ))
\heuristics  (conjNormalForm , cnf_expandIfThenElse , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 315 Offset :4

ifthenelse_to_or_right2

ifthenelse_to_or_right2  {
\find (                    t !=          \if (                   phi )\then (                   then )\else (                   else ))
  \replacewith (                   (         !             phi |              t !=           then )&            (                   phi |              t !=           else ))
\heuristics  (conjNormalForm , cnf_expandIfThenElse , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 321 Offset :4

ifthenelse_to_or_for

ifthenelse_to_or_for  {
\find (                   \if (                   phi )\then (                   b )\else (                   c ))
  \replacewith (                   (         !             phi |              b )&            (                   phi |              c ))
\heuristics  (conjNormalForm , cnf_expandIfThenElse , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 327 Offset :4

ifthenelse_to_or_for2

ifthenelse_to_or_for2  {
\find (          !            (                  \if (                   phi )\then (                   b )\else (                   c )))
  \replacewith (                   (         !             phi |    !             b )&            (                   phi |    !             c ))
\heuristics  (conjNormalForm , cnf_expandIfThenElse , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 333 Offset :4

elim_forall0

elim_forall0  {
\find (          \forall    Gvar ;            (                   Gvar !=           subGterm ))
\varcond   \replacewith (                    false )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 341 Offset :4

elim_forall1

elim_forall1  {
\find (          \forall    Gvar ;            (                   subGterm !=           Gvar ))
\varcond   \replacewith (                    false )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 348 Offset :4

elim_forall2

elim_forall2  {
\find (          \forall    Gvar ;            (                   Gvar !=           Hterm ))
\varcond   \replacewith (                   G ::  instance   (                   Hterm )=           FALSE )
\heuristics  (elimQuantifier , elimQuantifierWithCast )

};

defined in: formulaNormalisationRules.key Line: 355 Offset :4

elim_forall3

elim_forall3  {
\find (          \forall    Gvar ;            (                   Hterm !=           Gvar ))
\varcond   \replacewith (                   G ::  instance   (                   Hterm )=           FALSE )
\heuristics  (elimQuantifier , elimQuantifierWithCast )

};

defined in: formulaNormalisationRules.key Line: 362 Offset :4

elim_forall4

elim_forall4  {
\find (          \forall    Gvar ;            (                   phi |              Gvar !=           subGterm ))
\varcond   \replacewith (                {\subst   Gvar ;           subGterm }      phi )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 369 Offset :4

elim_forall5

elim_forall5  {
\find (          \forall    Gvar ;            (                   phi |              subGterm !=           Gvar ))
\varcond   \replacewith (                {\subst   Gvar ;           subGterm }      phi )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 376 Offset :4

elim_forall6

elim_forall6  {
\find (          \forall    Gvar ;            (                   phi |              Gvar !=           Hterm ))
\varcond   \replacewith (                   (               {\subst   Gvar ;       (G )      Hterm }      phi )|             G ::  instance   (                   Hterm )=           FALSE )
\heuristics  (elimQuantifier , elimQuantifierWithCast )

};

defined in: formulaNormalisationRules.key Line: 383 Offset :4

elim_forall7

elim_forall7  {
\find (          \forall    Gvar ;            (                   phi |              Hterm !=           Gvar ))
\varcond   \replacewith (                   (               {\subst   Gvar ;       (G )      Hterm }      phi )|             G ::  instance   (                   Hterm )=           FALSE )
\heuristics  (elimQuantifier , elimQuantifierWithCast )

};

defined in: formulaNormalisationRules.key Line: 391 Offset :4

elim_forall8

elim_forall8  {
\find (          \forall    Gvar ;            (                   Gvar =           subGterm ->                phi ))
\varcond   \replacewith (                {\subst   Gvar ;           subGterm }      phi )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 401 Offset :4

elim_forall9

elim_forall9  {
\find (          \forall    Gvar ;            (                   subGterm =           Gvar ->                phi ))
\varcond   \replacewith (                {\subst   Gvar ;           subGterm }      phi )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 408 Offset :4

elim_forall10

elim_forall10  {
\find (          \forall    Gvar ;            (                   Gvar =           Hterm ->                phi ))
\varcond   \replacewith (                   (               {\subst   Gvar ;       (G )      Hterm }      phi )|             G ::  instance   (                   Hterm )=           FALSE )
\heuristics  (elimQuantifier , elimQuantifierWithCast )

};

defined in: formulaNormalisationRules.key Line: 415 Offset :4

elim_forall11

elim_forall11  {
\find (          \forall    Gvar ;            (                   Hterm =           Gvar ->                phi ))
\varcond   \replacewith (                   (               {\subst   Gvar ;       (G )      Hterm }      phi )|             G ::  instance   (                   Hterm )=           FALSE )
\heuristics  (elimQuantifier , elimQuantifierWithCast )

};

defined in: formulaNormalisationRules.key Line: 423 Offset :4

elim_forall12

elim_forall12  {
\find (          \forall    Gvar ;            (                  (                   psi &             Gvar =           subGterm )->                phi ))
\varcond   \replacewith (                {\subst   Gvar ;           subGterm }     (                   psi ->                phi ))
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 431 Offset :4

elim_forall13

elim_forall13  {
\find (          \forall    Gvar ;            (                  (                   psi &             subGterm =           Gvar )->                phi ))
\varcond   \replacewith (                {\subst   Gvar ;           subGterm }     (                   psi ->                phi ))
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 438 Offset :4

elim_forall14

elim_forall14  {
\find (          \forall    Gvar ;            (                  (                   psi &             Gvar =           Hterm )->                phi ))
\varcond   \replacewith (                   (               {\subst   Gvar ;       (G )      Hterm }     (                   psi ->                phi ))|             G ::  instance   (                   Hterm )=           FALSE )
\heuristics  (elimQuantifier , elimQuantifierWithCast )

};

defined in: formulaNormalisationRules.key Line: 445 Offset :4

elim_forall15

elim_forall15  {
\find (          \forall    Gvar ;            (                  (                   psi &             Hterm =           Gvar )->                phi ))
\varcond   \replacewith (                   (               {\subst   Gvar ;       (G )      Hterm }     (                   psi ->                phi ))|             G ::  instance   (                   Hterm )=           FALSE )
\heuristics  (elimQuantifier , elimQuantifierWithCast )

};

defined in: formulaNormalisationRules.key Line: 453 Offset :4

elim_forall16

elim_forall16  {
\find (          \forall    Gvar ;            (                  (                   Gvar =           subGterm &             psi )->                phi ))
\varcond   \replacewith (                {\subst   Gvar ;           subGterm }     (                   psi ->                phi ))
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 461 Offset :4

elim_forall17

elim_forall17  {
\find (          \forall    Gvar ;            (                  (                   subGterm =           Gvar &             psi )->                phi ))
\varcond   \replacewith (                {\subst   Gvar ;           subGterm }     (                   psi ->                phi ))
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 468 Offset :4

elim_forall18

elim_forall18  {
\find (          \forall    Gvar ;            (                  (                   Gvar =           Hterm &             psi )->                phi ))
\varcond   \replacewith (                   (               {\subst   Gvar ;       (G )      Hterm }     (                   psi ->                phi ))|             G ::  instance   (                   Hterm )=           FALSE )
\heuristics  (elimQuantifier , elimQuantifierWithCast )

};

defined in: formulaNormalisationRules.key Line: 475 Offset :4

elim_forall19

elim_forall19  {
\find (          \forall    Gvar ;            (                  (                   Hterm =           Gvar &             psi )->                phi ))
\varcond   \replacewith (                   (               {\subst   Gvar ;       (G )      Hterm }     (                   psi ->                phi ))|             G ::  instance   (                   Hterm )=           FALSE )
\heuristics  (elimQuantifier , elimQuantifierWithCast )

};

defined in: formulaNormalisationRules.key Line: 483 Offset :4

elim_exists0

elim_exists0  {
\find (          \exists    Gvar ;            (                   Gvar =           subGterm ))
\varcond   \replacewith (                    true )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 491 Offset :4

elim_exists1

elim_exists1  {
\find (          \exists    Gvar ;            (                   subGterm =           Gvar ))
\varcond   \replacewith (                    true )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 498 Offset :4

elim_exists2

elim_exists2  {
\find (          \exists    Gvar ;            (                   Gvar =           Hterm ))
\varcond   \replacewith (                   G ::  instance   (                   Hterm )=           TRUE )
\heuristics  (elimQuantifier , elimQuantifierWithCast )

};

defined in: formulaNormalisationRules.key Line: 505 Offset :4

elim_exists3

elim_exists3  {
\find (          \exists    Gvar ;            (                   Hterm =           Gvar ))
\varcond   \replacewith (                   G ::  instance   (                   Hterm )=           TRUE )
\heuristics  (elimQuantifier , elimQuantifierWithCast )

};

defined in: formulaNormalisationRules.key Line: 512 Offset :4

elim_exists4

elim_exists4  {
\find (          \exists    Gvar ;            (                   phi &             Gvar =           subGterm ))
\varcond   \replacewith (                {\subst   Gvar ;           subGterm }      phi )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 519 Offset :4

elim_exists5

elim_exists5  {
\find (          \exists    Gvar ;            (                   phi &             subGterm =           Gvar ))
\varcond   \replacewith (                {\subst   Gvar ;           subGterm }      phi )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 526 Offset :4

elim_exists6

elim_exists6  {
\find (          \exists    Gvar ;            (                   phi &             Gvar =           Hterm ))
\varcond   \replacewith (                   (               {\subst   Gvar ;       (G )      Hterm }      phi )&            G ::  instance   (                   Hterm )=           TRUE )
\heuristics  (elimQuantifier , elimQuantifierWithCast )

};

defined in: formulaNormalisationRules.key Line: 533 Offset :4

elim_exists7

elim_exists7  {
\find (          \exists    Gvar ;            (                   phi &             Hterm =           Gvar ))
\varcond   \replacewith (                   (               {\subst   Gvar ;       (G )      Hterm }      phi )&            G ::  instance   (                   Hterm )=           TRUE )
\heuristics  (elimQuantifier , elimQuantifierWithCast )

};

defined in: formulaNormalisationRules.key Line: 541 Offset :4

elim_forall_nonSingleton0

elim_forall_nonSingleton0  {
\find (          \forall    nonSingleVar ;            (                   nonSingleVar =           Hterm ))
\varcond   \replacewith (                    false )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 553 Offset :4

elim_forall_nonSingleton1

elim_forall_nonSingleton1  {
\find (          \forall    nonSingleVar ;            (                   Hterm =           nonSingleVar ))
\varcond   \replacewith (                    false )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 560 Offset :4

elim_forall_nonSingleton2

elim_forall_nonSingleton2  {
\find (          \forall    INTVar ;            (                   INTVar >=          intTerm ))
\varcond   \replacewith (                    false )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 567 Offset :4

elim_forall_nonSingleton3

elim_forall_nonSingleton3  {
\find (          \forall    INTVar ;            (                   INTVar <=          intTerm ))
\varcond   \replacewith (                    false )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 574 Offset :4

elim_forall_nonSingleton4

elim_forall_nonSingleton4  {
\find (          \forall    INTVar ;            (                   intTerm >=          INTVar ))
\varcond   \replacewith (                    false )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 581 Offset :4

elim_forall_nonSingleton5

elim_forall_nonSingleton5  {
\find (          \forall    INTVar ;            (                   intTerm <=          INTVar ))
\varcond   \replacewith (                    false )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 588 Offset :4

elim_exists_nonSingleton0

elim_exists_nonSingleton0  {
\find (          \exists    nonSingleVar ;            (                   nonSingleVar !=           Hterm ))
\varcond   \replacewith (                    true )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 595 Offset :4

elim_exists_nonSingleton1

elim_exists_nonSingleton1  {
\find (          \exists    nonSingleVar ;            (                   Hterm !=           nonSingleVar ))
\varcond   \replacewith (                    true )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 602 Offset :4

elim_exists_nonSingleton2

elim_exists_nonSingleton2  {
\find (          \exists    INTVar ;            (                   INTVar >=          intTerm ))
\varcond   \replacewith (                    true )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 609 Offset :4

elim_exists_nonSingleton3

elim_exists_nonSingleton3  {
\find (          \exists    INTVar ;            (                   INTVar <=          intTerm ))
\varcond   \replacewith (                    true )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 616 Offset :4

elim_exists_nonSingleton4

elim_exists_nonSingleton4  {
\find (          \exists    INTVar ;            (                   intTerm >=          INTVar ))
\varcond   \replacewith (                    true )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 623 Offset :4

elim_exists_nonSingleton5

elim_exists_nonSingleton5  {
\find (          \exists    INTVar ;            (                   intTerm <=          INTVar ))
\varcond   \replacewith (                    true )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 630 Offset :4

elim_exists_sub_1

elim_exists_sub_1  {
\schemaVar   \variables LocSet   locVar ;
\schemaVar   \term LocSet   locSetTermLeft ,  locSetTermRight ;
\find (          \exists    locVar ;            (                   subset   (                   locVar ,                    locSetTermRight )&             subset   (                   locSetTermLeft ,                    locVar )))
\varcond   \replacewith (                    subset   (                   locSetTermLeft ,                    locSetTermRight ))
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 640 Offset :4

elim_exists_sub_1_or_phi

elim_exists_sub_1_or_phi  {
\schemaVar   \variables LocSet   locVar ;
\schemaVar   \term LocSet   locSetTermLeft ,  locSetTermRight ;
\find (          \exists    locVar ;            (                  (                   subset   (                   locVar ,                    locSetTermRight )&             subset   (                   locSetTermLeft ,                    locVar ))|              phi ))
\varcond   \replacewith (                    subset   (                   locSetTermLeft ,                    locSetTermRight )|    \exists    locVar ;             phi )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 651 Offset :4

elim_exists_sub_1_and_phi

elim_exists_sub_1_and_phi  {
\schemaVar   \variables LocSet   locVar ;
\schemaVar   \term LocSet   locSetTerm ;
\find (          \exists    locVar ;            (                   subset   (                   locVar ,                    locSetTerm )&             subset   (                   locSetTerm ,                    locVar )&             phi ))
\varcond   \replacewith (          \exists    locVar ;            (                   locVar =           locSetTerm &             phi ))
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 662 Offset :4

elim_forall_superOfAll

elim_forall_superOfAll  {
\schemaVar   \variables LocSet   locVar ;
\schemaVar   \term LocSet   locSetTerm ;
\find (          \forall    locVar ;             subset   (                   locVar ,                    locSetTerm ))
\varcond   \replacewith (                    locSetTerm =           allLocs )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 673 Offset :4

elim_forall_subOfAll

elim_forall_subOfAll  {
\schemaVar   \variables LocSet   locVar ;
\schemaVar   \term LocSet   locSetTerm ;
\find (          \forall    locVar ;             subset   (                   locSetTerm ,                    locVar ))
\varcond   \replacewith (                    locSetTerm =           empty )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 684 Offset :4

elim_forall_subOfAll_and_phi

elim_forall_subOfAll_and_phi  {
\schemaVar   \variables LocSet   locVar ;
\schemaVar   \term LocSet   locSetTerm ;
\find (          \forall    locVar ;            (                   subset   (                   locSetTerm ,                    locVar )&             phi ))
\varcond   \replacewith (                    locSetTerm =           empty &   \forall    locVar ;             phi )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 695 Offset :4

elim_forall_superOfAll_and_phi

elim_forall_superOfAll_and_phi  {
\schemaVar   \variables LocSet   locVar ;
\schemaVar   \term LocSet   locSetTerm ;
\find (          \forall    locVar ;            (                   subset   (                   locVar ,                    locSetTerm )&             phi ))
\varcond   \replacewith (                    locSetTerm =           allLocs &   \forall    locVar ;             phi )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 706 Offset :4

elim_forall_eqSet_imp_phi

elim_forall_eqSet_imp_phi  {
\schemaVar   \variables LocSet   locVar ;
\schemaVar   \term LocSet   locSetTerm ;
\find (          \forall    locVar ;            (                  (                   subset   (                   locVar ,                    locSetTerm )&             subset   (                   locSetTerm ,                    locVar ))->                phi ))
\varcond   \replacewith (          \forall    locVar ;            (                   locSetTerm =           locVar ->                phi ))
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 717 Offset :4

elim_forall_leq

elim_forall_leq  {
\find (          \forall    INTVar ;            (                   INTVar <=          intTermLeft |              INTVar >=          intTermRight ))
\varcond   \replacewith (                    intTermRight <=          intTermLeft +         1 )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 729 Offset :4

elim_exists_leq

elim_exists_leq  {
\find (          \exists    INTVar ;            (                   INTVar <=          intTermLeft &             INTVar >=          intTermRight ))
\varcond   \replacewith (                    intTermRight <=          intTermLeft )
\heuristics  (elimQuantifier )

};

defined in: formulaNormalisationRules.key Line: 736 Offset :4

swapQuantifiersAll

swapQuantifiersAll  {
\find (          \forall    u ;   \forall    v ;             phi )
  \replacewith (          \forall    v ;   \forall    u ;             phi )
\heuristics  (swapQuantifiers )

};

defined in: formulaNormalisationRules.key Line: 744 Offset :4

swapQuantifiersEx

swapQuantifiersEx  {
\find (          \exists    u ;   \exists    v ;             phi )
  \replacewith (          \exists    v ;   \exists    u ;             phi )
\heuristics  (swapQuantifiers )

};

defined in: formulaNormalisationRules.key Line: 750 Offset :4

distr_forallAnd

distr_forallAnd  {
\find (          \forall    u ;            (                   phi &             psi ))
  \replacewith (                   (         \forall    u ;             phi )&            (         \forall    u ;             psi ))
\heuristics  (distrQuantifier , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 758 Offset :4

distr_existsOr

distr_existsOr  {
\find (          \exists    u ;            (                   phi |              psi ))
  \replacewith (                   (         \exists    u ;             phi )|             (         \exists    u ;             psi ))
\heuristics  (distrQuantifier , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 764 Offset :4

distr_forallOr1

distr_forallOr1  {
\find (          \forall    u ;            (                   phi |              psi ))
\varcond   \replacewith (                   (         \forall    u ;             phi )|              psi )
\heuristics  (distrQuantifier , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 770 Offset :4

distr_forallOr2

distr_forallOr2  {
\find (          \forall    u ;            (                   phi |              psi ))
\varcond   \replacewith (                    phi |             (         \forall    u ;             psi ))
\heuristics  (distrQuantifier , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 777 Offset :4

distr_existsAnd1

distr_existsAnd1  {
\find (          \exists    u ;            (                   phi &             psi ))
\varcond   \replacewith (                   (         \exists    u ;             phi )&             psi )
\heuristics  (distrQuantifier , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 784 Offset :4

distr_existsAnd2

distr_existsAnd2  {
\find (          \exists    u ;            (                   phi &             psi ))
\varcond   \replacewith (                    phi &            (         \exists    u ;             psi ))
\heuristics  (distrQuantifier , notHumanReadable )

};

defined in: formulaNormalisationRules.key Line: 791 Offset :4

all_pull_out0

all_pull_out0  {
\find (                   (         \forall    u ;             b )&             c )
\varcond   \replacewith (          \forall    u ;            (                   b &             c ))
\heuristics  (pullOutQuantifierAll )

};

defined in: formulaNormalisationRules.key Line: 800 Offset :4

all_pull_out1

all_pull_out1  {
\find (                    c &            (         \forall    u ;             b ))
\varcond   \replacewith (          \forall    u ;            (                   c &             b ))
\heuristics  (pullOutQuantifierAll )

};

defined in: formulaNormalisationRules.key Line: 807 Offset :4

all_pull_out2

all_pull_out2  {
\find (                   (         \forall    u ;             b )|              c )
\varcond   \replacewith (          \forall    u ;            (                   b |              c ))
\heuristics  (pullOutQuantifierAll )

};

defined in: formulaNormalisationRules.key Line: 814 Offset :4

all_pull_out3

all_pull_out3  {
\find (                    c |             (         \forall    u ;             b ))
\varcond   \replacewith (          \forall    u ;            (                   c |              b ))
\heuristics  (pullOutQuantifierAll )

};

defined in: formulaNormalisationRules.key Line: 821 Offset :4

all_pull_out4

all_pull_out4  {
\find (                   (         \forall    u ;             b )&            (         \forall    u2 ;             c ))
\varcond   \replacewith (          \forall    u ;            (                   b &         {\subst   u2 ;           u }      c ))
\heuristics  (pullOutQuantifierAll , pullOutQuantifierUnifying )

};

defined in: formulaNormalisationRules.key Line: 828 Offset :4

ex_pull_out0

ex_pull_out0  {
\find (                   (         \exists    u ;             b )&             c )
\varcond   \replacewith (          \exists    u ;            (                   b &             c ))
\heuristics  (pullOutQuantifierEx )

};

defined in: formulaNormalisationRules.key Line: 835 Offset :4

ex_pull_out1

ex_pull_out1  {
\find (                    c &            (         \exists    u ;             b ))
\varcond   \replacewith (          \exists    u ;            (                   c &             b ))
\heuristics  (pullOutQuantifierEx )

};

defined in: formulaNormalisationRules.key Line: 842 Offset :4

ex_pull_out2

ex_pull_out2  {
\find (                   (         \exists    u ;             b )|              c )
\varcond   \replacewith (          \exists    u ;            (                   b |              c ))
\heuristics  (pullOutQuantifierEx )

};

defined in: formulaNormalisationRules.key Line: 849 Offset :4

ex_pull_out3

ex_pull_out3  {
\find (                    c |             (         \exists    u ;             b ))
\varcond   \replacewith (          \exists    u ;            (                   c |              b ))
\heuristics  (pullOutQuantifierEx )

};

defined in: formulaNormalisationRules.key Line: 856 Offset :4

ex_pull_out4

ex_pull_out4  {
\find (                   (         \exists    u ;             b )|             (         \exists    u2 ;             c ))
\varcond   \replacewith (          \exists    u ;            (                   b |          {\subst   u2 ;           u }      c ))
\heuristics  (pullOutQuantifierEx , pullOutQuantifierUnifying )

};

defined in: formulaNormalisationRules.key Line: 863 Offset :4

ifEqualsNull

ifEqualsNull  {
\schemaVar   \term any   x ,  y ;
\find (                   \if (                   phi )\then (                   x )\else (                   y )=           null )
  \replacewith (                   (                   phi &             x =           null )|             (         !             phi &             y =           null ))
\heuristics  (simplify )

};

defined in: formulaNormalisationRules.key Line: 871 Offset :4

ifEqualsTRUE

ifEqualsTRUE  {
\schemaVar   \term any   x ,  y ;
\find (                   \if (                   phi )\then (                   x )\else (                   y )=           TRUE )
  \replacewith (                   (                   phi &             x =           TRUE )|             (         !             phi &             y =           TRUE ))
\heuristics  (simplify )

};

defined in: formulaNormalisationRules.key Line: 880 Offset :4

ifEqualsInteger

ifEqualsInteger  {
\schemaVar   \term any   x ,  y ;
\schemaVar   \term numbers   iz ;
\find (                   \if (                   phi )\then (                   x )\else (                   y )=           Z   (                   iz ))
  \replacewith (                   (                   phi &             x =           Z   (                   iz ))|             (         !             phi &             y =           Z   (                   iz )))
\heuristics  (simplify )

};

defined in: formulaNormalisationRules.key Line: 889 Offset :4

KeY Logic Documentation

Defined symbols in the KeY System

Overview