You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
37 lines
871 B
37 lines
871 B
6 years ago
|
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
|