fact: Definition McCarthy_post n r := If n > 100 then r = n - 10 else r = 91.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat