"""{ 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 2.OK ans == mult(0) algebra 1 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 2.OK n - 1 >= 0 algebra 1 }""" #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 = sub * n #PREMISES FOR ATTACHED PROOF, IF ANY: # (ans == (sub * n)) # (sub == mult((n - 1))) """{ 1.OK ans == sub * n premise 2.OK sub == mult(n-1) premise 3.OK ans == mult(n-1) * n subst 2 1 4.OK mult(n) == mult(n-1) * n def 5.OK ans == mult(n) subst 4 3 }""" #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: