-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.Ackermann
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proving the relationship between Ackermann's original 3-argument function (1928)
-- and the Ackermann-Péter function (1935).
--
-- Ackermann's original function was a 3-argument function designed to demonstrate
-- a total computable function that is not primitive recursive. The third argument
-- generalizes the operation: @ack 0 n a = n + a@ (addition), and higher levels
-- correspond to multiplication, exponentiation, etc.
--
-- Rózsa Péter simplified this to a 2-argument function in 1935, which is what
-- most people today call "the Ackermann function."
--
-- This example is inspired by: <https://github.com/imandra-ai/imandrax-examples/blob/main/src/ackermann.iml>
--
-- Note: This proof was developed by Claude (Anthropic's AI assistant) with
-- minimal user prompting and guidance.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP               #-}
{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications  #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.Ackermann where

import Data.SBV
import Data.SBV.Tuple
import Data.SBV.TP

#ifdef DOCTEST
-- $setup
-- >>> import Data.SBV
-- >>> import Data.SBV.TP
#endif

-- * Ackermann's original 3-argument function (1928)

-- | Ackermann's original 3-argument function (1928). This is the lesser-known
-- original version, not the commonly referenced Ackermann-Péter function.
-- The third argument @a@ generalizes the operation at each level.
ack :: SInteger -> SInteger -> SInteger -> SInteger
ack :: SInteger -> SInteger -> SInteger -> SInteger
ack = String
-> (SInteger -> SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
-> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"ack" ((SInteger -> SInteger -> SInteger -> SInteger)
 -> SInteger -> SInteger -> SInteger -> SInteger)
-> (SInteger -> SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
-> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
m SInteger
n SInteger
a ->
    SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
a)
  (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) SInteger
0
  (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1) SInteger
a
  (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger -> SInteger -> SInteger -> SInteger
ack SInteger
m (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SInteger
a) SInteger
a

-- * Ackermann-Péter function (1935)

-- | The Ackermann-Péter function (1935), commonly known as "the Ackermann function."
-- This is Rózsa Péter's simplified 2-argument version of Ackermann's original function.
pet :: SInteger -> SInteger -> SInteger
pet :: SInteger -> SInteger -> SInteger
pet = String
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"pet" ((SInteger -> SInteger -> SInteger)
 -> SInteger -> SInteger -> SInteger)
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
m SInteger
n ->
    SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)
  (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) (SInteger -> SInteger -> SInteger
pet (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SInteger
1)
  (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SInteger -> SInteger -> SInteger
pet (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)   (SInteger -> SInteger -> SInteger
pet SInteger
m (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1))

-- * Correctness

-- | Prove that @ack m 2 2 = 4@ for all m >= 0.
--
-- >>> runTP ack_2_2_4
-- Inductive lemma (strong): ack_2_2_4
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2                         Q.E.D.
--     Step: 1.2.3                         Q.E.D.
--     Step: 1.2.4                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] ack_2_2_4 :: Ɐm ∷ Integer → Bool
ack_2_2_4 :: TP (Proof (Forall "m" Integer -> SBool))
ack_2_2_4 :: TP (Proof (Forall "m" Integer -> SBool))
ack_2_2_4 = String
-> (Forall "m" Integer -> SBool)
-> (MeasureArgs (Forall "m" Integer -> SBool) Integer, [ProofObj])
-> (Proof (Forall "m" Integer -> SBool)
    -> StepArgs (Forall "m" Integer -> SBool) Integer)
-> TP (Proof (Forall "m" Integer -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "m" Integer -> SBool), Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "m" Integer -> SBool)
-> (MeasureArgs (Forall "m" Integer -> SBool) m, [ProofObj])
-> (Proof (Forall "m" Integer -> SBool)
    -> StepArgs (Forall "m" Integer -> SBool) t)
-> TP (Proof (Forall "m" Integer -> SBool))
sInduct String
"ack_2_2_4"
                    (\(Forall SInteger
m) -> SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger -> SInteger
ack SInteger
m SInteger
2 SInteger
2 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
4)
                    (MeasureArgs (Forall "m" Integer -> SBool) Integer
SInteger -> SInteger
forall a. a -> a
id, []) ((Proof (Forall "m" Integer -> SBool)
  -> StepArgs (Forall "m" Integer -> SBool) Integer)
 -> TP (Proof (Forall "m" Integer -> SBool)))
-> (Proof (Forall "m" Integer -> SBool)
    -> StepArgs (Forall "m" Integer -> SBool) Integer)
-> TP (Proof (Forall "m" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                    \Proof (Forall "m" Integer -> SBool)
ih SInteger
m -> [SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0]
                          [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger -> SInteger -> SInteger
ack SInteger
m SInteger
2 SInteger
2
                          SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SInteger)] -> TPProofRaw SInteger
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
m SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SInteger
forall a. Trivial a => a
trivial
                                   , SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0  SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger -> SInteger
ack SInteger
m SInteger
2 SInteger
2
                                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger -> SInteger -> SInteger -> SInteger
ack SInteger
m SInteger
1 SInteger
2) SInteger
2
                                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SInteger
2 SInteger
2
                                              SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Integer -> SBool)
ih Proof (Forall "m" Integer -> SBool)
-> IArgs (Forall "m" Integer -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)
                                              TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
4 :: SInteger)
                                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
TPProofRaw SInteger
forall a. TPProofRaw a
qed
                                   ]

-- | Prove that @ack@ is non-negative when all arguments are non-negative.
-- We use strong induction on the lexicographic measure (m, n).
--
-- >>> runTP ack_psd
-- Inductive lemma (strong): ack_psd
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (4 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2                           Q.E.D.
--     Step: 1.3                           Q.E.D.
--     Step: 1.4.1                         Q.E.D.
--     Step: 1.4.2                         Q.E.D.
--     Step: 1.4.3                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] ack_psd :: Ɐm ∷ Integer → Ɐn ∷ Integer → Ɐa ∷ Integer → Bool
ack_psd :: TP (Proof (Forall "m" Integer -> Forall "n" Integer -> Forall "a" Integer -> SBool))
ack_psd :: TP
  (Proof
     (Forall "m" Integer
      -> Forall "n" Integer -> Forall "a" Integer -> SBool))
ack_psd = String
-> (Forall "m" Integer
    -> Forall "n" Integer -> Forall "a" Integer -> SBool)
-> (MeasureArgs
      (Forall "m" Integer
       -> Forall "n" Integer -> Forall "a" Integer -> SBool)
      (Integer, Integer),
    [ProofObj])
-> (Proof
      (Forall "m" Integer
       -> Forall "n" Integer -> Forall "a" Integer -> SBool)
    -> StepArgs
         (Forall "m" Integer
          -> Forall "n" Integer -> Forall "a" Integer -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "m" Integer
         -> Forall "n" Integer -> Forall "a" Integer -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition
   (Forall "m" Integer
    -> Forall "n" Integer -> Forall "a" Integer -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "m" Integer
    -> Forall "n" Integer -> Forall "a" Integer -> SBool)
-> (MeasureArgs
      (Forall "m" Integer
       -> Forall "n" Integer -> Forall "a" Integer -> SBool)
      m,
    [ProofObj])
-> (Proof
      (Forall "m" Integer
       -> Forall "n" Integer -> Forall "a" Integer -> SBool)
    -> StepArgs
         (Forall "m" Integer
          -> Forall "n" Integer -> Forall "a" Integer -> SBool)
         t)
-> TP
     (Proof
        (Forall "m" Integer
         -> Forall "n" Integer -> Forall "a" Integer -> SBool))
sInduct String
"ack_psd"
                  (\(Forall SInteger
m) (Forall SInteger
n) (Forall SInteger
a) ->
                      SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger -> SInteger
ack SInteger
m SInteger
n SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0)
                  (\SInteger
m SInteger
n SInteger
_a -> (SInteger, SInteger) -> SBV (Integer, Integer)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SInteger
m, SInteger
n), []) ((Proof
    (Forall "m" Integer
     -> Forall "n" Integer -> Forall "a" Integer -> SBool)
  -> StepArgs
       (Forall "m" Integer
        -> Forall "n" Integer -> Forall "a" Integer -> SBool)
       Bool)
 -> TP
      (Proof
         (Forall "m" Integer
          -> Forall "n" Integer -> Forall "a" Integer -> SBool)))
-> (Proof
      (Forall "m" Integer
       -> Forall "n" Integer -> Forall "a" Integer -> SBool)
    -> StepArgs
         (Forall "m" Integer
          -> Forall "n" Integer -> Forall "a" Integer -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "m" Integer
         -> Forall "n" Integer -> Forall "a" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                  \Proof
  (Forall "m" Integer
   -> Forall "n" Integer -> Forall "a" Integer -> SBool)
ih SInteger
m SInteger
n SInteger
a -> [SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0, SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0, SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0]
                            [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger -> SInteger -> SInteger
ack SInteger
m SInteger
n SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0 SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial   -- n + a >= 0
                                     , SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0 SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial   -- 0 >= 0
                                     , SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1 SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial   -- a >= 0
                                     , SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.&& SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
1
                                         SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger -> SInteger
ack SInteger
m SInteger
n SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger -> SInteger -> SInteger -> SInteger
ack SInteger
m (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SInteger
a) SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                                          SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "m" Integer
   -> Forall "n" Integer -> Forall "a" Integer -> SBool)
ih Proof
  (Forall "m" Integer
   -> Forall "n" Integer -> Forall "a" Integer -> SBool)
-> IArgs
     (Forall "m" Integer
      -> Forall "n" Integer -> Forall "a" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SInteger
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SInteger
a)
                                          TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "m" Integer
   -> Forall "n" Integer -> Forall "a" Integer -> SBool)
ih Proof
  (Forall "m" Integer
   -> Forall "n" Integer -> Forall "a" Integer -> SBool)
-> IArgs
     (Forall "m" Integer
      -> Forall "n" Integer -> Forall "a" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger -> SInteger -> SInteger -> SInteger
ack SInteger
m (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SInteger
a), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SInteger
a)
                                          Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                     ]

-- | Prove that @pet@ is non-negative when both arguments are non-negative.
-- We use strong induction on the lexicographic measure (m, n).
--
-- >>> runTPWith cvc5 pet_psd
-- Inductive lemma (strong): pet_psd
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (3 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2                         Q.E.D.
--     Step: 1.2.3                         Q.E.D.
--     Step: 1.3.1                         Q.E.D.
--     Step: 1.3.2                         Q.E.D.
--     Step: 1.3.3                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] pet_psd :: Ɐm ∷ Integer → Ɐn ∷ Integer → Bool
pet_psd :: TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool))
pet_psd :: TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool))
pet_psd = do
    String
-> (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> (MeasureArgs
      (Forall "m" Integer -> Forall "n" Integer -> SBool)
      (Integer, Integer),
    [ProofObj])
-> (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
    -> StepArgs
         (Forall "m" Integer -> Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "m" Integer -> Forall "n" Integer -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> (MeasureArgs
      (Forall "m" Integer -> Forall "n" Integer -> SBool) m,
    [ProofObj])
-> (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
    -> StepArgs (Forall "m" Integer -> Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool))
sInduct String
"pet_psd"
                  (\(Forall SInteger
m) (Forall SInteger
n) -> SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
pet SInteger
m SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0)
                  (\SInteger
m SInteger
n -> (SInteger, SInteger) -> SBV (Integer, Integer)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SInteger
m, SInteger
n), []) ((Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
  -> StepArgs
       (Forall "m" Integer -> Forall "n" Integer -> SBool) Bool)
 -> TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)))
-> (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
    -> StepArgs
         (Forall "m" Integer -> Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                  \Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
ih SInteger
m SInteger
n -> [SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0, SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0]
                          [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger -> SInteger
pet SInteger
m SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0 SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial   -- n + 1 >= 0
                                   , SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.&& SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0
                                       SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
pet SInteger
m SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                                        SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
pet (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                                        SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
ih Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger
1 :: SInteger))
                                        TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                        SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                   , SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.&& SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0
                                       SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
pet SInteger
m SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                                        SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
pet (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger -> SInteger -> SInteger
pet SInteger
m (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                                        SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
ih Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SInteger
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1))
                                        TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
ih Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger -> SInteger -> SInteger
pet SInteger
m (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)))
                                        Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                        SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                   ]

