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)
