wdSeqRules.key

Taclets

Enabled under choices: wdChecks:on

wd_Seq_Length

wd_Seq_Length  {
\find (                    wd   (                   seqLen   (                   s )))
  \replacewith (                    wd   (                   s ))
\heuristics  (simplify )

};

defined in: wdSeqRules.key Line: 13 Offset :4

wd_Seq_Singleton

wd_Seq_Singleton  {
\find (                    wd   (                   seqSingleton   (                   t )))
  \replacewith (                    wd   (                   t ))
\heuristics  (simplify )

};

defined in: wdSeqRules.key Line: 24 Offset :4

wd_Seq_Reverse

wd_Seq_Reverse  {
\find (                    wd   (                   seqReverse   (                   s )))
  \replacewith (                    wd   (                   s ))
\heuristics  (simplify )

};

defined in: wdSeqRules.key Line: 35 Offset :4

wd_Seq_NPermInv

wd_Seq_NPermInv  {
\find (                    wd   (                   seqNPermInv   (                   s )))
  \replacewith (                    wd   (                   s )&             seqNPerm   (                   s ))
\heuristics  (simplify )

};

defined in: wdSeqRules.key Line: 46 Offset :4

wd_Seq_Get

wd_Seq_Get  {
\find (                    wd   (                  alpha ::  seqGet   (                   s ,                    n )))
  \replacewith (                    wd   (                   s )&             wd   (                   n )&             leq   (                   0 ,                    n )&             lt   (                   n ,                    seqLen   (                   s )))
\heuristics  (simplify )

};

defined in: wdSeqRules.key Line: 57 Offset :4

wd_Seq_IndexOf

wd_Seq_IndexOf  {
\find (                    wd   (                   seqIndexOf   (                   s ,                    t )))
  \replacewith (                    wd   (                   s )&             wd   (                   t ))
\heuristics  (simplify )

};

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

wd_Seq_Concat

wd_Seq_Concat  {
\find (                    wd   (                   seqConcat   (                   s ,                    q )))
  \replacewith (                    wd   (                   s )&             wd   (                   q ))
\heuristics  (simplify )

};

defined in: wdSeqRules.key Line: 79 Offset :4

wd_Seq_Remove

wd_Seq_Remove  {
\find (                    wd   (                   seqRemove   (                   s ,                    n )))
  \replacewith (                    wd   (                   s )&             wd   (                   n )&             leq   (                   0 ,                    n )&             lt   (                   n ,                    seqLen   (                   s )))
\heuristics  (simplify )

};

defined in: wdSeqRules.key Line: 90 Offset :4

wd_Seq_Sub

wd_Seq_Sub  {
\find (                    wd   (                   seqSub   (                   s ,                    m ,                    n )))
  \replacewith (                    wd   (                   s )&             wd   (                   m )&             wd   (                   n )&             leq   (                   0 ,                    m )&             leq   (                   m ,                    n )&             leq   (                   n ,                    seqLen   (                   s )))
\heuristics  (simplify )

};

defined in: wdSeqRules.key Line: 101 Offset :4

wd_Seq_Swap

wd_Seq_Swap  {
\find (                    wd   (                   seqSwap   (                   s ,                    m ,                    n )))
  \replacewith (                    wd   (                   s )&             wd   (                   m )&             wd   (                   n )&             leq   (                   0 ,                    m )&             leq   (                   0 ,                    n )&             lt   (                   m ,                    seqLen   (                   s ))&             lt   (                   n ,                    seqLen   (                   s )))
\heuristics  (simplify )

};

defined in: wdSeqRules.key Line: 112 Offset :4

wd_Seq_Def

wd_Seq_Def  {
\find (                    wd   (                   seqDef  {   i ; } (                   m ,                    n ,                    t )))
\varcond   \replacewith (                    wd   (                   m )&             wd   (                   n )&             leq   (                   m ,                    n )&   \forall    i ;            (                  (                   leq   (                   m ,                    i )&             lt   (                   i ,                    n ))->                wd   (                   t )))
\heuristics  (simplify )

};

defined in: wdSeqRules.key Line: 123 Offset :4

wd_Seq_Pred_Perm

wd_Seq_Pred_Perm  {
\find (                    WD   (                   seqPerm   (                   s ,                    q )))
  \replacewith (                    wd   (                   s )&             wd   (                   q ))
\heuristics  (simplify )

};

defined in: wdSeqRules.key Line: 138 Offset :4

wd_Seq_Pred_NPerm

wd_Seq_Pred_NPerm  {
\find (                    WD   (                   seqNPerm   (                   s )))
  \replacewith (                    wd   (                   s ))
\heuristics  (simplify )

};

defined in: wdSeqRules.key Line: 149 Offset :4

KeY Logic Documentation

Defined symbols in the KeY System

Overview