Require Import List.
Inductive term : Set :=
| atom : nat -> term
| arr : term -> term -> term.
Definition valuation : Set := nat -> term.
Fixpoint substitute (f: valuation) (t: term) : term :=
match t with
| atom n => f n
| arr s t => arr (substitute f s) (substitute f t)
end.
Definition constraint : Set := ((bool * nat) * (nat * bool)).
Definition models (φ ψ0 ψ1: valuation) : constraint -> Prop :=
fun '((a, x), (y, b)) =>
match φ y with
| atom _ => False
| arr s t => (if b then t else s) = substitute (if a then ψ1 else ψ0) (φ x)
end.
Definition SSemiU (p : list constraint) :=
exists (φ ψ0 ψ1: valuation), forall (c : constraint), In c p -> models φ ψ0 ψ1 c.
Definition inequality : Set := (term * term).
Definition solution (φ : valuation) : inequality -> Prop :=
fun '(s, t) => exists (ψ : valuation), substitute ψ (substitute φ s) = substitute φ t.
Definition SemiU (p: list inequality) :=
exists (φ: valuation), forall (c: inequality), In c p -> solution φ c.
Definition RU2SemiU : term * term * term -> Prop :=
fun '(s0, s1, t) => exists (φ ψ0 ψ1: valuation),
substitute ψ0 (substitute φ s0) = substitute φ t /\ substitute ψ1 (substitute φ s1) = substitute φ t.
Definition LU2SemiU : term * term * term -> Prop :=
fun '(s, t0, t1) => exists (φ ψ0 ψ1: valuation),
substitute ψ0 (substitute φ s) = substitute φ t0 /\ substitute ψ1 (substitute φ s) = substitute φ t1.