proposition: Theorem decomposition_invariant : inductive_invariant step_async step_async_init composed_invariant.
proof: Proof. Proof using. unfold inductive_invariant. intuition. - unfold composed_invariant. simpl. intuition auto using state_invariant_init. - unfold inductive, composed_invariant. intros. match goal with H : step_async _ _ _ |- _ => invcs H end; intuition; simpl in *. + eauto using state_invariant_maintained_deliver. + find_apply_lem_hyp post_net_analyze_sent_packet. intuition eauto 10 using network_invariant_maintained_deliver_new, network_invariant_maintained_deliver_old, nw_nw_distinct_pairs_and_elim, network_network_invariant_sym. + apply distinct_pairs_and_app; eauto using network_network_invariant_maintained_deliver_new, distinct_pairs_and_app_cons. intros. do_in_map. subst. eapply network_network_invariant_maintained_deliver_old; eauto using nw_nw_distinct_pairs_and_elim. simpl; now rewrite <- surjective_pairing. + eauto using state_invariant_maintained_input. + find_apply_lem_hyp post_input_analyze_sent_packet. intuition eauto using network_invariant_maintained_input_new, network_invariant_maintained_input_old. + apply distinct_pairs_and_app; eauto using network_network_invariant_maintained_input_new. intros. do_in_map. subst. apply network_network_invariant_sym. eapply network_network_invariant_maintained_input_old; eauto. simpl. now rewrite <- surjective_pairing. Qed.
imports: Verdi(Verdi)