diff --git a/randmu.py b/randmu.py
index 2c1ed65edf6e4e8fee0603b5f07d9444b179b312..2494a11308e80cd7d42065f747486eda9df064e7 100755
--- a/randmu.py
+++ b/randmu.py
@@ -61,15 +61,9 @@ class And(Propositional):
 
 
     def finalize(self, atoms, guarded, unguarded, fixpoint):
-        if not isinstance(self._left, Variable):
-            self._left.finalize(atoms, guarded, unguarded, fixpoint)
-        else:
-            self._left = random.choice(atoms + guarded)
+        self._left.finalize(atoms, guarded, unguarded, fixpoint)
+        self._right.finalize(atoms, guarded, unguarded, fixpoint)
 
-        if not isinstance(self._right, Variable):
-            self._right.finalize(atoms, guarded, unguarded, fixpoint)
-        else:
-            self._right = random.choice(atoms + guarded)
 
 
 class Or(Propositional):
@@ -93,38 +87,8 @@ class Or(Propositional):
 
 
     def finalize(self, atoms, guarded, unguarded, fixpoint):
-        if not isinstance(self._left, Variable):
-            self._left.finalize(atoms, guarded, unguarded, fixpoint)
-        else:
-            self._left = random.choice(atoms + guarded)
-
-        if not isinstance(self._right, Variable):
-            self._right.finalize(atoms, guarded, unguarded, fixpoint)
-        else:
-            self._right = random.choice(atoms + guarded)
-
-
-
-class Not(Propositional):
-    def __init__(self):
-        self._subformula = Variable(self)
-
-
-    def __str__(self):
-        subformula = str(self._subformula)
-        return "~(%s)" % (subformula,)
-
-
-    def replace(self, what, withw):
-        assert self._subformula == what
-        self._subformula = withw
-
-
-    def finalize(self, atoms, guarded, unguarded, fixpoint):
-        if not isinstance(self._subformula, Variable):
-            self._subformula.finalize(atoms, guarded, unguarded, fixpoint)
-        else:
-            self._subformula = random.choice(atoms + guarded)
+        self._left.finalize(atoms, guarded, unguarded, fixpoint)
+        self._right.finalize(atoms, guarded, unguarded, fixpoint)
 
 
 
@@ -148,10 +112,7 @@ class Box(Modal):
 
 
     def finalize(self, atoms, guarded, unguarded, fixpoint):
-        if not isinstance(self._subformula, Variable):
-            self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
-        else:
-            self._subformula = random.choice(atoms + guarded)
+        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
 
 
 
@@ -171,10 +132,7 @@ class Diamond(Modal):
 
 
     def finalize(self, atoms, guarded, unguarded, fixpoint):
-        if not isinstance(self._subformula, Variable):
-            self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
-        else:
-            self._subformula = random.choice(atoms + guarded)
+        self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
 
 
 
@@ -201,14 +159,11 @@ class Mu(Fixpoint):
 
 
     def finalize(self, atoms, guarded, unguarded, fixpoint):
-        if not isinstance(self._subformula, Variable):
-            if fixpoint == 'nu':
-                guarded = []
-                unguarded = []
+        if fixpoint == 'nu':
+            guarded = []
+            unguarded = []
 
-            self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'mu')
-        else:
-            self._subformula = random.choice(atoms + guarded)
+        self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'mu')
 
 
 
@@ -232,18 +187,15 @@ class Nu(Fixpoint):
 
 
     def finalize(self, atoms, guarded, unguarded, fixpoint):
-        if not isinstance(self._subformula, Variable):
-            if fixpoint == 'mu':
-                guarded = []
-                unguarded = []
+        if fixpoint == 'mu':
+            guarded = []
+            unguarded = []
 
-            self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'nu')
-        else:
-            self._subformula = random.choice(atoms + guarded)
+        self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'nu')
 
 
 
-connectives = [And, And, Or, Or, Not, Box, Diamond, Mu, Nu]
+connectives = [And, And, Or, Or, Box, Diamond, Mu, Nu]
 
 
 class Variable:
@@ -264,7 +216,12 @@ class Variable:
 
 
     def finalize(self, atoms, guarded, unguarded, fixpoint):
-        assert False
+        choice = random.choice(guarded + atoms)
+        if choice in atoms:
+            choice = random.choice([choice, "~%s" % choice])
+
+        variables.remove(self)
+        self._parent.replace(self, choice)