def double(a):
    """returns a list  b  that holds all of  a's  values * 2 (see post)"""
    """{ pre  True
         post forall 0 <= i < len(a), b[i] == a[i] * 2
         return b
    }"""
    b = []
    #PREMISES FOR ATTACHED PROOF, IF ANY: 
    # (b == [])
    # True
    #PREMISES FOR NEXT LINE: 
    # (b == [])
    x = 0
    #PREMISES FOR ATTACHED PROOF, IF ANY: 
    # (x == 0)
    # (b == [])
    """{ 1.OK forall 0 <= i < x, b[i] == a[i] * 2    foralli
         2.OK x == len(b)                 algebra
    }"""
    #PREMISES FOR NEXT LINE: 
    # (x == len(b))
    while x != len(a) :
        """{ invariant  (forall 0 <= i < x, b[i] == a[i] * 2) and (x == len(b))
             modifies x, b
        }"""
        #PREMISES FOR LOOP BODY: 
        # (x != len(a))
        # (forall(0, x, lambda i: (b[i] == (a[i] * 2))) and (x == len(b)))
        b.append(a[x]*2)
        #PREMISES FOR ATTACHED PROOF, IF ANY: 
        # (b[(len(b) - 1)] == (a[x] * 2))
        # (len(b) == (len(b_old) + 1))
        # (x != len(a))
        # (forall(0, x, lambda i: (b[i] == (a[i] * 2))) and (x == len(b_old)))
        """{ 1.OK (forall 0 <= i < x, b[i] == a[i] * 2) and (x == len(b_old))  premise
             2.OK x == len(b_old)                         ande 1
             10.OK forall 0 <= i < x, b[i] == a[i] * 2    ande 1
             3.OK len(b) == len(b_old) + 1                 premise
             4.OK x == len(b)-1                                 algebra 2 3
             5.OK b[len(b)-1] == a[x]*2                    premise
             6.OK b[x] == a[x]*2                          subst 4 5
             7.OK forall 0 <= i < x+1, b[i] == a[i] * 2  foralli 10 6
             8.OK len(b) == x + 1                         algebra 4
             9.OK return 7 8
        }"""
        #PREMISES FOR NEXT LINE: 
        # forall(0, (x + 1), lambda i: (b[i] == (a[i] * 2)))
        # (len(b) == (x + 1))
        x = x + 1
        #PREMISES FOR ATTACHED PROOF, IF ANY: 
        # (x == (x_old + 1))
        # forall(0, (x_old + 1), lambda i: (b[i] == (a[i] * 2)))
        # (len(b) == (x_old + 1))
        """{ 1.OK  forall 0 <= i < x_old +1, b[i] == a[i] * 2  premise
             2.OK  x == x_old +1                              premise
             3.OK forall 0 <= i < x, b[i] == a[i] * 2    subst 2 1
             4.OK len(b) == x_old + 1                       premise
             5.OK len(b) == x                             subst 2 4
             6.OK x == len(b)                             algebra 5
             #7.OK (forall 0 <= i < x, b[i] == a[i] * 2) and (x == len(b)) andi 3 6
             8. return 3 6
        }"""
        #PREMISES FOR NEXT LINE: 
        # forall(0, x, lambda i: (b[i] == (a[i] * 2)))
        # (x == len(b))
    #PREMISES FOR NEXT LINE: 
    # (forall(0, x, lambda i: (b[i] == (a[i] * 2))) and (x == len(b)))
    # not (x != len(a))

    """{ 1.OK (forall 0 <= i < x, b[i] == a[i] * 2) and (x == len(b))  premise
         3.OK not(x != len(a))                        premise
         4.OK x == len(a)                            algebra
         6.OK forall 0 <= i < x, b[i] == a[i] * 2    ande 1
         5.OK forall 0 <= i < len(a), b[i] == a[i] * 2   subst 4 6
    }"""
    #PREMISES FOR NEXT LINE: 
    # forall(0, len(a), lambda i: (b[i] == (a[i] * 2)))
    return b
    #PREMISES FOR NEXT LINE: 
    # forall(0, len(a), lambda i: (b[i] == (a[i] * 2)))
#PREMISES FOR NEXT LINE: