proposition: Theorem transformed_correctness : forall (net : transformed_network) tr, step_dup_star (params := transformed_multi_params) step_async_init net tr -> @mutual_exclusion num_Clients (nwState (revertNetwork net)).
proof: Proof. Proof using. intros. pose proof @true_in_reachable_transform _ (LockServ_MultiParams num_Clients) (fun net : network => mutual_exclusion (nwState net)) (@true_in_reachable_mutual_exclusion num_Clients). unfold true_in_reachable in *. apply H0. unfold reachable. eauto. Qed.
imports: Verdi(Verdi LockServ) Verdi(SeqNumCorrect)