Proving the LOOP function

We must demonstrate that our guess is good, i.e.

   f = [WHILE]
     = ( R < Y --> ident ) | ( R >= Y and Y > 0 --> Q,R := Q+R/Y, R mod Y )

1. show f behaves like identity when the loop boolean is false
2. show dom(f) = dom([WHILE])
3. show f = [IF] o f where IF is made of the loop components
   
   [IF] = ( R >= Y --> Q,R := Q+1,R-Y ) | ( R < Y --> ident )
   
   so compute the composition [IF] o f =

      ( ( R >= Y --> Q,R := Q+1,R-Y ) | ( R < Y --> ident ) )
       o ( ( R < Y --> ident ) | ( R >= Y --> Q,R := Q+R/Y, R mod Y ) )
   
      = ( R >= Y --> Q,R := Q+1,R-Y ) o ( R < Y --> ident ) 
      | ( R >= Y --> Q,R := Q+1,R-Y ) o ( R >= Y and Y > 0 --> Q,R := Q+R/Y, R mod Y ) 
      | ( R < Y --> ident ) o ( R < Y --> ident ) 
      | ( R < Y --> ident ) o ( R >= Y and Y > 0 --> Q,R := Q+R/Y, R mod Y )
   

   After symbolic execution (click each clause to see its trace table):

       ( R >= Y and R < 2Y --> Q,R := Q+1, R-Y )
   
       | ( R >= 2Y and Y > 0 --> Q,R := Q+R/Y, R mod Y )
   
       | ( R < Y --> identity )
   
       | ( false --> Q,R := Q+R/Y, R mod Y )