-- | The main theorem, relating @pet@ and @ack@: @pet m n + 3 = ack (m-1) (n+3) 2@ for @m > 0@ and @n >= 0@.
--
-- >>> runTPWith cvc5 petAck
-- Inductive lemma (strong): ack_2_2_4
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2                         Q.E.D.
--     Step: 1.2.3                         Q.E.D.
--     Step: 1.2.4                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma (strong): pet_psd
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (3 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2                         Q.E.D.
--     Step: 1.2.3                         Q.E.D.
--     Step: 1.3.1                         Q.E.D.
--     Step: 1.3.2                         Q.E.D.
--     Step: 1.3.3                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma (strong): petAck
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (4 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2                         Q.E.D.
--     Step: 1.2.3                         Q.E.D.
--     Step: 1.3.1                         Q.E.D.
--     Step: 1.3.2                         Q.E.D.
--     Step: 1.3.3                         Q.E.D.
--     Step: 1.3.4                         Q.E.D.
--     Step: 1.3.5                         Q.E.D.
--     Step: 1.4.1                         Q.E.D.
--     Step: 1.4.2                         Q.E.D.
--     Step: 1.4.3                         Q.E.D.
--     Step: 1.4.4                         Q.E.D.
--     Step: 1.4.5                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] petAck :: Ɐm ∷ Integer → Ɐn ∷ Integer → Bool
petAck :: TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool))
petAck :: TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool))
petAck = do
    Proof (Forall "m" Integer -> SBool)
