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