MODULE 'Fac' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `fac`:
fac'nonfail :: Int -> Bool
fac'nonfail v1 = (v1 == 0) || (v1 > 0)

MODULE 'UseFac' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `fac1`:
fac1'nonfail :: Int -> Int -> Bool
fac1'nonfail v1 v2 = ((v2 + 5) == 0) || ((v2 + 5) > 0)

MODULE 'FacMore' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `fac`:
fac'nonfail :: Int -> Bool
fac'nonfail v1 = (v1 == 0) || (v1 > 0)

-- Non-fail condition of operation `fac5`:
fac5'nonfail :: Int -> Int -> Bool
fac5'nonfail v1 v2 = ((v2 + 5) == 0) || ((v2 + 5) > 0)

-- Non-fail condition of operation `facNeg`:
facNeg'nonfail :: Int -> Bool
facNeg'nonfail v1 = (v1 > 0) || ((not (v1 > 0)) && (v1 > 3))

-- Non-fail condition of operation `gt3`:
gt3'nonfail :: Int -> Bool
gt3'nonfail v1 = v1 > 3

MODULE 'FacIO' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `fac`:
fac'nonfail :: Int -> Bool
fac'nonfail v1 = (v1 == 0) || (v1 > 0)

MODULE 'UseDiv' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:
divZero: <FAILING>

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `div1`:
div1'nonfail :: Int -> Int -> Bool
div1'nonfail v1 v2 = not (v2 == 0)

MODULE 'Diamond' VERIFIED

MODULE 'Sig' VERIFIED

MODULE 'ListLength' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `f`:
f'nonfail :: [a] -> Bool
f'nonfail v1 = (len v1) < 10

MODULE 'Nth' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `nth`:
nth'nonfail :: [a] -> Int -> Bool
nth'nonfail v1 v2 = (v2 >= 0) && ((len (tak (v2 + 1) v1)) == (v2 + 1))

MODULE 'NthInfer' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `nth`:
nth'nonfail :: [a] -> Int -> Bool
nth'nonfail v1 v2 = ((not (null v1)) && (case v1 of
    v3 : v4 -> (v2 == 0) || (not (v2 > 0))
    _ -> True)) && ((not (null v1)) && (case v1 of
    v3 : v4 -> (v2 == 0) || (v2 > 0)
    _ -> True))

MODULE 'NthZero' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `nth`:
nth'nonfail :: [a] -> Int -> Bool
nth'nonfail v1 v2 = (not (null v1)) && (case v1 of
    v3 : v4 -> v2 == 0
    _ -> True)

MODULE 'NthZeroNonFail' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `nth`:
nth'nonfail :: [a] -> Int -> Bool
nth'nonfail v1 v2 = (not (null v1)) && (v2 == 0)

MODULE 'NthZeroNonFailWrong' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:
nth: <FAILING>

MODULE 'One' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `one`:
one'nonfail :: Int -> Bool
one'nonfail v1 = v1 == 0

MODULE 'HeadPos' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `headpos`:
headpos'nonfail :: [Int] -> Bool
headpos'nonfail v1 = (not (null v1)) && (case v1 of
    v2 : v3 -> v2 > 0
    _ -> True)

MODULE 'CharBounds' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `succChar`:
succChar'nonfail :: Char -> Bool
succChar'nonfail v1 = v1 < maxBound

MODULE 'Tuple' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `fPair`:
fPair'nonfail :: Pair Int Int -> Bool
fPair'nonfail v1 = case v1 of
    MkPair v2 v3 -> (v2 + v3) > 0

-- Non-fail condition of operation `fTriple`:
fTriple'nonfail :: (Int,Int,Int) -> Bool
fTriple'nonfail v1 = case v1 of
    (v2,v3,v4) -> ((v2 + v3) + v4) > 0

-- Non-fail condition of operation `usePair`:
usePair'nonfail :: Int -> Bool
usePair'nonfail v1 = v1 > 0

-- Non-fail condition of operation `useTriple`:
useTriple'nonfail :: Int -> Bool
useTriple'nonfail v1 = v1 > 0

MODULE 'CaseCond' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `pos`:
pos'nonfail :: Int -> Bool
pos'nonfail v1 = v1 > 0

-- Non-fail condition of operation `sumPos`:
sumPos'nonfail :: (Int,Int) -> Bool
sumPos'nonfail v1 = (case v1 of
    (v2,v3) -> False) || (case v1 of
    (v2,v3) -> v3 > 0)

MODULE 'UseFloatDiv' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:
divZero: <FAILING>

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `div1`:
div1'nonfail :: Float -> Float -> Bool
div1'nonfail v1 v2 = not (v2 == 0.0)

MODULE 'UseSqrt' VERIFIED W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:
failedSqrt: <FAILING>

NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:

-- Non-fail condition of operation `sqrtP2`:
sqrtP2'nonfail :: Float -> Bool
sqrtP2'nonfail v1 = (v1 + 2.0) >= 0.0