Question 6 - Given the right code for an implementation of a tree

A tree can be implemented in Alloy as below:

sig Tree {
	root: lone Node,
	successors: Node -> Node
}

sig Node {}

fact notCyclic {
	no n:Node | n in n.^(Tree.successors)
}

fact binaryTree {
	all n:Node | #n.(Tree.successors) = 2 or #n.(Tree.successors) = 0
}

fact allNodesBelongToOneTree {
	// ???
}

fact singleMapping {
	all n,x,y:Node |
		x -> n in Tree.successors and y -> n in Tree.successors
			implies x = y
}

pred show() {}

run show for 5 but 1 Tree

	[Tree_Q6.jpg]


Which one of the following is the correct implementation of the fact allNodesBelongToOneTree? 

	all n: Node | one t:Tree  | n in t.*root.(t.successors)

	all n: Node | some t:Tree | n in t.root.*(t.successors)

	all n: Node | one t:Tree  | n in t.root.(t.*successors)