1Step 1: 2 case split on whether 23 is visited 3Step 2: case in (1) where 23 is visited 4 prove visits to 64 related to visits [2, 4, 6 ...] to 10 5 with equalities 6 ((Mem) ('mem')) (@ addr 64) 7 = ((Mem) ('Mem')) (@ addr 10) 8 and with invariants 9 ((Word32) (('r1' + ((0 - '#seq-visits') * (4 + 4))))) (@ addr 64) 10 ((Word32) ('ret')) (@ addr 64) 11 ((Word32) (('r0' + ((0 - '#seq-visits') * (8 + 8))))) (@ addr 64) 12 ((Word32) ('r9')) (@ addr 64) 13 ((Word32) ('r8')) (@ addr 64) 14 ((Word32) ('r5')) (@ addr 64) 15 ((Word32) ('r11')) (@ addr 64) 16 ((Bool) (ROData('mem'))) (@ addr 64) 17 ((Word32) (('r3' + ((0 - '#seq-visits') * (1 + 1))))) (@ addr 64) 18 ((Word32) ('r14')) (@ addr 64) 19 ((Word32) ('r7')) (@ addr 64) 20 ((Word32) ('r6')) (@ addr 64) 21 ((Word32) ('r10')) (@ addr 64) 22 ((Word32) ('r13')) (@ addr 64) 23 ((RelWrapper) (StackWrapper(((Word32) (('r13' + 0))), ((Mem) ('stack'))))) (@ addr 64) 24 ((Word32) ('p#v')) (@ addr 10) 25 ((Word32) (('loop#2#count' + (('#seq-visits' * -2) * 1)))) (@ addr 10) 26 ((Word32) (('i#v' + (('#seq-visits' * -2) * 1)))) (@ addr 10) 27 .. proven. 28Step 3: case in (2) where the length of the sequence < 2 29 Prove the number of visits to 64 is in {0 ..< 3} 30 .. proven. 31Step 4: 32 Prove the number of visits to 10 is in {0 ..< 6} 33 .. proven. 34Step 5: 35 prove all verification conditions 36 .. proven. 37Step 6: case in (2) where the length of the sequence is i + 2 38 Prove the number of visits to 64 is in {i + 0 ..< i + 3} 39 .. proven. 40Step 7: 41 Prove the number of visits to 10 is in {i + 0 ..< i + 5} 42 .. proven. 43Step 8: 44 prove all verification conditions 45 .. proven. 46Step 9: case in (1) where 23 is not visited 47 prove visits to 64 related to visits [3, 5, 7 ...] to 73 48 with equalities 49 ((Mem) ('mem')) (@ addr 64) 50 = ((Mem) ('Mem.1')) (@ addr 73) 51 and with invariants 52 ((Word32) (('r1' + ((0 - '#seq-visits') * (4 + 4))))) (@ addr 64) 53 ((Word32) ('ret')) (@ addr 64) 54 ((Word32) (('r0' + ((0 - '#seq-visits') * (8 + 8))))) (@ addr 64) 55 ((Word32) ('r9')) (@ addr 64) 56 ((Word32) ('r8')) (@ addr 64) 57 ((Word32) ('r5')) (@ addr 64) 58 ((Word32) ('r11')) (@ addr 64) 59 ((Bool) (ROData('mem'))) (@ addr 64) 60 ((Word32) (('r3' + ((0 - '#seq-visits') * (1 + 1))))) (@ addr 64) 61 ((Word32) ('r14')) (@ addr 64) 62 ((Word32) ('r7')) (@ addr 64) 63 ((Word32) ('r6')) (@ addr 64) 64 ((Word32) ('r10')) (@ addr 64) 65 ((Word32) ('r13')) (@ addr 64) 66 ((RelWrapper) (StackWrapper(((Word32) (('r13' + 0))), ((Mem) ('stack'))))) (@ addr 64) 67 ((Word32) ('p#v')) (@ addr 73) 68 ((Word32) (('loop#2#count' + (('#seq-visits' * -2) * 1)))) (@ addr 73) 69 ((Word32) (('i#v' + (('#seq-visits' * -2) * 1)))) (@ addr 73) 70 .. proven. 71Step 10: case in (9) where the length of the sequence < 2 72 Prove the number of visits to 64 is in {0 ..< 3} 73 .. proven. 74Step 11: 75 Prove the number of visits to 73 is in {0 ..< 7} 76 .. proven. 77Step 12: 78 prove all verification conditions 79 .. proven. 80Step 13: case in (9) where the length of the sequence is j + 2 81 Prove the number of visits to 64 is in {j + 0 ..< j + 3} 82 .. proven. 83Step 14: 84 Prove the number of visits to 73 is in {j + 0 ..< j + 5} 85 .. proven. 86Step 15: 87 prove all verification conditions 88 .. proven. 89 90