proposition: Theorem reduction' phi : incl (FV phi) nil -> FSATd phi <-> MSLSAT (encode' phi).
proof: Proof. intros HV. split. - eintros (D & M & rho & [L HL] & [H2] % discrete_iff & [f H3] & H4). pose (f' (p : D * D) := let (d, e) := p in f ([d; e])). destruct (@discrete_nodup D L H2) as [L'[HL1 HL2]]. assert (HL2' : forall x, x el L') by auto. assert (H3' : forall v, i_atom (P:=tt) v <-> f' (Vector.hd v, Vector.hd (Vector.tl v)) = true). { intros v. unfold decider, reflects in H3. now rewrite (H3 v), (vec_inv2 v) at 1. } exists (@env2stack D L' H2 rho), (@interp2heap D L' H2 f'). split. + now eapply interp2heap_fun. + cbn. split; try now eapply reduction_forwards. apply guarded; trivial. exact (rho 0). - intros (s & h & _ & H). cbn in H. destruct H as [H' H]. destruct H' as (v & l & -> & Hl). exists (dom h), (model h), (@env s h (loc2dom Hl)). repeat split. + apply dom_listable. + apply dom_discrete. + intros [ ]. apply model_dec. + apply reduction_backwards; trivial. intros x Hx. destruct (HV x Hx). Qed.
imports: Undecidability.FOL(Semantics.FiniteTarski.Full) Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.SeparationLogic(MSL) Undecidability.Shared(Dec) Undecidability.Synthetic.DecidabilityFacts List Undecidability.Synthetic.Definitions