"""{ defOK mult(0) == 1
     defOK mult(n) == mult(n-1) * n  }"""
#PREMISES FOR NEXT LINE: 

def fac(n) :
    """{ pre  n >= 0
         post  ans == mult(n)
         return ans  }"""
    #PREMISES FOR NEXT LINE: 
    # (n >= 0)
    if n == 0 :
        #PREMISES FOR THEN-ARM: 
        # (n == 0)
        # (n >= 0)
        ans = 1
        #PREMISES FOR ATTACHED PROOF, IF ANY: 
        # (ans == 1)
        # (n == 0)
        # (n >= 0)
        """{ 1.OK mult(0) == 1    def
             6.OK ans == 1        premise
             2.OK ans == mult(0)  algebra 1 6
             3.OK n == 0          premise
             4.OK ans == mult(n)  subst 3 2}"""
        #PREMISES FOR NEXT LINE: 
        # (ans == mult(n))
    else :
        #PREMISES FOR ELSE-ARM: 
        # not (n == 0)
        # (n >= 0)
        """{ 1.OK not(n == 0)   premise
             3.OK n >= 0        premise
             2.OK n - 1 >= 0    algebra 1 3
        }"""
        #PREMISES FOR NEXT LINE: 
        # ((n - 1) >= 0)
        sub = fac(n-1)
        #PREMISES FOR ATTACHED PROOF, IF ANY: 
        # (sub == mult((n - 1)))
        # ((n - 1) >= 0)
        """{ 1.OK  sub == mult(n-1)    premise }"""
        #PREMISES FOR NEXT LINE: 
        # (sub == mult((n - 1)))
        ans = n * sub
        #PREMISES FOR ATTACHED PROOF, IF ANY: 
        # (ans == (n * sub))
        # (sub == mult((n - 1)))
        """{ 1.OK  ans == n * sub             premise
             2.OK  sub == mult(n-1)           premise
             3.OK  ans == n * mult(n-1)       subst 2 1
             6.OK  ans == mult(n-1) * n       algebra 3
             4.OK  mult(n) == mult(n-1) * n   def
             5.OK  ans == mult(n)             subst 4 6
        }"""
        #PREMISES FOR NEXT LINE: 
        # (ans == mult(n))
    #PREMISES FOR NEXT LINE: 
    # (ans == mult(n))
    # (n >= 0)
    """{ 1.OK  ans == mult(n)                 premise  }"""
    #PREMISES FOR NEXT LINE: 
    # (ans == mult(n))
    return ans
    #PREMISES FOR NEXT LINE: 
    # (ans == mult(n))
#PREMISES FOR NEXT LINE: