result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ]

Start from the conclusion and work back up the proof. Click the arrow to show the parents.

• result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ],

  if the following are true:

  • a = b
  • b = c

  then a = c

  • result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] = result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] with sorted stack [ ], result of sorting els = result of sorting els with sorted stack [ ]
  • result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] with sorted stack [ ] = [ 1, [ 2, [ 3, [ ] ] ] ],

    if the following are true:

    • a = b
    • b = c
    • c = d

    then a = d

    • result of sorting [ 3, [ 2, [ 1, [ ] ] ] ] with sorted stack [ ] = result of sorting (remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ])) with sorted stack [ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ], result of sorting [ el, rem ] with sorted stack sl = result of sorting (remaining elements after [ el, rem ] is popped at index (index of the maximum value in stack [ el, rem ])) with sorted stack [ maximum value in stack [ el, rem ], sl ]
    • result of sorting (remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ])) with sorted stack [ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ] = result of sorting [ 2, [ 1, [ ] ] ] with sorted stack [ 3, [ ] ],

      if the following are true:

      • remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ]) = [ 2, [ 1, [ ] ] ]
      • [ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ] = [ 3, [ ] ]

      then result of sorting (remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ])) with sorted stack [ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ] = result of sorting [ 2, [ 1, [ ] ] ] with sorted stack [ 3, [ ] ]

      • remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ]) = [ 2, [ 1, [ ] ] ],

        if the following are true:

        • a = b
        • b = c

        then a = c

        • remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ]) = remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 0,

          if index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ] = 0, then remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index (index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ]) = remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 0

          • index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ] = 0, index of the maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ] = 0
        • remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 0 = [ 2, [ 1, [ ] ] ], remaining elements after [ 3, [ 2, [ 1, [ ] ] ] ] is popped at index 0 = [ 2, [ 1, [ ] ] ]
      • [ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ] = [ 3, [ ] ],

        if maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ] = 3, then [ maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ], [ ] ] = [ 3, [ ] ]

        • maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ] = 3, maximum value in stack [ 3, [ 2, [ 1, [ ] ] ] ] = 3
    • result of sorting [ 2, [ 1, [ ] ] ] with sorted stack [ 3, [ ] ] = [ 1, [ 2, [ 3, [ ] ] ] ],

      if the following are true:

      • a = b
      • b = c
      • c = d

      then a = d

      • result of sorting [ 2, [ 1, [ ] ] ] with sorted stack [ 3, [ ] ] = result of sorting (remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ])) with sorted stack [ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ], result of sorting [ el, rem ] with sorted stack sl = result of sorting (remaining elements after [ el, rem ] is popped at index (index of the maximum value in stack [ el, rem ])) with sorted stack [ maximum value in stack [ el, rem ], sl ]
      • result of sorting (remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ])) with sorted stack [ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ] = result of sorting [ 1, [ ] ] with sorted stack [ 2, [ 3, [ ] ] ],

        if the following are true:

        • remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ]) = [ 1, [ ] ]
        • [ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ] = [ 2, [ 3, [ ] ] ]

        then result of sorting (remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ])) with sorted stack [ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ] = result of sorting [ 1, [ ] ] with sorted stack [ 2, [ 3, [ ] ] ]

        • remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ]) = [ 1, [ ] ],

          if the following are true:

          • a = b
          • b = c

          then a = c

          • remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ]) = remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 0,

            if index of the maximum value in stack [ 2, [ 1, [ ] ] ] = 0, then remaining elements after [ 2, [ 1, [ ] ] ] is popped at index (index of the maximum value in stack [ 2, [ 1, [ ] ] ]) = remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 0

            • index of the maximum value in stack [ 2, [ 1, [ ] ] ] = 0, index of the maximum value in stack [ 2, [ 1, [ ] ] ] = 0
          • remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 0 = [ 1, [ ] ], remaining elements after [ 2, [ 1, [ ] ] ] is popped at index 0 = [ 1, [ ] ]
        • [ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ] = [ 2, [ 3, [ ] ] ],

          if maximum value in stack [ 2, [ 1, [ ] ] ] = 2, then [ maximum value in stack [ 2, [ 1, [ ] ] ], [ 3, [ ] ] ] = [ 2, [ 3, [ ] ] ]

          • maximum value in stack [ 2, [ 1, [ ] ] ] = 2, maximum value in stack [ 2, [ 1, [ ] ] ] = 2
      • result of sorting [ 1, [ ] ] with sorted stack [ 2, [ 3, [ ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ],

        if the following are true:

        • a = b
        • b = c
        • c = d

        then a = d

        • result of sorting [ 1, [ ] ] with sorted stack [ 2, [ 3, [ ] ] ] = result of sorting (remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ])) with sorted stack [ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ], result of sorting [ el, rem ] with sorted stack sl = result of sorting (remaining elements after [ el, rem ] is popped at index (index of the maximum value in stack [ el, rem ])) with sorted stack [ maximum value in stack [ el, rem ], sl ]
        • result of sorting (remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ])) with sorted stack [ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ] = result of sorting [ ] with sorted stack [ 1, [ 2, [ 3, [ ] ] ] ],

          if the following are true:

          • remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ]) = [ ]
          • [ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ]

          then result of sorting (remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ])) with sorted stack [ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ] = result of sorting [ ] with sorted stack [ 1, [ 2, [ 3, [ ] ] ] ]

          • remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ]) = [ ],

            if the following are true:

            • a = b
            • b = c

            then a = c

            • remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ]) = remaining elements after [ 1, [ ] ] is popped at index 0,

              if index of the maximum value in stack [ 1, [ ] ] = 0, then remaining elements after [ 1, [ ] ] is popped at index (index of the maximum value in stack [ 1, [ ] ]) = remaining elements after [ 1, [ ] ] is popped at index 0

              • index of the maximum value in stack [ 1, [ ] ] = 0, index of the maximum value in stack [ x, [ ] ] = 0
            • remaining elements after [ 1, [ ] ] is popped at index 0 = [ ], remaining elements after [ x, [ ] ] is popped at index 0 = [ ]
          • [ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ],

            if maximum value in stack [ 1, [ ] ] = 1, then [ maximum value in stack [ 1, [ ] ], [ 2, [ 3, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ]

            • maximum value in stack [ 1, [ ] ] = 1, maximum value in stack [ x, [ ] ] = x
        • result of sorting [ ] with sorted stack [ 1, [ 2, [ 3, [ ] ] ] ] = [ 1, [ 2, [ 3, [ ] ] ] ], result of sorting [ ] with sorted stack sl = sl