up, tags, aliases
[!proposition]+ Théorème de lecture unique
Pour toute formule f \in \mathcal{F}_{v}
une et une seule des assertions suivantes est verrifée :
f = [0]f = [1]\exists v \in V,\quad f = [v]\exists f' \in \mathcal{F}_{v},\quad f = \neg f'\exists f_1, f_2 \in \mathcal{F}_{v},\quad f = [\vee f_1 f_2]\exists f_1, f_2 \in \mathcal{F}_{v},\quad f = [\wedge f_1 f_2]\exists f_1, f_2 \in \mathcal{F}_{v},\quad f = [\implies f_1 f_2]\exists f_1, f_2 \in \mathcal{F}_{v},\quad f = [\iff f_1 f_2]
De plus :
- dans 3.
v est unique et déterminé
- dans 4.
f' est unique et déterminé
- dans 5. 6. 7. et 8.
f_1 et f_2 sont uniques et déterminés
^thm
