Sequence Length Function

From GM-RKB
Jump to navigation Jump to search

A Sequence Length Function is a length function that is restricted to sequences (a count function that maps a sequence to a non-negative number of the count of the symbols in the sequence)



References

  (forall (n s)   
     (if (sequence s) 
         (iff (length n s)
              (exists (s1 s2)
                 (and (function0 s s1 s2)(ints s1 1 n))))))