Collo di bottiglia nella logica Hoare Impossibile arrivare al mio {p} da {q}

Question

{Q} = {n> 0}
C1 = i: = 1;
C2 = c: = 1;
C3 = p: = 0;
{P} = {i <= n, p = fib (i-1), c = fib (i)}

La mia mancanza di comprensione nei confronti della regola delle conseguenze nella logica di Hoare mi sta bloccando dal trovare la soluzione che spero che qualcuno possa far luce su come posso avvicinarmi a questo con una minima astrazione del processo.

{R} = {i <= n, p = fib (i-1), c = fib (i) [i 1]} i: = 1; {i <= n, p = fib (i-1) , c = fib (i)}

{R} = {1 <= n, p = fib (0), c = fib (1)}

{R} = {1 <= n, p = 0, c = 1}

{R1} = {1 <= n, p = 0, c = 1 [c 1]} c: = 1; {1 <= n, p = 0, c = 1}

{R1} = {1 <= n, p = 0, true}

{R2} = {1 <= n, p = 0 [p 0]} p: = 0; {1 <= n, p = 0}

{R2} = {1 <= n, true} {1 <= n, p = 0}

{R2} = {1 <= n -> 0> x} :( Non posso arrivare esattamente a N> 0

*modificare

Dalla mia osservazione il problema chiave è indipendentemente dalla sequenza, arriverei sempre a 1 <= n come non equivalente a n> 0, non sono sicuro di come posso eseguire legalmente p-> p 'p' c q 'q'-> q per dimostrare {p} c {q}