types.key

Sorts

SORT

SORT;defined in: types.key Line: 2 Offset :2

alph

\generic alph;defined in: types.key Line: 3 Offset :2

bet

\generic bet;defined in: types.key Line: 4 Offset :2

alphSub

\generic alphSub \extends alph ;defined in: types.key Line: 5 Offset :2

Functions

anySORT

SORT anySORT ; defined in: types.key Line: 9 Offset :2

alph::ssort

SORT alph :: ssort ; defined in: types.key Line: 10 Offset :2

Predicates

ssubsort

ssubsort (SORT , SORT ); defined in: types.key Line: 14 Offset :2

Taclets

No choice condition specified

ssubsortDirect

ssubsortDirect  {
\find (                    ssubsort   (                  alphSub ::  ssort ,                   alph ::  ssort ))
  \replacewith (                    true )
\heuristics  (simplify )

};

defined in: types.key Line: 18 Offset :2

ssubsortTop

ssubsortTop  {
\schemaVar   \term SORT   s ;
\find (                    ssubsort   (                   s ,                    anySORT ))
  \replacewith (                    true )
\heuristics  (simplify )

};

defined in: types.key Line: 24 Offset :2

subsortTrans

subsortTrans  {
\schemaVar   \term SORT   s1 ,  s2 ,  s3 ;
\assumes (                     ssubsort   (                   s1 ,                    s2 ),                     ssubsort   (                   s2 ,                    s3 )==>  )
  \add (                     ssubsort   (                   s1 ,                    s3 )==>  )
\heuristics  (simplify_enlarging )

};

defined in: types.key Line: 31 Offset :2

ssubsortSup

ssubsortSup  {
\find (                    ssubsort   (                  alph ::  ssort ,                   alphSub ::  ssort ))
\varcond   \replacewith (                    false )
\heuristics  (simplify )

};

defined in: types.key Line: 38 Offset :2

KeY Logic Documentation

Defined symbols in the KeY System

Overview