module BinTrees

sig BinTree {
	root : one NonEmptyNode
}

abstract sig Node {
}

sig NonEmptyNode extends Node {
	val : one Val,
	leftChild: one Node,
	rightChild : one Node
}

sig EmptyNode extends Node {
}

sig Val {
}

fun nodes[bt : BinTree] : set Node {
	 bt.root.*(leftChild+rightChild)
}

// All nodes have exactly one parent 
fact AtMostOneParent {
	all bt: BinTree | 
		all n : nodes[bt] | 
			one n.~(leftChild+rightChild)
}

// All nodes belong to at least one tree
fact AllNodesBelongToAtLeastOneBinTree {
//	all n : Node | some bt: BinTree |
//		n in nodes[bt]
	Node in nodes[BinTree] // Simplified way. Also removes the $Show_bt relation.
}

// Left child and right child are different
fact LeftChildIsDifferentThanRightChild {
	all bt: BinTree |
		all n : nodes[bt] - EmptyNode |
			(n.leftChild != n.rightChild)
}

// Two different nodes have different values
// A value is unique
fact NonEmptyNodesHaveDifferentValues {
	all bt: BinTree |
		all disj n1,n2 : nodes[bt] - EmptyNode |
			n1.val != n2.val

	all v : Val | one v.~val
}

// Acyclic tree
fact NoCycle {
//	all bt: BinTree |
//		no n: nodes[bt] |
//			n in n.^(leftChild+rightChild)
	no n : Node | n in n.^(leftChild+rightChild) // Simplified notation.
}

// If the left child is an empty node, then the right child is an empty node
// hint: the equivalence relation <-> can be defined using <=> or iff
fact LeftChildIffRightChild {
}

// There is exactly the same number of nodes on the left branch and the right branch of the tree
fact BinTreesAreBalanced {
}


pred Show {
	one BinTree
}

run Show for 8