L1: new_components;f0 = {}
L2: f0;new_components~ = {}

∀  m   ·
	∃ f · 
	  f∈components(m) ↔ components(m)  ∧
	  container(m)⊆f ∧ f;f⊆f ∧
	  id∩f=∅
instancier pour Mdl et Inst

Montrer les deux lemmes (L1, L2)

Faire deux cas en fonction des valeurs de Mdl (dc m = Mdl)

Magic (SMT)

instancier exist avec acycl 
acycl: (new_components∼;f;inst_components;f0) ∪ (new_components∼;f;(new_components ∪ inst_components)) ∪ f0

faire apparaitre les cas (Magic SMT)

distribuer les unions à gauche de l'inclusion

faire les rewrite L1 L2

Auto ????? Magic ... 

====================

pour unfold_node acyclic
 ((ran(new_c) × {dest});f) ∪ (ran(new_c) × {dest})   ∪ f

============================================
apply_pattern_link_oo:

ajouter XXX;(inst_comp \/ new_com); (inst_comp\/new_comp)~= XXX