/*@ predicate positive_power_of_2 (integer i) = i > 0 && (i == 1 || ((i & 1) == 0 && positive_power_of_2 (i >> 1))); lemma positive_power_of_2 (1); lemma positive_power_of_2 (2); lemma positive_power_of_2 (4); lemma !positive_power_of_2 (7); */https://stackoverflow.com/questions/64268418/how-do-i-write-an-is-power-of-2-predicate-in-acsl