Goulot d'étranglement dans la logique hoare incapable d'arriver à mon {p} de {q}

Question

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

Mon manque de compréhension envers la règle de conséquence dans la logique de Hoare me bloque de trouver la solution que j'espère que quelqu'un pourra éclairer comment puis-je aborder cela avec une abstraction minimale du processus.

{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, vrai}

{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} :( Je ne peux pas arriver exactement à n> 0

*Éditer

D'après mon observation, le problème clé est quelle que soit la séquence que j'arriverais toujours à 1 <= n comme n'étant pas équivalent à n> 0, je ne sais pas comment je peux légalement effectuer p-> p 'p' c q 'q' -> q pour prouver {p} c {q}