proposition: Lemma parent_invariant : forall c : Config, legal c -> forall s : Site, indirect_son1 c s -> exists s1 : Site, direct_son c s1 /\ ancestor c s1 s.
proof: Proof. intros c H. generalize H. elim H. simpl in |- *. intros. elim H1. simpl in |- *. intros. elim H4. intro; auto. unfold not in |- *; auto. exact parent_invariant_inductive. Qed.
imports: DistributedReferenceCounting.machine2.invariant6