KeY Logic Documentation
Defined symbols in the KeY System
Generated from version: heads/main on Sat Mar 01 14:33:17 UTC 2025
Startpage
Usage Index
KeY Docs
Overview
Rulesets
alpha
apply_auxiliary_eq
apply_equations
apply_equations_andOr
apply_select_eq
auto_induction
auto_induction_lemma
beta
boolean_cases
boxDiamondConv
cast_deletion
charLiteral_to_intLiteral
classAxiom
closure
cnf_andAssoc
cnf_andComm
cnf_dist
cnf_expandIfThenElse
cnf_orAssoc
cnf_orComm
cnf_setComm
comprehension_split
comprehensions
comprehensions_high_costs
comprehensions_low_costs
concrete
confluence_restricted
conjNormalForm
cut
cut_direct
defOpsConcat
defOpsReplace
defOpsReplaceInline
defOpsSeqEquality
defOpsStartsEndsWith
defOps_div
defOps_divModPullOut
defOps_expandJNumericOp
defOps_expandModulo
defOps_expandRanges
defOps_jdiv
defOps_jdiv_inline
defOps_mod
defOps_modHomoEq
delayedExpansion
delta
delta
distrQuantifier
elimQuantifier
elimQuantifierWithCast
eval_literals
evaluate_instanceof
executeDoubleAssignment
executeFloatAssignment
executeIntegerAssignment
find_term_not_in_assumes
gamma
gamma_destructive
hide_auxiliary_eq
hide_auxiliary_eq_const
inEqSimp_andOr_subsumption
inEqSimp_and_contradInEqs
inEqSimp_and_subsumptionEq
inEqSimp_antiSymm
inEqSimp_balance
inEqSimp_commute
inEqSimp_contradEqs
inEqSimp_contradInEqs
inEqSimp_directInEquations
inEqSimp_exactShadow
inEqSimp_expand
inEqSimp_forNormalisation
inEqSimp_homo
inEqSimp_makeNonStrict
inEqSimp_moveLeft
inEqSimp_nonLin
inEqSimp_nonLin_divide
inEqSimp_nonLin_multiply
inEqSimp_nonLin_neg
inEqSimp_nonLin_pos
inEqSimp_nonNegSquares
inEqSimp_normalise
inEqSimp_or_antiSymm
inEqSimp_or_tautInEqs
inEqSimp_or_weaken
inEqSimp_propagation
inEqSimp_pullOutGcd
inEqSimp_pullOutGcd_antec
inEqSimp_pullOutGcd_geq
inEqSimp_pullOutGcd_leq
inEqSimp_saturate
inEqSimp_signCases
inEqSimp_special_nonLin
inEqSimp_split_eq
inEqSimp_strengthen
inEqSimp_subsumption
inReachableStateImplication
induction_var
information_flow_contract_appl
insert_eq_nonrigid
instanceof_to_exists
int_arithmetic
integerToString
javaFloatSemantics
javaIntegerSemantics
limitObserver
loopInvariant
loop_expand
loop_scope_expand
loop_scope_inv_taclet
merge_point
method_expand
modal_tautology
moveQuantToLeft
negationNormalForm
no_self_application
nonDuplicateAppCheckEq
notHumanReadable
obsolete
order_terms
partialInvAxiom
polyDivision
polySimp_addAssoc
polySimp_addOrder
polySimp_applyEq
polySimp_applyEqPseudo
polySimp_applyEqRigid
polySimp_balance
polySimp_critPair
polySimp_directEquations
polySimp_dist
polySimp_elimOneLeft
polySimp_elimOneRight
polySimp_elimSubNeg
polySimp_expand
polySimp_homo
polySimp_leftNonUnit
polySimp_mulAssoc
polySimp_mulOne
polySimp_mulOrder
polySimp_newSmallSym
polySimp_newSym
polySimp_normalise
polySimp_pullOutFactor
polySimp_pullOutGcd
polySimp_saturate
pullOutQuantifierAll
pullOutQuantifierEx
pullOutQuantifierUnifying
pull_out_quantifier
pull_out_select
query_axiom
replace_known_left
replace_known_right
semantics_blasting
setEqualityBlastingRight
simplify
simplify_ENLARGING
simplify_autoname
simplify_boolean
simplify_enlarging
simplify_expression
simplify_heap_high_costs
simplify_instanceof_static
simplify_int
simplify_literals
simplify_prog
simplify_prog_subset
simplify_select
split_cond
split_if
std_taclets
stringNormalisationReduce
stringsConcatNotBothLiterals
stringsContainsDefInline
stringsExpandDefNormalOp
stringsIntroduceNewSym
stringsMoveReplaceInside
stringsReduceConcat
stringsReduceOrMoveOutsideConcat
stringsReduceSubstring
stringsSimplify
swapQuantifiers
system_invariant
test_gen
test_gen_empty_modality_hide
test_gen_quan
test_gen_quan_num
triggered
try_apply_subst
type_hierarchy_def
update_apply
update_apply_on_update
update_elim
update_join
userTaclets1
userTaclets2
userTaclets3
ruleSetsDeclarations.key