# week03B osize monoticity proof

Lemma: `osize' P x = 2^x osize' P 0`

Proof: break circular argument with lower bound M.

TODO: ask forum how to prove without M

Now, prove monoticity, that is `osize s < osize t --> osize u[s] < osize u[t]`

Clearly, for an empty context u0, u0[x] = x and thus we have:

    osize s < osize t --> osize u0[s] < osize u0[t]
    
Now assume for some contexts u1 and u2

    osize s < osize t --> osize u1[s] < osize u1[t]
    osize s < osize t --> osize u2[s] < osize u2[t]
    
Prove for each case:

    u = not (u1[s])
    
       osize u[s]
       = osize' u[s] 0              unfold osize
       = osize' (not u1[s]) 0       unfold u
       = osize' u1[s] 1
       = 2^1 * osize' u1[s] 0
       = 2 osize u1[s]
       
       Similarly, osize u[t] = 2 osize u1[t], and thus,
           osize s < osize t --> osize u[s] < osize u[t] holds.
   
    u[s] = u1[s] AND u2[s]
    
        osize u[s]
        = osize' u[s] 0
        = osize' (u1[s] AND u2[s]) 0
        = 2^0 + osize' u1[s] 1 + osize' u2[s] 1
        = 1 + 2^1 * osize u1[s] + 2^1 * osize' u2[s] 0
        = 1 + 2 osize u1[s] + 2 osize u2[s]
        
        similarly, osize u[t] = 1 + 2 osize u1[t] + 2 osize u2[t]
        
        Sub: 
        
            1 + 2 osize u1[s] + 2 osize u2[s] < 1 + 2 osize u1[t] + 2 osize u2[t]
            osize u1[s] + osize u2[s] < osize u1[t] + osize u2[t]

        thus osize s < osize t --> osize u[s] < osize u[t] holds.


    u = u1[s] OR u2[t]
    
        similar to case above
        
    u = u1[s] IMPLIES u2[t]
    
        similar to case above

TODO: prove that every expression can be build through a chain of the above cases.