var2 $ where ~ex1 p where true: p notin $ & p+1 in $;
allpos $;

defaultwhere1(p) = all1 r: r<p => r in $;
defaultwhere2(P) = all1 p: p in P => all1 r: r<p => r in $;

# we declare a string of 8-bit vectors
var2 bit0 where bit0 sub $, bit1 where bit1 sub $,
     bit2 where bit2 sub $, bit3 where bit3 sub $,
     bit4 where bit4 sub $, bit5 where bit5 sub $,
     bit6 where bit6 sub $, bit7 where bit7 sub $;

macro consecutive_in_set(var1 p, var1 q, var2 P) =
p < q & p in P & q in P & all1 r: p < r & r < q => r notin P;

# ASCII 'a' is 97, which is 01100001
macro is_a(var1 p, var1 q) =
q = p + 1 & 
p in bit0 & p notin bit1 & p notin bit2 & p notin bit3 &
p notin bit4 & p in bit5 & p in bit6 & p notin bit7;

# ASCII 'b' is 98, which is 01100010
macro is_b(var1 p, var1 q) =
q = p + 1 & 
p notin bit0 & p in bit1 & p notin bit2 & p notin bit3 &
p notin bit4 & p in bit5 & p in bit6 & p notin bit7;

# we concatenate by guessing the intermediate position where
# the string parsed according to the first regular expression 
# (in this case "a") ends and the string parsed according to 
# the second (in this case "b") starts
pred is_ab(var1 p, var1 q) =
ex1 r where p<=r & r<=q: is_a(p, r) & is_b(r, q);

# a star expression is handled by guessing the set of
# intermediate positions
pred is_ab_star(var1 p, var1 q) =
ex2 P: p in P & q in P &
       all1 r, r': consecutive_in_set(r, r', P) => is_ab(r, r');

pred is_a_star(var1 p, var1 q) =
ex2 P: p in P & q in P &
       all1 r, r': consecutive_in_set(r, r', P) => is_a(r, r');

pred is_a_star_ab_star(var1 p, var1 q) =
ex1 r where p<=r & r<=q: is_a_star(p, r) & is_ab_star(r, q);

is_a_star_ab_star(0, max($)+1);