20-theory-words.mm0

import "10-theory-definedness.mm0";

term a_symbol : Symbol ;
def a : Pattern = $sym a_symbol$ ;
term b_symbol : Symbol ;
def b : Pattern = $sym b_symbol$ ;

def emptyset : Pattern = $bot$ ;

term epsilon_symbol : Symbol ;
def epsilon : Pattern = $sym epsilon_symbol$ ;

term concat_symbol : Symbol ;
def concat (phi psi: Pattern) : Pattern = $(app (app (sym concat_symbol) phi) psi)$;
infixl concat: $..$ prec 39;

def kleene_l {X: SVar} (alpha: Pattern X) : Pattern = $mu X (epsilon \/ sVar X .. alpha)$;
def kleene_r {X: SVar} (alpha: Pattern X) : Pattern = $mu X (epsilon \/ alpha .. sVar X)$;
def kleene   {X: SVar} (alpha: Pattern X) : Pattern = $(kleene_r X alpha)$;

--- We assume that the alphabet has only two letters.
--- This, however, captures the full expressivity.
def top_letter : Pattern = $a \/ b$;

def top_word_l {X: SVar} : Pattern = $(kleene_l X top_letter )$ ;
def top_word_r {X: SVar} : Pattern = $(kleene_r X top_letter )$ ;
def top_word   {X: SVar} : Pattern = $(kleene   X top_letter )$ ;

--- Axioms (e suffix indicates over element vars)

axiom domain_words {X: SVar} : $ top_word X $;

axiom functional_epsilon {x : EVar} : $exists x (eVar x == epsilon)$;
axiom functional_a       {x : EVar} : $exists x (eVar x == a)$;
axiom functional_b       {x : EVar} : $exists x (eVar x == b)$;
axiom functional_concat  {w v x: EVar} : $exists x (eVar x == (eVar w .. eVar v))$;

axiom no_confusion_ab_e  : $a != b$;
axiom no_confusion_ae_e  : $~(epsilon C= top_letter)$;
axiom no_confusion_ec_e  {u v: EVar} : $(epsilon == eVar u .. eVar v) -> (epsilon == eVar u) /\ (epsilon == eVar v)$;
axiom no_confusion_cc_e  {u v x y: EVar} : $(x in top_letter) -> (y in top_letter)
                            -> (eVar x .. eVar u == eVar y .. eVar v) -> (eVar x == eVar y) /\ (eVar u == eVar v)$;

axiom assoc_concat_e     {u v w: EVar} : $(eVar u .. eVar v) .. eVar w == eVar u .. (eVar v .. eVar w)$;
axiom identity_left_e    {u : EVar} : $epsilon .. (eVar u) == (eVar u)$;
axiom identity_right_e   {u : EVar} : $(eVar u) .. epsilon == (eVar u)$;

--- Secondary sugar

--- TODO: Remove these (Need to be removed from maude as well.
def nnimp (phi1 phi2: Pattern): Pattern = $ ~phi1 \/ phi2 $;
infixr nnimp: $->>$ prec 24;
def nnequiv (phi1 phi2: Pattern): Pattern = $ (phi1 ->> phi2) /\ (phi2 ->> phi1) $;
infixr nnequiv: $<<->>$ prec 20;
def replus (phi1 phi2: Pattern): Pattern = $ phi1 \/ phi2 $;
infixl replus: $+$ prec 29;

def derivative (l: Pattern) (phi: Pattern) {.box : SVar}: Pattern
= $ctximp_app box (l .. sVar box) phi $;