Library LangAlg.terms_graphs
Using the translation of terms into primed weak terms we can reduce the axiomatic containment of
𝐓
-terms to the ordering of graphs.
Set Implicit Arguments
.
Require
Import
terms_w_terms
w_terms_graphs
.
Definition
𝕲
t
{
X
} (
u
:
𝐓
X
) :=
𝕲
w
π{
𝐓
_to_
𝐖'
u
}
.
Theorem
𝐓
_inf_is_weak_graph_inf
{
X
:
Set
} `{
decidable_set
X
}:
∀
u
v
:
𝐓
X
,
u
≤
v
↔
𝕲
t
u
≲
𝕲
t
v
.