Hanoi:::OBJECT
Hanoi.stackA[] elements != null
Hanoi.stackB[] elements != null
Hanoi.stackC[] elements != null
size(Hanoi.stackC[]) == - size(Hanoi.stackA[]) - size(Hanoi.stackB[]) + 5
===========================================================================
Hanoi.putOnA():::ENTER
size(Hanoi.stackA[]) <= 2
size(Hanoi.stackA[]) one of { 0, 1, 2 }
size(Hanoi.stackB[]) == 0  (mod 2)
size(Hanoi.stackB[]) one of { 2, 4 }
size(Hanoi.stackC[]) >= 1
size(Hanoi.stackC[]) one of { 1, 2, 3 }
size(Hanoi.stackA[]) != size(Hanoi.stackC[])
size(Hanoi.stackA[])-1 != size(Hanoi.stackC[])-1
===========================================================================
Hanoi.putOnA():::EXIT
size(Hanoi.stackA[])-1 == orig(size(Hanoi.stackA[]))
size(Hanoi.stackA[]) >= 1
size(Hanoi.stackA[]) one of { 1, 2, 3 }
size(Hanoi.stackB[]) one of { 1, 2, 3 }
size(Hanoi.stackC[]) == 1  (mod 2)
size(Hanoi.stackC[]) one of { 1, 3 }
orig(Hanoi.stackA[]) is a subsequence of Hanoi.stackA[]
Hanoi.stackB[] is a subsequence of orig(Hanoi.stackB[])
Hanoi.stackC[] is a subsequence of orig(Hanoi.stackC[])
size(Hanoi.stackA[]) != size(Hanoi.stackB[])-1
size(Hanoi.stackA[]) != size(Hanoi.stackC[])-1
size(Hanoi.stackA[]) != orig(size(Hanoi.stackC[]))-1
size(Hanoi.stackA[])-1 != size(Hanoi.stackB[])
size(Hanoi.stackB[]) != size(Hanoi.stackC[])-1
size(Hanoi.stackB[]) != orig(size(Hanoi.stackC[]))-1
size(Hanoi.stackB[])-1 != orig(size(Hanoi.stackA[]))-1
size(Hanoi.stackB[])-1 != orig(size(Hanoi.stackC[]))
size(Hanoi.stackC[]) != orig(size(Hanoi.stackB[]))
size(Hanoi.stackC[])-1 != orig(size(Hanoi.stackB[]))-1
orig(size(Hanoi.stackA[]))-1 != orig(size(Hanoi.stackC[]))-1
===========================================================================
Hanoi.putOnB():::ENTER
size(Hanoi.stackA[]) >= 1
size(Hanoi.stackC[]) == 1  (mod 2)
size(Hanoi.stackC[]) one of { 1, 3 }
size(Hanoi.stackA[])-1 != size(Hanoi.stackB[])
===========================================================================
Hanoi.putOnB():::EXIT
size(Hanoi.stackB[])-1 == orig(size(Hanoi.stackB[]))
size(Hanoi.stackA[]) == 1  (mod 2)
size(Hanoi.stackA[]) one of { 1, 3 }
Hanoi.stackA[] is a subsequence of orig(Hanoi.stackA[])
orig(Hanoi.stackB[]) is a subsequence of Hanoi.stackB[]
Hanoi.stackC[] is a subsequence of orig(Hanoi.stackC[])
size(Hanoi.stackA[]) != orig(size(Hanoi.stackC[]))-1
size(Hanoi.stackA[])-1 != orig(size(Hanoi.stackC[]))
size(Hanoi.stackB[]) != orig(size(Hanoi.stackA[]))
size(Hanoi.stackB[])-1 != size(Hanoi.stackC[])
size(Hanoi.stackB[])-1 != orig(size(Hanoi.stackA[]))-1
size(Hanoi.stackC[]) != orig(size(Hanoi.stackA[]))
size(Hanoi.stackC[])-1 != orig(size(Hanoi.stackA[]))-1
size(Hanoi.stackC[])-1 != orig(size(Hanoi.stackB[]))-1
orig(size(Hanoi.stackC[])) == - size(Hanoi.stackB[]) - orig(size(Hanoi.stackA[])) + 6
===========================================================================
Hanoi.putOnC():::ENTER
size(Hanoi.stackA[]) == 1  (mod 2)
size(Hanoi.stackA[]) one of { 1, 3, 5 }
size(Hanoi.stackB[]) != size(Hanoi.stackC[])-1
size(Hanoi.stackB[])-1 != size(Hanoi.stackC[])
===========================================================================
Hanoi.putOnC():::EXIT
size(Hanoi.stackC[])-1 == orig(size(Hanoi.stackC[]))
size(Hanoi.stackB[]) == 0  (mod 2)
size(Hanoi.stackB[]) one of { 0, 2, 4 }
size(Hanoi.stackC[]) >= 1
Hanoi.stackA[] is a subsequence of orig(Hanoi.stackA[])
Hanoi.stackB[] is a subsequence of orig(Hanoi.stackB[])
orig(Hanoi.stackC[]) is a subsequence of Hanoi.stackC[]
size(Hanoi.stackA[]) != size(Hanoi.stackC[])
size(Hanoi.stackA[]) != orig(size(Hanoi.stackB[]))-1
size(Hanoi.stackA[]) != orig(size(Hanoi.stackC[]))-1
size(Hanoi.stackA[])-1 != size(Hanoi.stackC[])-1
size(Hanoi.stackA[])-1 != orig(size(Hanoi.stackB[]))
size(Hanoi.stackB[]) != orig(size(Hanoi.stackA[]))
size(Hanoi.stackB[])-1 != orig(size(Hanoi.stackA[]))-1
size(Hanoi.stackC[]) != orig(size(Hanoi.stackB[]))
size(Hanoi.stackC[])-1 != orig(size(Hanoi.stackB[]))-1
orig(size(Hanoi.stackB[])) != orig(size(Hanoi.stackC[]))-1
orig(size(Hanoi.stackB[])) == - size(Hanoi.stackC[]) - orig(size(Hanoi.stackA[])) + 6
===========================================================================
Hanoi.start():::ENTER
size(Hanoi.stackA[]) == size(Hanoi.stackB[]) == size(Hanoi.stackC[])
Hanoi.stackA[] == []
Hanoi.stackB[] == []
Hanoi.stackC[] == []
size(Hanoi.stackA[]) == 0
===========================================================================
Hanoi.start():::EXIT
size(Hanoi.stackB[]) == size(Hanoi.stackC[]) == orig(size(Hanoi.stackA[]))
                     == orig(size(Hanoi.stackB[])) == orig(size(Hanoi.stackC[]))
Hanoi.stackA[] contains no nulls and has only one value, of length 5
Hanoi.stackB[] == []
Hanoi.stackC[] == []
size(Hanoi.stackA[]) == 5