Pattern-Instanciation-On-System-Engineering-Model/Event-B/pseim/preuves.txt

VARIANT: nbre de chemins restant à construire
chemin = {s |-> i | s : subc(root) & i <= mult(s)}
ens des chemins = 
  {ch: subc(root) -> NAT | !s. s:dom(ch) => ch(s) <= mult(s)}

====================
inter({sc·x∈sc∧container∼[sc]⊆sc ∣ sc}) /= {}
en prenant {x}\/f~[{x}]
===================
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

============================================
UNION c. 1..card(to_unfold_c ∩ {c}) ∪ to_unfold_c_in[{c}])
		 ** (containers∼[{c}] +-> 0‥M)

(containers \/ id)~[to_unfold_c \/ dom(to_unfold_c_in)] +-> 0..M \/
containers~[to_unfold_c] ** 0..M \/
to_unfold_c ** 0..0 \/
{c|->i | c:dom(to_unfold_c_in) & i:0..card(to_unfold_c_in[{c}])}

{f | f: ((containers\/id)~[dom(to_unfold_c_in)] \/ dom(to_unfold_c_in) +-> 0..M
   & !c. c:dom(to_unfold_c_in) /\ dom(f) => f(c) : 0..card(to_unfold_c_in[{c}])
   & !c. c:to_unfold_c /\ dom(f) => f(c) = 0
     }
#c * weight(c)
w(c):=w(c)-M^h(c) || ||_sc<c w(sc):=w(sc)+M^(h(c)-1)
c,i --> SC(c)+-> 0..M
sc --> SC(sc) ** {i} +-> 0..M
ordre lexico sur c1,...cN trie par <

(c,i) ==> ajout de (sc,i1) ... (sc,im)
(c,j) ==> ajout de (sc,j1) ... (sc,jm)