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   (                    seqGet  <[ alpha ]>   (                    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