Ejercicio1.slspec

Pc : {|s|=2*|t| ∧ i=0}
Qc : {|s|=2*|t| ∧L (∀k: ℤ)(0≤k<(|s| div 2) ⟹L t[k] = s[2*k] + s[2*k+1])}
I : {|s|=2*|t| ∧ 0≤i≤|s| ∧ (i mod 2)=0 ∧L (∀k: ℤ)(0≤k<(i div 2) ⟹L t[k] = s[2*k] + s[2*k+1])}
B : {i<|s|}

--------------------------------------------------------------------------------

Pc ⟹ I
|s|=2*|t| ⟹ |s|=2*|t|
i=0 ⟹ 0≤i≤|s| ∧ (i mod 2)=0
i=0 ⟹ (∀k: ℤ)(0≤k<(i div 2) ⟹L t[k] = s[2*k] + s[2*k+1])
    ≡ (∀k: ℤ)(0≤k<(0 div 2) ⟹L t[k] = s[2*k] + s[2*k+1])
    ≡ (∀k: ℤ)(0≤k<0 ⟹L t[k] = s[2*k] + s[2*k+1])
    ≡ True Pues el antecedente 0≤k<0 es siempre False

--------------------------------------------------------------------------------

(I ∧ ¬B) ⟹ Qc
I ∧ ¬B ≡ |s|=2*|t| ∧ 0≤i≤|s| ∧ (i mod 2)=0 ∧L (∀k: ℤ)(0≤k<(i div 2) ⟹L t[k] = s[2*k] + s[2*k+1]) ∧ ¬(i<|s|)
Qc ≡ |s|=2*|t| ∧L (∀k: ℤ)(0≤k<(|s| div 2) ⟹L t[k] = s[2*k] + s[2*k+1])

Observemos que del I ∧ ¬B vale lo siguiente:
0≤i≤|s| ∧ ¬(i<|s|)
≡ 0≤i≤|s| ∧ i≥|s|
≡ i=|s|

Implicar esta parte de Qc es trivial:
|s|=2*|t| ⟹ |s|=2*|t|

Finalmente:
i=|s| ∧ (∀k: ℤ)(0≤k<(i div 2) ⟹L ...) ⟹ (∀k: ℤ)(0≤k<(|s| div 2) ⟹L ...)

--------------------------------------------------------------------------------

{I ∧ B} S {I} ⟺ I ∧ B ⟹ wp(S, I)
S1 ≡ t[i div 2] := s[i]+s[i+1]
S2 ≡ i := i+2
S ≡ S1;S2

wp(S, I) ≡ wp(S1, wp(S2, I)) // Axioma 3

wp(S2, I)
≡ wp(i := i+2, I)
≡ def(i) ∧L I(i := i+2) // Axioma 1. Además asumimos que todas las variables están definidas
≡ |s|=2*|t| ∧ 0≤i+2≤|s| ∧ (i+2 mod 2)=0 ∧L (∀k: ℤ)(0≤k<(i+2 div 2) ⟹L t[k] = s[2*k] + s[2*k+1])
≡ E2

wp(S1, wp(S2, I))
≡ wp(S1, E2)
≡ wp(t[i div 2] := s[i]+s[i+1], E2)
≡ wp(setAt(t, i div 2, s[i]+s[i+1]), E2)
≡ |s|=2*|t|
    ∧ 0≤i+2≤|s|
    ∧ 0≤(i div 2)<|t|
    ∧ (i+2 mod 2)=0
    ∧L (∀k: ℤ)(0≤k<(i+2 div 2) ⟹L setAt(t, i div 2, s[i]+s[i+1])[k] = s[2*k] + s[2*k+1])
≡ E1

qvq: I ∧ B ⟹ wp(S, I) ≡ E1

Implicar esta parte es trivial:
|s|=2*|t| ⟹ |s|=2*|t|

Observemos que del I ∧ B vale lo siguiente:
0≤i≤|s| ∧ i<|s| ≡ 0≤i<|s|

A su vez, como |s| e i son pares, no puede ser i=|s|-1, por lo tanto:
|s|=2*|t| ∧ (i mod 2)=0 ∧ 0≤i<|s| ⟹ 0≤i<|s|-1

Con esto podemos implicar esta parte de E1:
0≤i<|s|-1 ≡ 2≤i+2<|s|+1 ≡ 2≤i+2≤|s|
0≤i ∧ i+2≤|s| ⟹ 0≤i+2≤|s|

Para implicar 0≤(i div 2)<|t| podemos hacer esto:
0≤i<|s| ∧ (i mod 2)=0
≡ 0≤i<2*|t| ∧ (i mod 2)
⟹ 0≤(i div 2)<|t| // Aplico div en ambos lados de la desigualdad de i

Observemos que:
(i+2 mod 2)=0 ⟺ (i mod 2)=0
Y por lo tanto implicar esta parte también es trivial pues es exactamente lo mismo que tenemos en el I:
(i mod 2)=0 ⟹ (i mod 2)=0

Finalmente, qvq:
(∀k: ℤ)(0≤k<(i div 2) ⟹L t[k] = s[2*k] + s[2*k+1])
⟹ (∀k: ℤ)(0≤k<(i+2 div 2) ⟹L setAt(t, i div 2, s[i]+s[i+1])[k] = s[2*k]+s[2*k+1])

Simplificamos esta parte de E1 primero:
(∀k: ℤ)(0≤k<(i+2 div 2) ⟹L setAt(t, i div 2, s[i]+s[i+1])[k] = s[2*k]+s[2*k+1])
≡ (∀k: ℤ)(0≤k<(i div 2)+1 ⟹L setAt(t, i div 2, s[i]+s[i+1])[k] = s[2*k]+s[2*k+1])
≡ (∀k: ℤ)(0≤k<(i div 2) ⟹L t[k] = s[2*k] + s[2*k+1]) ∧ setAt(t, i div 2, s[i]+s[i+1])[i div 2] = s[2*k]+s[2*k+1]
≡ (∀k: ℤ)(0≤k<(i div 2) ⟹L t[k] = s[2*k] + s[2*k+1]) ∧ s[i]+s[i+1] = s[2*(i div 2)]+s[2*(i div 2)+1]
≡ (∀k: ℤ)(0≤k<(i div 2) ⟹L t[k] = s[2*k] + s[2*k+1]) ∧ s[i]+s[i+1] = s[i]+s[i+1]
≡ (∀k: ℤ)(0≤k<(i div 2) ⟹L t[k] = s[2*k] + s[2*k+1])

En efecto, es lo que queríamos implicar.