KeY Logic Documentation

Defined symbols in the KeY System

Generated from version: heads/main on Fri Aug 21 01:50:47 UTC 2026

Overview

wdFormulaRules.key

Taclets

Enabled under choices: wdChecks:onwdOperator:L

wd_Logical_Op_Neg

wd_Logical_Op_Neg { \find ( WD ( ! a ) ) \replacewith ( WD ( a ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 16 Offset :4

wd_Logical_Op_And

wd_Logical_Op_And { \find ( WD ( ( a & b ) << l >> ) ) \varcond \replacewith ( WD ( a ) & WD ( b ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 27 Offset :4

wd_Logical_Op_AndSC

wd_Logical_Op_AndSC { \find ( WD ( ( ( a & b ) << l >> ) ) ) \varcond \replacewith ( WD ( a ) & ( a -> WD ( b ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 41 Offset :4

wd_Logical_Op_Or

wd_Logical_Op_Or { \find ( WD ( ( a | b ) << l >> ) ) \varcond \replacewith ( WD ( a ) & WD ( b ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 55 Offset :4

wd_Logical_Op_OrSC

wd_Logical_Op_OrSC { \find ( WD ( ( ( a | b ) << l >> ) ) ) \varcond \replacewith ( WD ( a ) & ( ! a -> WD ( b ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 69 Offset :4

wd_Logical_Op_Imp

wd_Logical_Op_Imp { \find ( WD ( ( a -> b ) ) ) \replacewith ( WD ( a ) & ( a -> WD ( b ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 83 Offset :4

wd_Logical_Op_Eqv

wd_Logical_Op_Eqv { \find ( WD ( ( a <-> b ) ) ) \replacewith ( WD ( a ) & WD ( b ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 94 Offset :4

wd_Logical_Op_Cond_Expr

wd_Logical_Op_Cond_Expr { \find ( wd ( \if ( a ) \then ( s ) \else ( t ) ) ) \replacewith ( WD ( a ) & ( a -> wd ( s ) ) & ( ! a -> wd ( t ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 105 Offset :4

wd_Logical_Op_Cond_Form

wd_Logical_Op_Cond_Form { \find ( WD ( \if ( a ) \then ( b ) \else ( c ) ) ) \replacewith ( WD ( a ) & ( a -> WD ( b ) ) & ( ! a -> WD ( c ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 116 Offset :4

wd_Logical_Op_ExCond_Expr

wd_Logical_Op_ExCond_Expr { \find ( wd ( \ifEx j ; ( a ) \then ( s ) \else ( t ) ) ) \varcond \replacewith ( ( \forall j ; WD ( a ) ) & ( ( \forall j ; ! a ) -> wd ( t ) ) & ( \forall j ; ( a -> wd ( s ) ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 127 Offset :4

wd_Logical_Op_ExCond_Form

wd_Logical_Op_ExCond_Form { \find ( WD ( \ifEx j ; ( a ) \then ( b ) \else ( c ) ) ) \varcond \replacewith ( ( \forall j ; WD ( a ) ) & ( ( \forall j ; ! a ) -> WD ( c ) ) & ( \forall j ; ( a -> WD ( b ) ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 142 Offset :4

wd_Logical_Quant_All

wd_Logical_Quant_All { \find ( WD ( \forall i ; a ) ) \replacewith ( \forall i ; WD ( a ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 157 Offset :4

wd_Logical_Quant_Exist

wd_Logical_Quant_Exist { \find ( WD ( \exists i ; a ) ) \replacewith ( \forall i ; WD ( a ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 168 Offset :4

Taclets

Enabled under choices: wdChecks:onwdOperator:D

wd_Logical_Op_Neg

wd_Logical_Op_Neg { \find ( WD ( ! a ) ) \replacewith ( WD ( a ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 182 Offset :4

wd_Logical_Op_And

wd_Logical_Op_And { \find ( WD ( ( a & b ) ) ) \replacewith ( ( WD ( a ) & ! a ) | ( WD ( b ) & ! b ) | ( WD ( a ) & WD ( b ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 193 Offset :4

wd_Logical_Op_Or

wd_Logical_Op_Or { \find ( WD ( ( a | b ) ) ) \replacewith ( ( WD ( a ) & a ) | ( WD ( b ) & b ) | ( WD ( a ) & WD ( b ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 204 Offset :4

wd_Logical_Op_Imp

wd_Logical_Op_Imp { \find ( WD ( ( a -> b ) ) ) \replacewith ( ( WD ( a ) & ! a ) | ( WD ( b ) & b ) | ( WD ( a ) & WD ( b ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 215 Offset :4

wd_Logical_Op_Eqv

wd_Logical_Op_Eqv { \find ( WD ( ( a <-> b ) ) ) \replacewith ( WD ( a ) & WD ( b ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 226 Offset :4

wd_Logical_Op_Cond_Expr

wd_Logical_Op_Cond_Expr { \find ( wd ( \if ( a ) \then ( s ) \else ( t ) ) ) \replacewith ( ( WD ( a ) & wd ( s ) & a ) | ( WD ( a ) & wd ( t ) & ! a ) | ( wd ( s ) & wd ( t ) & ( s = t ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 237 Offset :4

wd_Logical_Op_Cond_Form

wd_Logical_Op_Cond_Form { \find ( WD ( \if ( a ) \then ( b ) \else ( c ) ) ) \replacewith ( ( WD ( a ) & WD ( b ) & a ) | ( WD ( a ) & WD ( c ) & ! a ) | ( WD ( b ) & WD ( c ) & ( b <-> c ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 248 Offset :4

wd_Logical_Op_ExCond_Expr

wd_Logical_Op_ExCond_Expr { \find ( wd ( \ifEx j ; ( a ) \then ( s ) \else ( t ) ) ) \varcond \replacewith ( ( \exists j ; ( WD ( a ) & wd ( s ) & a & ( ( wellOrderLeqInt ( jPrime , j ) & ( jPrime != j ) ) -> { \subst j ; jPrime } ( WD ( a ) & ! a ) ) ) ) | ( \forall j ; ( WD ( a ) & wd ( t ) & ! a ) ) | ( \forall j ; ( wd ( s ) & wd ( t ) & ( s = t ) ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 259 Offset :4

wd_Logical_Op_ExCond_Form

wd_Logical_Op_ExCond_Form { \find ( WD ( \ifEx j ; ( a ) \then ( b ) \else ( c ) ) ) \varcond \replacewith ( ( \exists j ; ( WD ( a ) & WD ( b ) & a & ( ( wellOrderLeqInt ( jPrime , j ) & ( jPrime != j ) ) -> { \subst j ; jPrime } ( WD ( a ) & ! a ) ) ) ) | ( \forall j ; ( WD ( a ) & WD ( c ) & ! a ) ) | ( \forall j ; ( WD ( b ) & WD ( c ) & ( b <-> c ) ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 278 Offset :4

wd_Logical_Quant_All

wd_Logical_Quant_All { \find ( WD ( \forall i ; a ) ) \replacewith ( ( \exists i ; ( WD ( a ) & ! a ) ) | ( \forall i ; WD ( a ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 297 Offset :4

wd_Logical_Quant_Exist

wd_Logical_Quant_Exist { \find ( WD ( \exists i ; a ) ) \replacewith ( ( \exists i ; ( WD ( a ) & a ) ) | ( \forall i ; WD ( a ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 308 Offset :4

Taclets

Enabled under choices: wdChecks:onwdOperator:Y

wd_T_Logical_Op_Neg

wd_T_Logical_Op_Neg { \find ( T ( ! a ) ) \replacewith ( F ( a ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 322 Offset :4

wd_F_Logical_Op_Neg

wd_F_Logical_Op_Neg { \find ( F ( ! a ) ) \replacewith ( T ( a ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 333 Offset :4

wd_T_Logical_Op_And

wd_T_Logical_Op_And { \find ( T ( ( a & b ) ) ) \replacewith ( T ( a ) & T ( b ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 344 Offset :4

wd_F_Logical_Op_And

wd_F_Logical_Op_And { \find ( F ( ( a & b ) ) ) \replacewith ( F ( a ) | F ( b ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 355 Offset :4

wd_T_Logical_Op_Or

wd_T_Logical_Op_Or { \find ( T ( ( a | b ) ) ) \replacewith ( T ( a ) | T ( b ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 366 Offset :4

wd_F_Logical_Op_Or

wd_F_Logical_Op_Or { \find ( F ( ( a | b ) ) ) \replacewith ( F ( a ) & F ( b ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 377 Offset :4

wd_T_Logical_Op_Imp

wd_T_Logical_Op_Imp { \find ( T ( ( a -> b ) ) ) \replacewith ( F ( a ) | T ( b ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 388 Offset :4

wd_F_Logical_Op_Imp

wd_F_Logical_Op_Imp { \find ( F ( ( a -> b ) ) ) \replacewith ( T ( a ) & F ( b ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 399 Offset :4

wd_T_Logical_Op_Eqv

wd_T_Logical_Op_Eqv { \find ( T ( ( a <-> b ) ) ) \replacewith ( ( T ( a ) & T ( b ) ) | ( F ( a ) & F ( b ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 410 Offset :4

wd_F_Logical_Op_Eqv

wd_F_Logical_Op_Eqv { \find ( F ( ( a <-> b ) ) ) \replacewith ( ( T ( a ) & F ( b ) ) | ( F ( a ) & T ( b ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 421 Offset :4

wd_Logical_Op_Cond_Expr

wd_Logical_Op_Cond_Expr { \find ( wd ( \if ( a ) \then ( s ) \else ( t ) ) ) \replacewith ( ( T ( a ) & wd ( s ) ) | ( F ( a ) & wd ( t ) ) | ( wd ( s ) & wd ( t ) & ( s = t ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 432 Offset :4

wd_T_Logical_Op_Cond_Form

wd_T_Logical_Op_Cond_Form { \find ( T ( \if ( a ) \then ( b ) \else ( c ) ) ) \replacewith ( ( T ( a ) & T ( b ) ) | ( F ( a ) & T ( c ) ) | ( T ( b ) & T ( c ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 443 Offset :4

wd_F_Logical_Op_Cond_Form

wd_F_Logical_Op_Cond_Form { \find ( F ( \if ( a ) \then ( b ) \else ( c ) ) ) \replacewith ( ( T ( a ) & F ( b ) ) | ( F ( a ) & F ( c ) ) | ( F ( b ) & F ( c ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 454 Offset :4

wd_Logical_Op_ExCond_Expr

wd_Logical_Op_ExCond_Expr { \find ( wd ( \ifEx j ; ( a ) \then ( s ) \else ( t ) ) ) \varcond \replacewith ( ( \exists j ; ( T ( a ) & wd ( s ) & ( ( wellOrderLeqInt ( jPrime , j ) & ( jPrime != j ) ) -> { \subst j ; jPrime } F ( a ) ) ) ) | ( \forall j ; ( F ( a ) & wd ( t ) ) ) | ( \forall j ; ( wd ( s ) & wd ( t ) & ( s = t ) ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 465 Offset :4

wd_T_Logical_Op_ExCond_Form

wd_T_Logical_Op_ExCond_Form { \find ( T ( \ifEx j ; ( a ) \then ( b ) \else ( c ) ) ) \varcond \replacewith ( ( \exists j ; ( T ( a ) & T ( b ) & ( ( wellOrderLeqInt ( jPrime , j ) & ( jPrime != j ) ) -> { \subst j ; jPrime } F ( a ) ) ) ) | ( \forall j ; ( F ( a ) & T ( c ) ) ) | ( \forall j ; ( T ( b ) & T ( c ) ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 484 Offset :4

wd_F_Logical_Op_ExCond_Form

wd_F_Logical_Op_ExCond_Form { \find ( F ( \ifEx j ; ( a ) \then ( b ) \else ( c ) ) ) \varcond \replacewith ( ( \exists j ; ( T ( a ) & F ( b ) & ( ( wellOrderLeqInt ( jPrime , j ) & ( jPrime != j ) ) -> { \subst j ; jPrime } F ( a ) ) ) ) | ( \forall j ; ( F ( a ) & F ( c ) ) ) | ( \forall j ; ( F ( b ) & F ( c ) ) ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 503 Offset :4

wd_T_Logical_Quant_All

wd_T_Logical_Quant_All { \find ( T ( \forall i ; a ) ) \replacewith ( \forall i ; T ( a ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 522 Offset :4

wd_F_Logical_Quant_All

wd_F_Logical_Quant_All { \find ( F ( \forall i ; a ) ) \replacewith ( \exists i ; F ( a ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 533 Offset :4

wd_T_Logical_Quant_Exist

wd_T_Logical_Quant_Exist { \find ( T ( \exists i ; a ) ) \replacewith ( \exists i ; T ( a ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 544 Offset :4

wd_F_Logical_Quant_Exist

wd_F_Logical_Quant_Exist { \find ( F ( \exists i ; a ) ) \replacewith ( \forall i ; F ( a ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 555 Offset :4

wd_Y_Split

wd_Y_Split { \find ( WD ( a ) ) \varcond \replacewith ( T ( a ) | F ( a ) ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 568 Offset :4

wd_T_Resolve

wd_T_Resolve { \find ( T ( a ) ) \varcond \replacewith ( WD ( a ) & a ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 582 Offset :4

wd_F_Resolve

wd_F_Resolve { \find ( F ( a ) ) \varcond \replacewith ( WD ( a ) & ! a ) \heuristics (simplify ) };defined in: wdFormulaRules.key Line: 596 Offset :4