The final stages of the proof.

%%lemma('Ground Reducible Graph').
A ground non-empty acceptable graph can be reduced by one of the reduction rules.
Proof:
Either the %%linkLemma('Ground Explicit Type Reduction'). or the %%linkLemma('Ground Triple Reduction'). applies.

%%lemma('Reducible Graph').
A non-empty acceptable graph can be reduced by one of the reduction rules.
Proof:
Suppose not. Then by the %%linkLemma('ground reducible graph'). we have that there must be a blank node b. Moreover, by the %%linkLemma(list). b cannot be of type rdf:List. Hence, if b were the object of a triple with a uriref subject, we can apply either the %%linkLemma('GGB Triple Reduction'). or the %%linkLemma('blank explicit type reduction'). . Thus, by the %%linkLemma('blank node'). , without loss of generality, we have that b is not the object of any triple.
Since b is not of type rdf:List, it must be of category unnamedIndividual, allDifferent, %%dl_only(Lvl,'unnamedDataRange, '). %%dl_only(Lvl,'description, '). or restriction. By the %%linkLemma('unnamed individual'). the first possibility is excluded. %%dl_only(Lvl,'Since the '). %%Lvl=dl->linkLemma('Description Comparison Reduction');true. %%dl_only(Lvl,'does not apply, b is not the subject of a triple with predicate owl:disjointWith, or owl:equivalentClass.'). The conditions on b and g now meet the premises of the %%Lvl=dl->linkLemma('Structured Nodes');linkLemma('first structure reduction'). and so g is, after all, reducible.

We now can prove the main results:

Correspondence Theorem
Every acceptable graph corresponds to an abstract syntax tree.
Proof:
By induction, with initial step furnished by the %%linkLemma('empty graph'). and inductive step by the %%linkLemma('Reducible Graph'). .
Corollary: Sufficiency Theorem
Every acceptable graph is mappable.