proposition: Theorem machine_correctness {s t} : closed s -> (L.eval s t) <-> (exists y, flatten y = t /\ machine (closure [] s) [] y).
proof: Proof. move=> Hs. split. - move=> /machine_simulation. by apply. - move=> [?] [+] /machine_inverse_simulation. move=> ->. rewrite flatten_term. move=> /closed_dcl in Hs. by apply. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun