KeY Logic Documentation
Defined symbols in the KeY System
Generated from version: heads/main on Fri Aug 21 01:50:48 UTC 2026
Startpage
Usage Index
KeY Docs
Overview
Sorts
G
G2
Predicates
wellOrderLeqInt
Taclets
def_wellOrderLeqInt
ifExthenelse1_eq
ifExthenelse1_eq2
ifExthenelse1_eq2_for
ifExthenelse1_eq2_for_phi
ifExthenelse1_eq2_phi
ifExthenelse1_eq_for
ifExthenelse1_eq_for_phi
ifExthenelse1_eq_phi
ifExthenelse1_false
ifExthenelse1_false_for
ifExthenelse1_min
ifExthenelse1_min_for
ifExthenelse1_solve
ifExthenelse1_solve_for
ifExthenelse1_split
ifExthenelse1_split_for
ifExthenelse1_unused_var
ifExthenelse1_unused_var_for
ifthenelse_concrete
ifthenelse_concrete2
ifthenelse_concrete3
ifthenelse_concrete4
ifthenelse_false
ifthenelse_false_for
ifthenelse_negated
ifthenelse_negated_for
ifthenelse_same_branches
ifthenelse_same_branches_for
ifthenelse_split
ifthenelse_split_for
ifthenelse_true
ifthenelse_true_for
ifThenElseRules.key
Sorts
G
\generic G, G2;
defined in: ifThenElseRules.key Line: 10 Offset :4
G2
\generic G, G2;
defined in: ifThenElseRules.key Line: 10 Offset :4
Predicates
wellOrderLeqInt
wellOrderLeqInt
(
int
,
int
)
;
defined in: ifThenElseRules.key Line: 27 Offset :4
Taclets
No choice condition specified
ifthenelse_true