# Library LangAlg.w_terms_graphs

This module is devoted to the translation of weak terms into graphs.

Set Implicit Arguments.

Require Export sp_terms_graphs w_terms.

Section s.
Variable X : Set.
Variable Λ : decidable_set X.

A weak graph is a pair of a graph and a set of tests.
Definition weak_graph : Set := (graph nat X) × list X.

We define the graph of a weak term using the graph of its series-parallel term, or the point graph (0,[],0) in the case of the constant None.
Definition 𝕲w (x : 𝐖 X) : weak_graph :=
match x with
| (Some u,A)(𝕲 u,A)
| (None,A)((0,[],0),A)
end.

We extend the ordering of graphs to an ordering of weak graphs.
Global Instance weak_graph_inf : SemSmaller weak_graph :=
fun g hsnd h snd g snd g fst g fst h.

This allows us to obtain the following theorem, equating the axiomatic containment of weak terms to the ordering of weak graphs.
Theorem 𝐖_inf_is_weak_graph_inf : x y, x y 𝕲w x 𝕲w y.

We can test the ordering of weak graph using a boolean function.
Definition weak_graph_infb (g h : weak_graph) :=
forallb (fun nexistsb (eqX n) (snd g)) (snd h)
&& ex_is_morphismb NatNum NatNum _ (snd g) (fst h) (fst g).

Lemma weak_graph_infb_correct g h :
weak_graph_infb g h = true g h.
End s.