ack224 <- TP (Proof (Forall "m" Integer -> SBool))
ack_2_2_4
    Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
psd    <- TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool))
pet_psd
    String
-> (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> (MeasureArgs
      (Forall "m" Integer -> Forall "n" Integer -> SBool)
      (Integer, Integer),
    [ProofObj])
-> (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
    -> StepArgs
         (Forall "m" Integer -> Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "m" Integer -> Forall "n" Integer -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> (MeasureArgs
      (Forall "m" Integer -> Forall "n" Integer -> SBool) m,
    [ProofObj])
-> (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
    -> StepArgs (Forall "m" Integer -> Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool))
sInduct String
"petAck"
               (\(Forall SInteger
m) (Forall SInteger
n) ->
                   SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.&& SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
pet SInteger
m SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3) SInteger
2)
               (\SInteger
m SInteger
n -> (SInteger, SInteger) -> SBV (Integer, Integer)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SInteger
m, SInteger
n), []) ((Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
  -> StepArgs
       (Forall "m" Integer -> Forall "n" Integer -> SBool) Bool)
 -> TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)))
-> (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
    -> StepArgs
         (Forall "m" Integer -> Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
               \Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
ih SInteger
m SInteger
n -> [SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0, SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0]
                       [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger -> SInteger
pet SInteger
m SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3) SInteger
2
                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
m SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1 SBool -> SBool -> SBool
.&& SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0
                                    SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                                , SInteger
m SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1 SBool -> SBool -> SBool
.&& SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0
                                    SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
pet SInteger
1 SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger -> SInteger
ack SInteger
0 (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3) SInteger
2
                                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
pet SInteger
0 (SInteger -> SInteger -> SInteger
pet SInteger
1 (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2
                                     SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
ih Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" (SInteger
1 :: SInteger), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1))
                                     TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                , SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
1 SBool -> SBool -> SBool
.&& SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0
                                    -- n <= 0 with n >= 0 means n == 0
                                    SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
pet SInteger
m SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3) SInteger
2
                                     -- First unfold pet: since n <= 0, pet m n = pet (m-1) 1
                                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
pet (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3) SInteger
2
                                     -- Unfold ack: ack (m-1) (n+3) 2 = ack (m-2) (ack (m-1) (n+2) 2) 2
                                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
pet (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
2) (SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2) SInteger
2) SInteger
2
                                     -- Apply IH at (m-1, 1): pet (m-1) 1 + 3 = ack (m-2) 4 2
                                     SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
ih Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger
1 :: SInteger))
                                     TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
2) SInteger
4 SInteger
2 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
2) (SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2) SInteger
2) SInteger
2
                                     -- Since n = 0, n+2 = 2, and ack (m-1) 2 2 = 4 by ack_2_2_4
                                     SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Integer -> SBool)
ack224 Proof (Forall "m" Integer -> SBool)
-> IArgs (Forall "m" Integer -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)
                                     TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                , SInteger
m SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
1 SBool -> SBool -> SBool
.&& SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0
                                    SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
pet SInteger
m SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3) SInteger
2
                                     -- Unfold pet: pet m n = pet (m-1) (pet m (n-1))
                                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
pet (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger -> SInteger -> SInteger
pet SInteger
m (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3) SInteger
2
                                     -- Unfold ack on RHS: ack (m-1) (n+3) 2 = ack (m-2) (ack (m-1) (n+2) 2) 2
                                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger
pet (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger -> SInteger -> SInteger
pet SInteger
m (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
2) (SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2) SInteger
2) SInteger
2
                                     -- Use pet_psd to establish pet m (n-1) >= 0
                                     SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
psd Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SInteger
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1))
                                     -- Apply IH at (m-1, pet m (n-1)) to transform LHS
                                     TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
ih Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger -> SInteger -> SInteger
pet SInteger
m (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)))
                                     Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
2) (SInteger -> SInteger -> SInteger
pet SInteger
m (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
3) SInteger
2 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
2) (SInteger -> SInteger -> SInteger -> SInteger
ack (SInteger
m SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2) SInteger
2) SInteger
2
                                     -- Apply IH at (m, n-1): pet m (n-1) + 3 = ack (m-1) (n+2) 2
                                     SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
ih Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> IArgs (Forall "m" Integer -> Forall "n" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SInteger
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1))
                                     TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                ]

{- HLint ignore module    "Use curry"     -}
{- HLint ignore ack_psd   "Use camelCase" -}
{- HLint ignore pet_psd   "Use camelCase" -}
{- HLint ignore ack_2_2_4 "Use camelCase" -}