Example Proofs Using Theorem 8.22 of Gries & Schneider

1. Prove (*i | 0<i≤m : 2i) = (*i | 0<i≤2m ∧ even.i : i)

Solution::

     (*i | 0<i≤2m ∧ even.i : i)

 =      < (8.22), with x,y,f.j := i,j,2j >

     (*j | (0<i≤2m ∧ even.i)[i:=2j] : i[i:=2j])

 =      < textual substitution >

     (*j | 0<2j≤2m ∧ even(2j) : 2j)

 =      < even(2j) ≡ true, (3.39) >

     (*j | 0<2j≤2m : 2j)

 =      < 0<2j≤2m  ≡  0<j≤m >

     (*j | 0<j≤m : 2j)

 =      < (8.21), x,y := j,i >

     (*i | 0<i≤m : 2i)

2. Prove (*i | -8<i≤0 : f.i) = (*j | 0≤j<8 : f(-j))

     (*i | -8<i≤0 : f.i)  

 =      < 8.22, with x,y,f.j := i,j,-j >

     (*j | -8<-j≤0 : f.(-j))  

 =      < rewrite range (using a<b ≡ -a>-b) >

     (*j | 0≤j<8 : f(-j))