- exists, _ := u.getIndex(num)
- if !exists {
- num.metadata.identifier = u.nextUniqueID
- u.nextUniqueID++
- // Find spot to insert based on ordering defined in Axiom 2.
- // TODO: Insert some comments explaining the basic algorithm.
- for i := 0; i < len(u.numbers); i++ {
-
-// if num.number.leftSet != nil {
-// // By assumption, everything is in reduced form by this point,
-// // thus there is precisely one element at this time.
-// _, leftIndex := u.getIndex(num.number.leftSet[0])
-// _, rightIndex := u.getIndex(u.numbers[i])
-// if leftIndex >= rightIndex {
-// // num is NOT LEQ to u.numbers[i]
-// }
-// }
-// if u.numbers[i].rightSet != nil {
-// // TODO: How do I check if the second number's rightSet is less
-// // than or equal to the first number? After all, the first
-// // number isn't on the numberline yet.
-// }
-
-// =================================================================================================
-//// Algorithm
-//foreach u.numbers as oldNum, in increasing order:
-// if newNum <= oldNum:
-// if oldNum <= newNum:
-// // the number are the same, just in a different reduced form.
-// else:
-// // Insert newNum immediately before oldNum
-// else:
-// if more oldNums exist:
-// // loop and try the next oldNum
-// else:
-// // Found a new largest number?
-// =================================================================================================
-
-// if !lessThanOrEqual(num, u.numbers[i]) {
-// if i+1 < len(u.numbers) {
-// // There are still more entries to check.
-// continue
-// } else {
-// // New largest number. Append to numberline.
-// u.numbers = append(u.numbers, num)
-// }
-// } else {
-// // Found insertion spot between two existing numbers.
-// u.numbers = append(u.numbers[:i], num, u.numbers[i:]...)
-// }
- }
+ // Before we can insert a number into the universe, we must first determine
+ // if it is newly discovered. We do this by looking at its ancestors, all
+ // guaranteed to be on the number line by construction, finding three
+ // cases:
+ //
+ // 1. There are zero ancestors.
+ // We have rediscovered 0 and can abort the insertion unless creating
+ // a brand new universe.
+ //
+ // 2. There is one ancestor.
+ // If the number extends the number line, it is new, otherwise it will
+ // be similar to a form with two ancestors and should be ignored since
+ // the two ancestor form is a better visual representation.
+ //
+ // 3. There are two ancestors.
+ // The number is only new if both ancestors are side-by-side on the
+ // number line.
+
+ ancestorCount := num.leftSet.cardinality() + num.rightSet.cardinality()
+ switch ancestorCount {
+ case 0:
+ if u.cardinality() == 0 {
+ num.identifier = u.nextUniqueID
+ u.nextUniqueID++
+ u.numbers = append(u.numbers, num)
+ }
+ case 1:
+ if num.leftSet.cardinality() == 1{
+ index := u.getIndex(num.leftSet.members[0])
+ num.identifier = u.nextUniqueID
+ u.nextUniqueID++
+ if index+1 == u.cardinality() {
+ u.numbers = append(u.numbers, num)
+ }
+ } else {
+ index := u.getIndex(num.rightSet.members[0])
+ num.identifier = u.nextUniqueID
+ u.nextUniqueID++
+ if index == 0 {
+ u.numbers = append(u.numbers[:1], u.numbers...)
+ u.numbers[0] = num
+ }
+ }
+ case 2:
+ leftIndex := u.getIndex(num.leftSet.members[0])
+ rightIndex := u.getIndex(num.rightSet.members[0])
+ if leftIndex+1 == rightIndex {
+ num.identifier = u.nextUniqueID
+ u.nextUniqueID++
+ u.numbers = append(u.numbers[:rightIndex+1], u.numbers[rightIndex:]...)
+ u.numbers[rightIndex] = num
+ }