{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE ExplicitNamespaces #-}

{-# LANGUAGE UndecidableInstances #-}


-- |
-- Module      : OAlg.Entity.Natural
-- Description : natrual numbers promoted to type-level
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- natural numbers promotable to type-level. They serve to parameterize the length of finite lists on
-- type-level (see "OAlg.Entity.FinList").
--
-- __Note__ We need the language extension @UndecidableInstances@ for type checking the definition
--
-- > N0 * m = N0
-- > S n * m = m + n * m
--
-- for the type family t'*'.
--
-- Using @UndecidableInstances@ could cause the type checker to not terminate, but this will
-- obviously not happen for the given definition (we also use the same definition for the
-- multiplicative structure of 'N'').
module OAlg.Entity.Natural
  (
    -- * Natrual Numbers
     N'(..), toN', type (+), type (*)

    -- * Ordering
  , (:<=:)(..), nodAnyFst, nodAnySnd, nodRefl, nodPred

    -- * Attest
  , Attestable(..), Ats(..), ats, atsSucc, nValue, W(..), cmpW, (++), (**), W'(..), toW'
  , SomeNatural(..), succSomeNatural, someNatural, naturals

    -- * Induction
  , induction


    -- * Propositions
    -- | The following propositions are based - for the most part - on induction.
    --   To ensure that the /proofs/ yield a terminal value, i.e. 'Refl', we
    --   used in the /proof/ of the induction hypothesis only propositions which
    --   are proofed before. So: if these propositions terminate, then also
    --   the hypothesis will terminate.
  , Any, Some

    -- | __Some basic Lemmas__
  , refl, lemma1, sbstAdd

    -- | __Some abbreviations__
  , prpAdd0, prpAdd1, prpAdd2

    -- | __Equivalence of Any__  
  , prpEqlAny, prpEqlAny'

    -- | __Injectivity of the Successor__
  , prpSuccInjective

    -- ** Addition
    -- | __Neutral Element__
    -- 
    -- t'N0' is the neutral element of t'+'.
  , prpAddNtrlL, prpAddNtrlR

    -- | __Associativity__
  , prpAddAssoc

    -- | __Commutativity__
  , lemmaAdd1, prpAddComm

    -- ** Multiplication
    -- | __Neutral Element__
    --
    -- @'N1' = 'S' t'N0'@ is the neutral element of t'*'.
  , prpMltNtrlL, prpMltNtrlR

    -- | __Distributivity on the left__
  , prpDstrL

    -- | __Associativity__
  , prpMltAssoc

    -- | __Distributivity on the right__
  , lemmaMlt1, lemmaAdd2, prpDstrR

    -- | __Commutativity__
  , prpMltComm

    -- * Some attests
    -- | generating the Haskell code and interface for witnesses.
  , codeW, itfW

  , type N0, type N1, type N2, type N3, type N4, type N5
  , type N6, type N7, type N8, type N9, type N10

  -- * X
  , xSomeNatural

  )
  where

import Control.Monad (join,return, (>>=))
import Control.Exception

import Data.Typeable
import Data.Type.Equality
import qualified Data.List as L

import OAlg.Prelude

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Fibred
import OAlg.Structure.FibredOriented
import OAlg.Structure.Additive hiding (prpAdd1,prpAdd2)
import OAlg.Structure.Distributive

--------------------------------------------------------------------------------
-- N' -

-- | natural number promotable to type-level.
data N' = N0 | S N' deriving (N' -> N' -> Bool
(N' -> N' -> Bool) -> (N' -> N' -> Bool) -> Eq N'
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: N' -> N' -> Bool
== :: N' -> N' -> Bool
$c/= :: N' -> N' -> Bool
/= :: N' -> N' -> Bool
Eq,Eq N'
Eq N' =>
(N' -> N' -> Ordering)
-> (N' -> N' -> Bool)
-> (N' -> N' -> Bool)
-> (N' -> N' -> Bool)
-> (N' -> N' -> Bool)
-> (N' -> N' -> N')
-> (N' -> N' -> N')
-> Ord N'
N' -> N' -> Bool
N' -> N' -> Ordering
N' -> N' -> N'
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: N' -> N' -> Ordering
compare :: N' -> N' -> Ordering
$c< :: N' -> N' -> Bool
< :: N' -> N' -> Bool
$c<= :: N' -> N' -> Bool
<= :: N' -> N' -> Bool
$c> :: N' -> N' -> Bool
> :: N' -> N' -> Bool
$c>= :: N' -> N' -> Bool
>= :: N' -> N' -> Bool
$cmax :: N' -> N' -> N'
max :: N' -> N' -> N'
$cmin :: N' -> N' -> N'
min :: N' -> N' -> N'
Ord,Int -> N' -> ShowS
[N'] -> ShowS
N' -> String
(Int -> N' -> ShowS)
-> (N' -> String) -> ([N'] -> ShowS) -> Show N'
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> N' -> ShowS
showsPrec :: Int -> N' -> ShowS
$cshow :: N' -> String
show :: N' -> String
$cshowList :: [N'] -> ShowS
showList :: [N'] -> ShowS
Show)

instance LengthN N' where
  lengthN :: N' -> N
lengthN N'
N0 = N
0
  lengthN (S N'
i) = N
1 N -> N -> N
forall a. Additive a => a -> a -> a
+ N' -> N
forall x. LengthN x => x -> N
lengthN N'
i

--------------------------------------------------------------------------------
-- toN' -

-- | mapping a natural number in 'N' to 'N''.
toN' :: N -> N'
toN' :: N -> N'
toN' N
0 = N'
N0
toN' N
i = N' -> N'
S (N -> N'
toN' (N
iN -> N -> N
>-N
1))

----------------------------------------
-- (+) -

infixr 6 +
  
-- | addition of natural numbers.
type family (+) (n :: N') (m :: k) :: N'
type instance N0 + n = n
type instance S n + (m :: N') = S (n+m)
type instance n + 0 = n
type instance n + 1 = S n
type instance n + 2 = S (S n)
type instance n + 3 = S (S (S n))

----------------------------------------
-- (*) -
infixr 7 *

-- | multiplication of natural numbers.
type family (*) (n :: k) (m :: N') :: N'
type instance N0 * m  = N0
type instance S n * m = m + (n * m)
-- the reason for switching the variables is to define (**) easely, without any infering of equality.
type instance 0 * m = N0
type instance 1 * m = m
type instance 2 * m = m + m

----------------------------------------
-- N' - CmpN' -

-- | comparing two natural numbers.
type family CmpN' (n :: N') (m :: N') :: Ordering
type instance CmpN' N0 N0    = EQ
type instance CmpN' (S _) N0 = GT
type instance CmpN' N0 (S _) = LT
type instance CmpN' (S n) (S m) = CmpN' n m

----------------------------------------
-- N' - Enum -

instance Enum N' where
  succ :: N' -> N'
succ = N' -> N'
S
  
  pred :: N' -> N'
pred N'
N0    = AlgebraicException -> N'
forall a e. Exception e => e -> a
throw AlgebraicException
NoPredecor
  pred (S N'
i) = N'
i

  toEnum :: Int -> N'
toEnum Int
0 = N'
N0
  toEnum Int
i = N' -> N'
forall a. Enum a => a -> a
succ (N' -> N') -> N' -> N'
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Int -> N'
forall a. Enum a => Int -> a
toEnum (Int
iInt -> Int -> Int
forall a. Abelian a => a -> a -> a
-Int
1)

  fromEnum :: N' -> Int
fromEnum N'
N0 = Int
0
  fromEnum (S N'
i) = Int
1Int -> Int -> Int
forall a. Additive a => a -> a -> a
+N' -> Int
forall a. Enum a => a -> Int
fromEnum N'
i

----------------------------------------
-- N' - Entity -

instance Validable N' where
  valid :: N' -> Statement
valid N'
N0    = Statement
SValid
  valid (S N'
n) = N' -> Statement
forall a. Validable a => a -> Statement
valid N'
n

----------------------------------------
-- N' - Structure -

type instance Point N' = ()
instance ShowPoint N'
instance EqPoint N'
instance OrdPoint N'
instance SingletonPoint N'
instance ValidablePoint N'
instance TypeablePoint N'
instance XStandardPoint N'
instance Oriented N' where
  orientation :: N' -> Orientation (Point N')
orientation = Orientation () -> N' -> Orientation ()
forall b a. b -> a -> b
const (()() -> () -> Orientation ()
forall p. p -> p -> Orientation p
:>())

instance Multiplicative N' where
  one :: Point N' -> N'
one () = N' -> N'
S N'
N0
  N'
N0 * :: N' -> N' -> N'
* N'
_   = N'
N0
  S N'
n * N'
m  = N'
m N' -> N' -> N'
forall a. Additive a => a -> a -> a
+ N'
n N' -> N' -> N'
forall c. Multiplicative c => c -> c -> c
* N'
m -- (1+n)*m = n*m + m

type instance Root N' = Orientation ()
instance ShowRoot N'
instance EqRoot N'
instance ValidableRoot N'
instance SingletonRoot N'
instance TypeableRoot N'
instance Fibred N'
instance FibredOriented N'

instance Additive N' where
  zero :: Root N' -> N'
zero Root N'
_ = N'
N0
  N'
N0 + :: N' -> N' -> N'
+ N'
m  = N'
m
  S N'
n + N'
m = N' -> N'
S (N'
n N' -> N' -> N'
forall a. Additive a => a -> a -> a
+ N'
m)

instance Distributive N'
instance Commutative N'
-- instance Number N'

--------------------------------------------------------------------------------
-- W -

-- | witness for a natural number and serves for inductively definable elements (see 'induction'). 
data W n where
  W0 :: W N0
  SW :: W n -> W (n+1)
  
deriving instance Eq (W n)

-- | comparing of two witnesses.
cmpW :: W n -> W m -> Ordering
cmpW :: forall (n :: N') (m :: N'). W n -> W m -> Ordering
cmpW W n
W0 W m
W0         = Ordering
EQ
cmpW (SW W n
_) W m
W0     = Ordering
GT
cmpW W n
W0 (SW W n
_)     = Ordering
LT
cmpW (SW W n
n) (SW W n
m) = W n -> W n -> Ordering
forall (n :: N') (m :: N'). W n -> W m -> Ordering
cmpW W n
n W n
m

instance Show (W n) where
  show :: W n -> String
show W n
w = N -> String
forall a. Show a => a -> String
show (W n -> N
forall x. LengthN x => x -> N
lengthN W n
w)

instance Validable (W n) where
  valid :: W n -> Statement
valid W n
W0     = Statement
SValid
  valid (SW W n
w) = W n -> Statement
forall a. Validable a => a -> Statement
valid W n
w

instance LengthN (W n) where
  lengthN :: W n -> N
lengthN W n
W0     = N
0
  lengthN (SW W n
i) = N
1 N -> N -> N
forall a. Additive a => a -> a -> a
+ W n -> N
forall x. LengthN x => x -> N
lengthN W n
i
  
--------------------------------------------------------------------------------
-- (++)

infixr 6 ++

-- | addition of witnesses.
(++) :: W n -> W m -> W (n+m)
W n
W0 ++ :: forall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++ W m
m = W m
W (n + m)
m
(SW W n
n) ++ W m
m = W (n + m) -> W ((n + m) + 1)
forall (d :: N'). W d -> W (d + 1)
SW (W n
nW n -> W m -> W (n + m)
forall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++W m
m)

--------------------------------------------------------------------------------
-- (**) -
infixr 7 **

-- | multiplication of witnesses.
(**) :: W n -> W m -> W (n*m)
W n
W0 ** :: forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
** W m
_ = W (n * m)
W N0
W0
(SW W n
n) ** W m
m = W m
m W m -> W (n * m) -> W (m + (n * m))
forall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++ W n
nW n -> W m -> W (n * m)
forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**W m
m

--------------------------------------------------------------------------------
-- induction-

-- | predicate for any natural number.
type Any = W

-- | induction for general type functions.
induction :: Any n -> f N0 -> (forall i . f i -> f (i+1)) -> f n
induction :: forall (n :: N') (f :: N' -> Type).
Any n -> f N0 -> (forall (i :: N'). f i -> f (i + 1)) -> f n
induction W n
W0 f N0
f0 forall (i :: N'). f i -> f (i + 1)
_    = f n
f N0
f0
induction (SW W n
i) f N0
f0 forall (i :: N'). f i -> f (i + 1)
h = f n -> f (n + 1)
forall (i :: N'). f i -> f (i + 1)
h (W n -> f N0 -> (forall (i :: N'). f i -> f (i + 1)) -> f n
forall (n :: N') (f :: N' -> Type).
Any n -> f N0 -> (forall (i :: N'). f i -> f (i + 1)) -> f n
induction W n
i f N0
f0 f i -> f (i + 1)
forall (i :: N'). f i -> f (i + 1)
h)

--------------------------------------------------------------------------------
-- Attestable -

-- | attest for any natural number.
class Typeable n => Attestable n where
  attest :: W n

instance Attestable N0 where
  attest :: W N0
attest = W N0
W0

instance Attestable n => Attestable (S n) where
  attest :: W ('S n)
attest = W n -> W (n + 1)
forall (d :: N'). W d -> W (d + 1)
SW W n
forall (n :: N'). Attestable n => W n
attest

--------------------------------------------------------------------------------
-- Ats -

-- | witness of being attestable.
data Ats n where Ats :: Attestable n => Ats n

--------------------------------------------------------------------------------
-- nValue -

-- | the corresponding natural number in 'N' of a type parameterized by @__n__@.
nValue :: Attestable n => p n -> N
nValue :: forall (n :: N') (p :: N' -> Type). Attestable n => p n -> N
nValue p n
p = p n -> Any n -> N
forall (p :: N' -> Type) (n :: N'). p n -> Any n -> N
nValue' p n
p Any n
forall (n :: N'). Attestable n => W n
attest where
  nValue' :: p n -> Any n -> N
  nValue' :: forall (p :: N' -> Type) (n :: N'). p n -> Any n -> N
nValue' p n
_ = Any n -> N
forall x. LengthN x => x -> N
lengthN

--------------------------------------------------------------------------------
-- ats -

-- | any natural @__n__@ is also attestable.
ats :: Any n -> Ats n
ats :: forall (n :: N'). Any n -> Ats n
ats W n
W0     = Ats n
forall (n :: N'). Attestable n => Ats n
Ats
ats (SW W n
n) = Ats n -> Ats (n + 1)
forall (n :: N'). Ats n -> Ats (n + 1)
atsSucc (W n -> Ats n
forall (n :: N'). Any n -> Ats n
ats W n
n)

--------------------------------------------------------------------------------
-- atsSucc -

-- | if @__n__@ is attestable then also @__n__ t'+' __1__@ is.
atsSucc :: Ats n -> Ats (n+1)
atsSucc :: forall (n :: N'). Ats n -> Ats (n + 1)
atsSucc Ats n
Ats = Ats (n + 1)
Ats ('S n)
forall (n :: N'). Attestable n => Ats n
Ats

--------------------------------------------------------------------------------
-- SomeNatural -

-- | witnesse of some natural.
data SomeNatural where
  SomeNatural :: Attestable n => W n -> SomeNatural

instance Show SomeNatural where
  show :: SomeNatural -> String
show (SomeNatural W n
n) = W n -> String
forall a. Show a => a -> String
show W n
n

-- | equality for witnesses.
eqlW :: W n -> W m -> Bool
eqlW :: forall (n :: N') (m :: N'). W n -> W m -> Bool
eqlW W n
W0 W m
W0         = Bool
True
eqlW W n
W0 (SW W n
_)     = Bool
False
eqlW (SW W n
_) W m
W0     = Bool
False
eqlW (SW W n
n) (SW W n
m) = W n -> W n -> Bool
forall (n :: N') (m :: N'). W n -> W m -> Bool
eqlW W n
n W n
m

instance Eq SomeNatural where
  SomeNatural W n
n == :: SomeNatural -> SomeNatural -> Bool
== SomeNatural W n
m = W n -> W n -> Bool
forall (n :: N') (m :: N'). W n -> W m -> Bool
eqlW W n
n W n
m

instance Validable SomeNatural where
  valid :: SomeNatural -> Statement
valid (SomeNatural W n
n) = W n -> Statement
forall a. Validable a => a -> Statement
valid W n
n

--------------------------------------------------------------------------------
-- succSomeNatural -

-- | successor of some natural number.
succSomeNatural :: SomeNatural -> SomeNatural
succSomeNatural :: SomeNatural -> SomeNatural
succSomeNatural (SomeNatural W n
n) = W ('S n) -> SomeNatural
forall (d :: N'). Attestable d => W d -> SomeNatural
SomeNatural (W n -> W (n + 1)
forall (d :: N'). W d -> W (d + 1)
SW W n
n)

--------------------------------------------------------------------------------
-- someNatural -

-- | mapping 'N' to 'SomeNatural'.
--
--   __Note__ The implementation of this mapping is quite inefficent for high values of 'N'.
someNatural :: N -> SomeNatural
someNatural :: N -> SomeNatural
someNatural N
0 = W N0 -> SomeNatural
forall (d :: N'). Attestable d => W d -> SomeNatural
SomeNatural W N0
W0
someNatural N
i = SomeNatural -> SomeNatural
succSomeNatural (N -> SomeNatural
someNatural (N -> N
forall a. Enum a => a -> a
pred N
i))

--------------------------------------------------------------------------------
-- xSomeNatural -

-- | the induced random variable for some natural number.
xSomeNatural :: X N -> X SomeNatural
xSomeNatural :: X N -> X SomeNatural
xSomeNatural X N
xn = X N
xn X N -> (N -> X SomeNatural) -> X SomeNatural
forall a b. X a -> (a -> X b) -> X b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= SomeNatural -> X SomeNatural
forall a. a -> X a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SomeNatural -> X SomeNatural)
-> (N -> SomeNatural) -> N -> X SomeNatural
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: Type -> Type -> Type) y z x.
Category c =>
c y z -> c x y -> c x z
. N -> SomeNatural
someNatural
    
--------------------------------------------------------------------------------
-- naturals -

-- | the infinite list of some naturals.
naturals :: [SomeNatural]
naturals :: [SomeNatural]
naturals = SomeNatural -> [SomeNatural]
nats (N -> SomeNatural
someNatural N
0) where nats :: SomeNatural -> [SomeNatural]
nats SomeNatural
n = SomeNatural
n SomeNatural -> [SomeNatural] -> [SomeNatural]
forall a. a -> [a] -> [a]
: SomeNatural -> [SomeNatural]
nats (SomeNatural -> SomeNatural
succSomeNatural SomeNatural
n)

--------------------------------------------------------------------------------
-- W' -

-- | union of all witnesses, which is isomorphic to 'N' and 'N''.
data W' = forall n . W' (W n) 

deriving instance Show W'

instance Eq W' where
  W' W n
n == :: W' -> W' -> Bool
== W' W n
m = case W n -> W n -> Ordering
forall (n :: N') (m :: N'). W n -> W m -> Ordering
cmpW W n
n W n
m of
    Ordering
EQ -> Bool
True
    Ordering
_  -> Bool
False

instance Ord W' where
  compare :: W' -> W' -> Ordering
compare (W' W n
n) (W' W n
m) = W n -> W n -> Ordering
forall (n :: N') (m :: N'). W n -> W m -> Ordering
cmpW W n
n W n
m

instance LengthN W' where
  lengthN :: W' -> N
lengthN (W' W n
w) = W n -> N
forall x. LengthN x => x -> N
lengthN W n
w

-- | mapping a natural value in 'N' to 'W''.
toW' :: N -> W'
toW' :: N -> W'
toW' N
0 = W N0 -> W'
forall (n :: N'). W n -> W'
W' W N0
W0
toW' N
n = W' -> W'
forall a. Enum a => a -> a
succ (W' -> W') -> W' -> W'
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ N -> W'
toW' (N
nN -> N -> N
>-N
1)

----------------------------------------
-- W' - Enum -

instance Enum W' where
  succ :: W' -> W'
succ (W' W n
w) = W ('S n) -> W'
forall (n :: N'). W n -> W'
W' (W n -> W (n + 1)
forall (d :: N'). W d -> W (d + 1)
SW W n
w)

  pred :: W' -> W'
pred (W' W n
W0)     = AlgebraicException -> W'
forall a e. Exception e => e -> a
throw AlgebraicException
NoPredecor
  pred (W' (SW W n
w)) = W n -> W'
forall (n :: N'). W n -> W'
W' W n
w

  toEnum :: Int -> W'
toEnum = N -> W'
toW' (N -> W') -> (Int -> N) -> Int -> W'
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: Type -> Type -> Type) y z x.
Category c =>
c y z -> c x y -> c x z
. Int -> N
forall a. Enum a => Int -> a
toEnum
  fromEnum :: W' -> Int
fromEnum = N -> Int
forall a. Enum a => a -> Int
fromEnum (N -> Int) -> (W' -> N) -> W' -> Int
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: Type -> Type -> Type) y z x.
Category c =>
c y z -> c x y -> c x z
. W' -> N
forall x. LengthN x => x -> N
lengthN

----------------------------------------
-- W' - Entity -

instance Validable W' where
  valid :: W' -> Statement
valid (W' W n
w) = W n -> Statement
forall a. Validable a => a -> Statement
valid W n
w

----------------------------------------
-- W' - Structure -
type instance Point W' = ()
instance ShowPoint W'
instance EqPoint W'
instance OrdPoint W'
instance SingletonPoint W'
instance ValidablePoint W'
instance TypeablePoint W'
instance Oriented W' where
  orientation :: W' -> Orientation (Point W')
orientation = Orientation () -> W' -> Orientation ()
forall b a. b -> a -> b
const (()() -> () -> Orientation ()
forall p. p -> p -> Orientation p
:>())

type instance Root W' = Orientation ()
instance ShowRoot W'
instance EqRoot W'
instance ValidableRoot W'
instance SingletonRoot W'
instance TypeableRoot W'
instance Fibred W' where
instance FibredOriented W'

instance Multiplicative W' where
  one :: Point W' -> W'
one () = W' -> W'
forall a. Enum a => a -> a
succ (Root W' -> W'
forall a. Additive a => Root a -> a
zero (()() -> () -> Orientation ()
forall p. p -> p -> Orientation p
:>()))
  W' W n
W0 * :: W' -> W' -> W'
* W'
_     = W N0 -> W'
forall (n :: N'). W n -> W'
W' W N0
W0
  W' (SW W n
n) * W'
m = W'
m W' -> W' -> W'
forall a. Additive a => a -> a -> a
+ W n -> W'
forall (n :: N'). W n -> W'
W' W n
n W' -> W' -> W'
forall c. Multiplicative c => c -> c -> c
* W'
m

instance Additive W' where
  zero :: Root W' -> W'
zero (():>()) = W N0 -> W'
forall (n :: N'). W n -> W'
W' W N0
W0
  W' W n
W0     + :: W' -> W' -> W'
+ W'
m = W'
m
  W' (SW W n
n) + W'
m = W' -> W'
forall a. Enum a => a -> a
succ (W n -> W'
forall (n :: N'). W n -> W'
W' W n
n W' -> W' -> W'
forall a. Additive a => a -> a -> a
+ W'
m)
  
instance Distributive W'
instance Commutative W'
-- instance Number W'

---------------------------------------------------------------------------------
-- Propositon -

-- | some witness.
type Some = W'

infixl 0 >>
(>>) :: forall {k} {a :: k} {b :: k} {c :: k} . (a :~: b) -> (b :~: c) -> a :~: c
>> :: forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
(>>) = (a :~: b) -> (b :~: c) -> a :~: c
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
trans

--------------------------------------------------------------------------------
-- refl -

-- | reflexivity.
refl :: Any x -> x :~: x
refl :: forall (x :: N'). Any x -> x :~: x
refl Any x
_ = x :~: x
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- lemma1 -

-- | well definition of parameterized types.
lemma1 :: x :~: y -> f x :~: f y
lemma1 :: forall {k} {k} (x :: k) (y :: k) (f :: k -> k).
(x :~: y) -> f x :~: f y
lemma1 x :~: y
Refl = f x :~: f x
f x :~: f y
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- sbstAdd -

-- | substitution rule for addition.
sbstAdd :: a :~: a' -> b :~: b' -> a + b :~: a' + b'
sbstAdd :: forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd a :~: a'
Refl b :~: b'
Refl = (a + b) :~: (a + b)
(a + b) :~: (a' + b')
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpAdd -

-- | @0@ is right neural for the addition.
prpAdd0 :: a + 0 :~: a
prpAdd0 :: forall (a :: N'). (a + 0) :~: a
prpAdd0 = a :~: a
(a + 0) :~: a
forall {k} (a :: k). a :~: a
Refl

-- | adding @1@ is equal to the successor.
prpAdd1 :: a + 1 :~: S a
prpAdd1 :: forall (a :: N'). (a + 1) :~: 'S a
prpAdd1 = (a + 1) :~: 'S a
'S a :~: 'S a
forall {k} (a :: k). a :~: a
Refl

-- | adding @2@ is equal to the successor of the successor.
prpAdd2 :: a + 2 :~: S (S a)
prpAdd2 :: forall (a :: N'). (a + 2) :~: 'S ('S a)
prpAdd2 = (a + 2) :~: 'S ('S a)
'S ('S a) :~: 'S ('S a)
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpMlt -

-- | mutlitplication with @0@ is zero.
prpMlt0 :: 0*a :~: N0
prpMlt0 :: forall (a :: N'). (0 * a) :~: N0
prpMlt0 = (0 * a) :~: N0
N0 :~: N0
forall {k} (a :: k). a :~: a
Refl

-- | @1@ is left neutral for the multiplication.
prpMlt1 :: 1*a :~: a
prpMlt1 :: forall (a :: N'). (1 * a) :~: a
prpMlt1 = a :~: a
(1 * a) :~: a
forall {k} (a :: k). a :~: a
Refl

prpMlt2 :: p a -> 2*a :~: a + a
prpMlt2 :: forall (p :: N' -> Type) (a :: N'). p a -> (2 * a) :~: (a + a)
prpMlt2 p a
_ = (2 * a) :~: (a + a)
(a + a) :~: (a + a)
forall {k} (a :: k). a :~: a
Refl

---------------------------------------------------------------------------------
-- prpEqlAny -

-- | equality of the underlying natural number.
prpEqlAny :: Any n :~: Any m -> n :~: m
prpEqlAny :: forall (n :: N') (m :: N'). (Any n :~: Any m) -> n :~: m
prpEqlAny Any n :~: Any m
Refl = n :~: n
n :~: m
forall {k} (a :: k). a :~: a
Refl

-- | 'Any' is as parameterized type is well defined.
prpEqlAny' ::  n :~: m -> Any n :~: Any m
prpEqlAny' :: forall (n :: N') (m :: N'). (n :~: m) -> Any n :~: Any m
prpEqlAny' n :~: m
Refl = Any n :~: Any n
Any n :~: W m
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpSuccInjective -

-- | successor is injective.
prpSuccInjective :: S n :~: S m -> n :~: m
prpSuccInjective :: forall (n :: N') (m :: N'). ('S n :~: 'S m) -> n :~: m
prpSuccInjective 'S n :~: 'S m
Refl = n :~: n
n :~: m
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpAddNtrlL -

-- | t'N0' is left neutral for the addition.
prpAddNtrlL :: p a -> N0 + a :~: a
prpAddNtrlL :: forall (p :: N' -> Type) (a :: N'). p a -> (N0 + a) :~: a
prpAddNtrlL p a
_ = a :~: a
(N0 + a) :~: a
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpAddNtrlR -

-- | t'N0' is the right neutral for the addition.
prpAddNtrlR :: Any a -> a + N0 :~: a

-- anchoring -
prpAddNtrlR :: forall (a :: N'). Any a -> (a + N0) :~: a
prpAddNtrlR W a
W0     = a :~: a
(a + N0) :~: a
forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
prpAddNtrlR (SW W n
a) = W n -> ((n + 1) + N0) :~: (n + 1)
forall (a :: N'). Any a -> ((a + 1) + N0) :~: (a + 1)
qed W n
a where
  qed :: Any a -> (a+1) + N0 :~: a+1
  qed :: forall (a :: N'). Any a -> ((a + 1) + N0) :~: (a + 1)
qed Any a
a = Any a -> ((a + 1) + N0) :~: ('S a + N0)
forall (p :: N' -> Type) (a :: N').
p a -> ((a + 1) + N0) :~: ('S a + N0)
r1 Any a
a ('S (a + N0) :~: 'S (a + N0))
-> ('S (a + N0) :~: 'S (a + N0)) -> 'S (a + N0) :~: 'S (a + N0)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> ('S a + N0) :~: 'S (a + N0)
forall (p :: N' -> Type) (a :: N').
p a -> ('S a + N0) :~: 'S (a + N0)
r2 Any a
a ('S (a + N0) :~: 'S (a + N0))
-> ('S (a + N0) :~: 'S a) -> 'S (a + N0) :~: 'S a
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> 'S (a + N0) :~: 'S a
forall (a :: N'). Any a -> 'S (a + N0) :~: 'S a
hyp Any a
a ('S (a + N0) :~: 'S a) -> ('S a :~: 'S a) -> 'S (a + N0) :~: 'S a
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> 'S a :~: (a + 1)
forall (p :: N' -> Type) (a :: N'). p a -> 'S a :~: (a + 1)
r3 Any a
a

  r1  :: p a   -> (a+1) + N0 :~: S a + N0
  r2  :: p a   -> S a + N0   :~: S (a + N0)
  hyp :: Any a -> S (a + N0) :~: S a
  r3  :: p a   -> S a        :~: a+1

  r1 :: forall (p :: N' -> Type) (a :: N').
p a -> ((a + 1) + N0) :~: ('S a + N0)
r1  p a
_ = ((a + 1) + N0) :~: ('S a + N0)
'S (a + N0) :~: 'S (a + N0)
forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (p :: N' -> Type) (a :: N').
p a -> ('S a + N0) :~: 'S (a + N0)
r2  p a
_ = ('S a + N0) :~: 'S (a + N0)
'S (a + N0) :~: 'S (a + N0)
forall {k} (a :: k). a :~: a
Refl 
  hyp :: forall (a :: N'). Any a -> 'S (a + N0) :~: 'S a
hyp Any a
a = ((a + N0) :~: a) -> 'S (a + N0) :~: 'S a
forall {k} {k} (x :: k) (y :: k) (f :: k -> k).
(x :~: y) -> f x :~: f y
lemma1 (((a + N0) :~: a) -> 'S (a + N0) :~: 'S a)
-> ((a + N0) :~: a) -> 'S (a + N0) :~: 'S a
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any a -> (a + N0) :~: a
forall (a :: N'). Any a -> (a + N0) :~: a
prpAddNtrlR Any a
a
  r3 :: forall (p :: N' -> Type) (a :: N'). p a -> 'S a :~: (a + 1)
r3  p a
_ = 'S a :~: (a + 1)
'S a :~: 'S a
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpAddAssoc -

-- | addition is associative.
prpAddAssoc :: Any a -> Any b -> Any c -> (a + b) + c :~: a + (b + c)

-- anchoring -
prpAddAssoc :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc W a
W0 Any b
_ Any c
_ = (b + c) :~: (b + c)
((a + b) + c) :~: (a + (b + c))
forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
prpAddAssoc (SW W n
a) Any b
b Any c
c = W n
-> Any b -> Any c -> (((n + 1) + b) + c) :~: ((n + 1) + (b + c))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> (((a + 1) + b) + c) :~: ((a + 1) + (b + c))
qed W n
a Any b
b Any c
c where
  qed :: Any a -> Any b -> Any c -> ((a+1) + b) + c :~: (a+1) + (b + c)
  qed :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> (((a + 1) + b) + c) :~: ((a + 1) + (b + c))
qed Any a
a Any b
b Any c
c = Any a -> Any b -> Any c -> (((a + 1) + b) + c) :~: (('S a + b) + c)
forall {k} {k} (a :: N') (p :: k -> Type) (b :: k) (q :: k -> Type)
       (c :: k).
Any a -> p b -> q c -> (((a + 1) + b) + c) :~: (('S a + b) + c)
r1 Any a
a Any b
b Any c
c ('S ((a + b) + c) :~: 'S ((a + b) + c))
-> ('S ((a + b) + c) :~: 'S ((a + b) + c))
-> 'S ((a + b) + c) :~: 'S ((a + b) + c)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> Any c -> (('S a + b) + c) :~: ('S (a + b) + c)
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (('S a + b) + c) :~: ('S (a + b) + c)
r2 Any a
a Any b
b Any c
c ('S ((a + b) + c) :~: 'S ((a + b) + c))
-> ('S ((a + b) + c) :~: 'S ((a + b) + c))
-> 'S ((a + b) + c) :~: 'S ((a + b) + c)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> Any c -> ('S (a + b) + c) :~: 'S ((a + b) + c)
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S (a + b) + c) :~: 'S ((a + b) + c)
r3 Any a
a Any b
b Any c
c ('S ((a + b) + c) :~: 'S ((a + b) + c))
-> ('S ((a + b) + c) :~: 'S (a + (b + c)))
-> 'S ((a + b) + c) :~: 'S (a + (b + c))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> Any c -> 'S ((a + b) + c) :~: 'S (a + (b + c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> 'S ((a + b) + c) :~: 'S (a + (b + c))
hyp Any a
a Any b
b Any c
c ('S ((a + b) + c) :~: 'S (a + (b + c)))
-> ('S (a + (b + c)) :~: 'S (a + (b + c)))
-> 'S ((a + b) + c) :~: 'S (a + (b + c))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> Any c -> 'S (a + (b + c)) :~: ('S a + (b + c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> 'S (a + (b + c)) :~: ('S a + (b + c))
r4 Any a
a Any b
b Any c
c ('S ((a + b) + c) :~: 'S (a + (b + c)))
-> ('S (a + (b + c)) :~: 'S (a + (b + c)))
-> 'S ((a + b) + c) :~: 'S (a + (b + c))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> Any c -> ('S a + (b + c)) :~: ((a + 1) + (b + c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S a + (b + c)) :~: ((a + 1) + (b + c))
r5 Any a
a Any b
b Any c
c 

  r1  :: Any a -> p b   -> q c   -> ((a+1) + b) + c :~: (S a + b) + c
  r2  :: Any a -> Any b -> Any c -> (S a + b) + c   :~: S (a + b) + c
  r3  :: Any a -> Any b -> Any c -> S (a + b) + c   :~: S ((a + b) + c)
  hyp :: Any a -> Any b -> Any c -> S ((a + b) + c) :~: S (a + (b + c))
  r4  :: Any a -> Any b -> Any c -> S (a + (b + c)) :~: (S a + (b + c)) 
  r5  :: Any a -> Any b -> Any c -> S a + (b + c)   :~: (a+1) + (b + c)

  r1 :: forall {k} {k} (a :: N') (p :: k -> Type) (b :: k) (q :: k -> Type)
       (c :: k).
Any a -> p b -> q c -> (((a + 1) + b) + c) :~: (('S a + b) + c)
r1  Any a
_ p b
_ q c
_ = (((a + 1) + b) + c) :~: (('S a + b) + c)
(('S a + b) + c) :~: (('S a + b) + c)
forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (('S a + b) + c) :~: ('S (a + b) + c)
r2  Any a
_ Any b
_ Any c
_ = (('S a + b) + c) :~: ('S (a + b) + c)
'S ((a + b) + c) :~: 'S ((a + b) + c)
forall {k} (a :: k). a :~: a
Refl
  r3 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S (a + b) + c) :~: 'S ((a + b) + c)
r3  Any a
_ Any b
_ Any c
_ = ('S (a + b) + c) :~: 'S ((a + b) + c)
'S ((a + b) + c) :~: 'S ((a + b) + c)
forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> 'S ((a + b) + c) :~: 'S (a + (b + c))
hyp Any a
a Any b
b Any c
c = (((a + b) + c) :~: (a + (b + c)))
-> 'S ((a + b) + c) :~: 'S (a + (b + c))
forall {k} {k} (x :: k) (y :: k) (f :: k -> k).
(x :~: y) -> f x :~: f y
lemma1 ((((a + b) + c) :~: (a + (b + c)))
 -> 'S ((a + b) + c) :~: 'S (a + (b + c)))
-> (((a + b) + c) :~: (a + (b + c)))
-> 'S ((a + b) + c) :~: 'S (a + (b + c))
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc Any a
a Any b
b Any c
c 
  r4 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> 'S (a + (b + c)) :~: ('S a + (b + c))
r4  Any a
_ Any b
_ Any c
_ = 'S (a + (b + c)) :~: ('S a + (b + c))
'S (a + (b + c)) :~: 'S (a + (b + c))
forall {k} (a :: k). a :~: a
Refl
  r5 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S a + (b + c)) :~: ((a + 1) + (b + c))
r5  Any a
_ Any b
_ Any c
_ = ('S a + (b + c)) :~: ((a + 1) + (b + c))
'S (a + (b + c)) :~: 'S (a + (b + c))
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- lemmaAdd1 -

-- | lemma 1 for the addition.
lemmaAdd1 :: Any a -> Any b -> S a + b :~: a + S b

-- anchoring -
lemmaAdd1 :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + b) :~: (a + 'S b)
lemmaAdd1 W a
W0 Any b
_ = ('S a + b) :~: (a + 'S b)
'S b :~: 'S b
forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
lemmaAdd1 (SW W n
a) Any b
b = W n -> Any b -> ('S (n + 1) + b) :~: ((n + 1) + 'S b)
forall (a :: N') (b :: N').
Any a -> Any b -> ('S (a + 1) + b) :~: ((a + 1) + 'S b)
qed W n
a Any b
b where
  qed :: Any a -> Any b -> S (a+1) + b :~: (a+1) + S b
  qed :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S (a + 1) + b) :~: ((a + 1) + 'S b)
qed Any a
a Any b
b = Any a -> Any b -> ('S (a + 1) + b) :~: ('S ('S a) + b)
forall (a :: N') (b :: N').
Any a -> Any b -> ('S (a + 1) + b) :~: ('S ('S a) + b)
r1 Any a
a Any b
b ('S ('S (a + b)) :~: 'S ('S (a + b)))
-> ('S ('S (a + b)) :~: 'S ('S (a + b)))
-> 'S ('S (a + b)) :~: 'S ('S (a + b))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> ('S ('S a) + b) :~: 'S ('S a + b)
forall (a :: N') (b :: N').
Any a -> Any b -> ('S ('S a) + b) :~: 'S ('S a + b)
r2 Any a
a Any b
b ('S ('S (a + b)) :~: 'S ('S (a + b)))
-> ('S ('S (a + b)) :~: 'S (a + 'S b))
-> 'S ('S (a + b)) :~: 'S (a + 'S b)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> 'S ('S a + b) :~: 'S (a + 'S b)
forall (a :: N') (b :: N').
Any a -> Any b -> 'S ('S a + b) :~: 'S (a + 'S b)
hyp Any a
a Any b
b ('S ('S (a + b)) :~: 'S (a + 'S b))
-> ('S (a + 'S b) :~: 'S (a + 'S b))
-> 'S ('S (a + b)) :~: 'S (a + 'S b)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> 'S (a + 'S b) :~: ('S a + 'S b)
forall (a :: N') (b :: N').
Any a -> Any b -> 'S (a + 'S b) :~: ('S a + 'S b)
r3 Any a
a Any b
b ('S ('S (a + b)) :~: 'S (a + 'S b))
-> ('S (a + 'S b) :~: 'S (a + 'S b))
-> 'S ('S (a + b)) :~: 'S (a + 'S b)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> ('S a + 'S b) :~: ((a + 1) + 'S b)
forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + 'S b) :~: ((a + 1) + 'S b)
r4 Any a
a Any b
b

  r1  :: Any a -> Any b -> S (a+1) + b :~: S (S a) + b
  r2  :: Any a -> Any b -> S (S a) + b :~: S (S a + b)
  hyp :: Any a -> Any b -> S (S a + b) :~: S (a + S b)
  r3  :: Any a -> Any b -> S (a + S b) :~: S a + S b
  r4  :: Any a -> Any b -> S a + S b   :~: (a+1) + S b  

  r1 :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S (a + 1) + b) :~: ('S ('S a) + b)
r1  Any a
_ Any b
_ = ('S (a + 1) + b) :~: ('S ('S a) + b)
'S ('S (a + b)) :~: 'S ('S (a + b))
forall {k} (a :: k). a :~: a
Refl 
  r2 :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S ('S a) + b) :~: 'S ('S a + b)
r2  Any a
_ Any b
_ = ('S ('S a) + b) :~: 'S ('S a + b)
'S ('S (a + b)) :~: 'S ('S (a + b))
forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N') (b :: N').
Any a -> Any b -> 'S ('S a + b) :~: 'S (a + 'S b)
hyp Any a
a Any b
b = ('S (a + b) :~: (a + 'S b)) -> 'S ('S (a + b)) :~: 'S (a + 'S b)
forall {k} {k} (x :: k) (y :: k) (f :: k -> k).
(x :~: y) -> f x :~: f y
lemma1 (('S (a + b) :~: (a + 'S b)) -> 'S ('S (a + b)) :~: 'S (a + 'S b))
-> ('S (a + b) :~: (a + 'S b)) -> 'S ('S (a + b)) :~: 'S (a + 'S b)
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any a -> Any b -> ('S a + b) :~: (a + 'S b)
forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + b) :~: (a + 'S b)
lemmaAdd1 Any a
a Any b
b
  r3 :: forall (a :: N') (b :: N').
Any a -> Any b -> 'S (a + 'S b) :~: ('S a + 'S b)
r3  Any a
_ Any b
_ = 'S (a + 'S b) :~: ('S a + 'S b)
'S (a + 'S b) :~: 'S (a + 'S b)
forall {k} (a :: k). a :~: a
Refl
  r4 :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + 'S b) :~: ((a + 1) + 'S b)
r4  Any a
_ Any b
_ = ('S a + 'S b) :~: ((a + 1) + 'S b)
'S (a + 'S b) :~: 'S (a + 'S b)
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpAddComm -

-- | addition is commutative.
prpAddComm :: Any a -> Any b -> a + b :~: b + a 

-- anchoring -
prpAddComm :: forall (a :: N') (b :: N'). Any a -> Any b -> (a + b) :~: (b + a)
prpAddComm W a
W0 Any b
b = Any b -> (N0 + b) :~: (b + N0)
forall (b :: N'). Any b -> (N0 + b) :~: (b + N0)
qed Any b
b where
  qed :: Any b -> N0 + b :~: b + N0
  qed :: forall (b :: N'). Any b -> (N0 + b) :~: (b + N0)
qed Any b
b = Any b -> (N0 + b) :~: b
forall (b :: N'). Any b -> (N0 + b) :~: b
r1 Any b
b (b :~: b) -> (b :~: (b + N0)) -> b :~: (b + N0)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any b -> b :~: (b + N0)
forall (b :: N'). Any b -> b :~: (b + N0)
r2 Any b
b

  r1 :: Any b -> N0 + b :~: b
  r2 :: Any b -> b      :~: b + N0

  r1 :: forall (b :: N'). Any b -> (N0 + b) :~: b
r1 = W b -> (N0 + b) :~: b
forall (p :: N' -> Type) (a :: N'). p a -> (N0 + a) :~: a
prpAddNtrlL
  r2 :: forall (b :: N'). Any b -> b :~: (b + N0)
r2 Any b
b = ((b + N0) :~: b) -> b :~: (b + N0)
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (((b + N0) :~: b) -> b :~: (b + N0))
-> ((b + N0) :~: b) -> b :~: (b + N0)
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any b -> (b + N0) :~: b
forall (a :: N'). Any a -> (a + N0) :~: a
prpAddNtrlR Any b
b

-- hypothesis -
prpAddComm (SW W n
a) Any b
b = W n -> Any b -> ((n + 1) + b) :~: (b + (n + 1))
forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) + b) :~: (b + (a + 1))
qed W n
a Any b
b where
  qed :: Any a -> Any b -> (a+1) + b :~: b + (a+1)
  qed :: forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) + b) :~: (b + (a + 1))
qed Any a
a Any b
b = Any a -> Any b -> ((a + 1) + b) :~: ('S a + b)
forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) + b) :~: ('S a + b)
r1 Any a
a Any b
b ('S (a + b) :~: 'S (a + b))
-> ('S (a + b) :~: 'S (a + b)) -> 'S (a + b) :~: 'S (a + b)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> ('S a + b) :~: 'S (a + b)
forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + b) :~: 'S (a + b)
r2 Any a
a Any b
b ('S (a + b) :~: 'S (a + b))
-> ('S (a + b) :~: 'S (b + a)) -> 'S (a + b) :~: 'S (b + a)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> 'S (a + b) :~: 'S (b + a)
forall (a :: N') (b :: N').
Any a -> Any b -> 'S (a + b) :~: 'S (b + a)
hyp Any a
a Any b
b ('S (a + b) :~: 'S (b + a))
-> ('S (b + a) :~: 'S (b + a)) -> 'S (a + b) :~: 'S (b + a)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> 'S (b + a) :~: ('S b + a)
forall (a :: N') (b :: N').
Any a -> Any b -> 'S (b + a) :~: ('S b + a)
r3 Any a
a Any b
b ('S (a + b) :~: 'S (b + a))
-> ('S (b + a) :~: (b + 'S a)) -> 'S (a + b) :~: (b + 'S a)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> ('S b + a) :~: (b + 'S a)
forall (a :: N') (b :: N').
Any a -> Any b -> ('S b + a) :~: (b + 'S a)
r4 Any a
a Any b
b ('S (a + b) :~: (b + 'S a))
-> ((b + 'S a) :~: (b + 'S a)) -> 'S (a + b) :~: (b + 'S a)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> (b + 'S a) :~: (b + (a + 1))
forall (a :: N') (b :: N').
Any a -> Any b -> (b + 'S a) :~: (b + (a + 1))
r5 Any a
a Any b
b

  r1  :: Any a -> Any b -> (a+1) + b :~: S a + b
  r2  :: Any a -> Any b -> S a + b   :~: S (a + b)
  hyp :: Any a -> Any b -> S (a + b) :~: S (b + a)
  r3  :: Any a -> Any b -> S (b + a) :~: S b + a 
  r4  :: Any a -> Any b -> S b + a   :~: b + S a
  r5  :: Any a -> Any b -> b + S a   :~: b + (a+1)

  r1 :: forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) + b) :~: ('S a + b)
r1  Any a
_ Any b
_ = ((a + 1) + b) :~: ('S a + b)
'S (a + b) :~: 'S (a + b)
forall {k} (a :: k). a :~: a
Refl 
  r2 :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + b) :~: 'S (a + b)
r2  Any a
_ Any b
_ = ('S a + b) :~: 'S (a + b)
'S (a + b) :~: 'S (a + b)
forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N') (b :: N').
Any a -> Any b -> 'S (a + b) :~: 'S (b + a)
hyp Any a
a Any b
b = ((a + b) :~: (b + a)) -> 'S (a + b) :~: 'S (b + a)
forall {k} {k} (x :: k) (y :: k) (f :: k -> k).
(x :~: y) -> f x :~: f y
lemma1 (((a + b) :~: (b + a)) -> 'S (a + b) :~: 'S (b + a))
-> ((a + b) :~: (b + a)) -> 'S (a + b) :~: 'S (b + a)
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any a -> Any b -> (a + b) :~: (b + a)
forall (a :: N') (b :: N'). Any a -> Any b -> (a + b) :~: (b + a)
prpAddComm Any a
a Any b
b
  r3 :: forall (a :: N') (b :: N').
Any a -> Any b -> 'S (b + a) :~: ('S b + a)
r3  Any a
_ Any b
_ = 'S (b + a) :~: ('S b + a)
'S (b + a) :~: 'S (b + a)
forall {k} (a :: k). a :~: a
Refl
  r4 :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S b + a) :~: (b + 'S a)
r4  Any a
a Any b
b = Any b -> Any a -> ('S b + a) :~: (b + 'S a)
forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + b) :~: (a + 'S b)
lemmaAdd1 Any b
b Any a
a 
  r5 :: forall (a :: N') (b :: N').
Any a -> Any b -> (b + 'S a) :~: (b + (a + 1))
r5  Any a
_ Any b
_ = (b + 'S a) :~: (b + (a + 1))
(b + 'S a) :~: (b + 'S a)
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpMltNtrlL -

-- | 'N1' is left neutral for the multiplication.
prpMltNtrlL :: Any a -> N1*a :~: a
prpMltNtrlL :: forall (a :: N'). Any a -> (N1 * a) :~: a
prpMltNtrlL Any a
a = Any a -> (N1 * a) :~: a
forall (a :: N'). Any a -> (N1 * a) :~: a
qed Any a
a where
  qed :: Any a -> N1 * a :~: a
  qed :: forall (a :: N'). Any a -> (N1 * a) :~: a
qed Any a
a = Any a -> (N1 * a) :~: (N1 * a)
forall (a :: N'). Any a -> (N1 * a) :~: (N1 * a)
r1 Any a
a ((a + N0) :~: (a + N0))
-> ((a + N0) :~: (a + N0)) -> (a + N0) :~: (a + N0)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> (N1 * a) :~: (a + (N0 * a))
forall (a :: N'). Any a -> (N1 * a) :~: (a + (N0 * a))
r2 Any a
a ((a + N0) :~: (a + N0))
-> ((a + N0) :~: (a + N0)) -> (a + N0) :~: (a + N0)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> (a + (N0 * a)) :~: (a + N0)
forall (a :: N'). Any a -> (a + (N0 * a)) :~: (a + N0)
r3 Any a
a ((a + N0) :~: (a + N0)) -> ((a + N0) :~: a) -> (a + N0) :~: a
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> (a + N0) :~: a
forall (a :: N'). Any a -> (a + N0) :~: a
r4 Any a
a

  r1  :: Any a -> N1 * a   :~: (S N0)*a
  r2  :: Any a -> (S N0)*a :~: a + N0*a
  r3  :: Any a -> a + N0*a :~: a + N0
  r4  :: Any a -> a + N0   :~: a


  r1 :: forall (a :: N'). Any a -> (N1 * a) :~: (N1 * a)
r1 Any a
_ = (N1 * a) :~: (N1 * a)
(a + N0) :~: (a + N0)
forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N'). Any a -> (N1 * a) :~: (a + (N0 * a))
r2 Any a
_ = (N1 * a) :~: (a + (N0 * a))
(a + N0) :~: (a + N0)
forall {k} (a :: k). a :~: a
Refl
  r3 :: forall (a :: N'). Any a -> (a + (N0 * a)) :~: (a + N0)
r3 Any a
_ = (a + (N0 * a)) :~: (a + N0)
(a + N0) :~: (a + N0)
forall {k} (a :: k). a :~: a
Refl
  r4 :: forall (a :: N'). Any a -> (a + N0) :~: a
r4 Any a
a = Any a -> (a + N0) :~: a
forall (a :: N'). Any a -> (a + N0) :~: a
prpAddNtrlR Any a
a 

--------------------------------------------------------------------------------
-- prpMltNtrlR -

-- | 'N1' is right neutral for the multiplication.
prpMltNtrlR :: Any a -> a*N1 :~: a

-- anchoring -
prpMltNtrlR :: forall (a :: N'). Any a -> (a * N1) :~: a
prpMltNtrlR W a
W0 = a :~: a
(a * N1) :~: a
forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
prpMltNtrlR (SW W n
a) = W n -> ((n + 1) * N1) :~: (n + 1)
forall (a :: N'). Any a -> ((a + 1) * N1) :~: (a + 1)
qed W n
a where
  qed :: Any a -> (a+1)*N1 :~: a+1
  qed :: forall (a :: N'). Any a -> ((a + 1) * N1) :~: (a + 1)
qed Any a
a = Any a -> ((a + 1) * N1) :~: ('S a * N1)
forall (a :: N'). Any a -> ((a + 1) * N1) :~: ('S a * N1)
r1 Any a
a ('S (a * N1) :~: 'S (a * N1))
-> ('S (a * N1) :~: 'S (a * N1)) -> 'S (a * N1) :~: 'S (a * N1)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> ('S a * N1) :~: (N1 + (a * N1))
forall (a :: N'). Any a -> ('S a * N1) :~: (N1 + (a * N1))
r2 Any a
a ('S (a * N1) :~: 'S (a * N1))
-> ('S (a * N1) :~: 'S a) -> 'S (a * N1) :~: 'S a
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> (N1 + (a * N1)) :~: (N1 + a)
forall (a :: N'). Any a -> (N1 + (a * N1)) :~: (N1 + a)
hyp Any a
a ('S (a * N1) :~: 'S a) -> ('S a :~: 'S a) -> 'S (a * N1) :~: 'S a
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> (N1 + a) :~: (N1 + a)
forall (a :: N'). Any a -> (N1 + a) :~: (N1 + a)
r3 Any a
a ('S (a * N1) :~: 'S a) -> ('S a :~: 'S a) -> 'S (a * N1) :~: 'S a
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> (N1 + a) :~: (N0 + 'S a)
forall (a :: N'). Any a -> (N1 + a) :~: (N0 + 'S a)
r4 Any a
a ('S (a * N1) :~: 'S a) -> ('S a :~: 'S a) -> 'S (a * N1) :~: 'S a
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> (N0 + 'S a) :~: 'S a
forall (a :: N'). Any a -> (N0 + 'S a) :~: 'S a
r5 Any a
a ('S (a * N1) :~: 'S a) -> ('S a :~: 'S a) -> 'S (a * N1) :~: 'S a
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> 'S a :~: (a + 1)
forall (a :: N'). Any a -> 'S a :~: (a + 1)
r6 Any a
a

  r1  :: Any a -> (a+1)*N1   :~: S a * N1
  r2  :: Any a -> S a * N1   :~: N1 + a*N1
  hyp :: Any a -> N1 + a*N1  :~: N1 + a
  r3  :: Any a -> N1 + a     :~: S N0 + a
  r4  :: Any a -> S N0 + a   :~: N0 + S a
  r5  :: Any a -> N0 + S a   :~: S a 
  r6  :: Any a -> S a        :~: a+1

  r1 :: forall (a :: N'). Any a -> ((a + 1) * N1) :~: ('S a * N1)
r1  Any a
_ = ((a + 1) * N1) :~: ('S a * N1)
'S (a * N1) :~: 'S (a * N1)
forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N'). Any a -> ('S a * N1) :~: (N1 + (a * N1))
r2  Any a
_ = ('S a * N1) :~: (N1 + (a * N1))
'S (a * N1) :~: 'S (a * N1)
forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N'). Any a -> (N1 + (a * N1)) :~: (N1 + a)
hyp Any a
a = (N1 :~: N1) -> ((a * N1) :~: a) -> (N1 + (a * N1)) :~: (N1 + a)
forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (Any N1 -> N1 :~: N1
forall (x :: N'). Any x -> x :~: x
refl Any N1
w1) (Any a -> (a * N1) :~: a
forall (a :: N'). Any a -> (a * N1) :~: a
prpMltNtrlR Any a
a)
  r3 :: forall (a :: N'). Any a -> (N1 + a) :~: (N1 + a)
r3  Any a
_ = (N1 + a) :~: (N1 + a)
'S a :~: 'S a
forall {k} (a :: k). a :~: a
Refl
  r4 :: forall (a :: N'). Any a -> (N1 + a) :~: (N0 + 'S a)
r4  Any a
a = W N0 -> Any a -> (N1 + a) :~: (N0 + 'S a)
forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + b) :~: (a + 'S b)
lemmaAdd1 W N0
w0 Any a
a
  r5 :: forall (a :: N'). Any a -> (N0 + 'S a) :~: 'S a
r5  Any a
_ = (N0 + 'S a) :~: 'S a
'S a :~: 'S a
forall {k} (a :: k). a :~: a
Refl
  r6 :: forall (a :: N'). Any a -> 'S a :~: (a + 1)
r6  Any a
_ = 'S a :~: (a + 1)
'S a :~: 'S a
forall {k} (a :: k). a :~: a
Refl


--------------------------------------------------------------------------------
-- prpDstrL -

-- | law of left distributivity holds.
prpDstrL :: Any a -> Any b -> Any c -> (a + b)*c :~: a*c + b*c

-- anchoring -
prpDstrL :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) * c) :~: ((a * c) + (b * c))
prpDstrL W a
W0 Any b
_ Any c
_ = (b * c) :~: (b * c)
((a + b) * c) :~: ((a * c) + (b * c))
forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
prpDstrL (SW W n
a) Any b
b Any c
c = W n
-> Any b
-> Any c
-> (((n + 1) + b) * c) :~: (((n + 1) * c) + (b * c))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (((a + 1) + b) * c) :~: (((a + 1) * c) + (b * c))
qed W n
a Any b
b Any c
c where
  qed :: Any a -> Any b -> Any c -> ((a+1) + b)*c :~: (a+1)*c + b*c
  qed :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (((a + 1) + b) * c) :~: (((a + 1) * c) + (b * c))
qed Any a
a Any b
b Any c
c =  Any a -> Any b -> Any c -> (((a + 1) + b) * c) :~: (('S a + b) * c)
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (((a + 1) + b) * c) :~: (('S a + b) * c)
r1 Any a
a Any b
b Any c
c ((c + ((a + b) * c)) :~: (c + ((a + b) * c)))
-> ((c + ((a + b) * c)) :~: (c + ((a + b) * c)))
-> (c + ((a + b) * c)) :~: (c + ((a + b) * c))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> Any c -> (('S a + b) * c) :~: ('S (a + b) * c)
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (('S a + b) * c) :~: ('S (a + b) * c)
r2 Any a
a Any b
b Any c
c ((c + ((a + b) * c)) :~: (c + ((a + b) * c)))
-> ((c + ((a + b) * c)) :~: (c + ((a + b) * c)))
-> (c + ((a + b) * c)) :~: (c + ((a + b) * c))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> Any c -> ('S (a + b) * c) :~: (c + ((a + b) * c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S (a + b) * c) :~: (c + ((a + b) * c))
r3 Any a
a Any b
b Any c
c
            ((c + ((a + b) * c)) :~: (c + ((a + b) * c)))
-> ((c + ((a + b) * c)) :~: (c + ((a * c) + (b * c))))
-> (c + ((a + b) * c)) :~: (c + ((a * c) + (b * c)))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a
-> Any b
-> Any c
-> (c + ((a + b) * c)) :~: (c + ((a * c) + (b * c)))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (c + ((a + b) * c)) :~: (c + ((a * c) + (b * c)))
hyp Any a
a Any b
b Any c
c ((c + ((a + b) * c)) :~: (c + ((a * c) + (b * c))))
-> ((c + ((a * c) + (b * c))) :~: ((c + (a * c)) + (b * c)))
-> (c + ((a + b) * c)) :~: ((c + (a * c)) + (b * c))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a
-> Any b
-> Any c
-> (c + ((a * c) + (b * c))) :~: ((c + (a * c)) + (b * c))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (c + ((a * c) + (b * c))) :~: ((c + (a * c)) + (b * c))
r4 Any a
a Any b
b Any c
c ((c + ((a + b) * c)) :~: ((c + (a * c)) + (b * c)))
-> (((c + (a * c)) + (b * c)) :~: ((c + (a * c)) + (b * c)))
-> (c + ((a + b) * c)) :~: ((c + (a * c)) + (b * c))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a
-> Any b
-> Any c
-> ((c + (a * c)) + (b * c)) :~: (((a + 1) * c) + (b * c))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((c + (a * c)) + (b * c)) :~: (((a + 1) * c) + (b * c))
r5 Any a
a Any b
b Any c
c

  r1  :: Any a -> Any b -> Any c -> ((a+1) + b)*c   :~: (S a + b)*c
  r2  :: Any a -> Any b -> Any c -> (S a + b)*c     :~: S (a + b) * c
  r3  :: Any a -> Any b -> Any c -> S (a + b) * c   :~: c + (a + b)*c
  hyp :: Any a -> Any b -> Any c -> c + (a + b)*c   :~: c + a*c + b*c
  r4  :: Any a -> Any b -> Any c -> c + a*c + b*c   :~: (c + a*c) + b*c
  r5  :: Any a -> Any b -> Any c -> (c + a*c) + b*c :~: (a+1)*c + b*c

  r1 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (((a + 1) + b) * c) :~: (('S a + b) * c)
r1  Any a
_ Any b
_ Any c
_ = (((a + 1) + b) * c) :~: (('S a + b) * c)
(c + ((a + b) * c)) :~: (c + ((a + b) * c))
forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (('S a + b) * c) :~: ('S (a + b) * c)
r2  Any a
_ Any b
_ Any c
_ = (('S a + b) * c) :~: ('S (a + b) * c)
(c + ((a + b) * c)) :~: (c + ((a + b) * c))
forall {k} (a :: k). a :~: a
Refl
  r3 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S (a + b) * c) :~: (c + ((a + b) * c))
r3  Any a
_ Any b
_ Any c
_ = ('S (a + b) * c) :~: (c + ((a + b) * c))
(c + ((a + b) * c)) :~: (c + ((a + b) * c))
forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (c + ((a + b) * c)) :~: (c + ((a * c) + (b * c)))
hyp Any a
a Any b
b Any c
c = (c :~: c)
-> (((a + b) * c) :~: ((a * c) + (b * c)))
-> (c + ((a + b) * c)) :~: (c + ((a * c) + (b * c)))
forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (Any c -> c :~: c
forall (x :: N'). Any x -> x :~: x
refl Any c
c) (Any a -> Any b -> Any c -> ((a + b) * c) :~: ((a * c) + (b * c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) * c) :~: ((a * c) + (b * c))
prpDstrL Any a
a Any b
b Any c
c)
  r4 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (c + ((a * c) + (b * c))) :~: ((c + (a * c)) + (b * c))
r4  Any a
a Any b
b Any c
c = (((c + (a * c)) + (b * c)) :~: (c + ((a * c) + (b * c))))
-> (c + ((a * c) + (b * c))) :~: ((c + (a * c)) + (b * c))
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((((c + (a * c)) + (b * c)) :~: (c + ((a * c) + (b * c))))
 -> (c + ((a * c) + (b * c))) :~: ((c + (a * c)) + (b * c)))
-> (((c + (a * c)) + (b * c)) :~: (c + ((a * c) + (b * c))))
-> (c + ((a * c) + (b * c))) :~: ((c + (a * c)) + (b * c))
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any c
-> Any (a * c)
-> Any (b * c)
-> ((c + (a * c)) + (b * c)) :~: (c + ((a * c) + (b * c)))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc Any c
c (Any a
aAny a -> Any c -> Any (a * c)
forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any c
c) (Any b
bAny b -> Any c -> Any (b * c)
forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any c
c)
  r5 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((c + (a * c)) + (b * c)) :~: (((a + 1) * c) + (b * c))
r5  Any a
_ Any b
_ Any c
_ = ((c + (a * c)) + (b * c)) :~: (((a + 1) * c) + (b * c))
((c + (a * c)) + (b * c)) :~: ((c + (a * c)) + (b * c))
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpMltAssoc -

-- | multiplication is associative.
prpMltAssoc :: Any a -> Any b -> Any c -> (a*b)*c :~: a*(b*c)

-- anchoring -
prpMltAssoc :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a * b) * c) :~: (a * (b * c))
prpMltAssoc W a
W0 Any b
_ Any c
_ = ((a * b) * c) :~: (a * (b * c))
N0 :~: N0
forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
prpMltAssoc (SW W n
a) Any b
b Any c
c = W n
-> Any b -> Any c -> (((n + 1) * b) * c) :~: ((n + 1) * (b * c))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> (((a + 1) * b) * c) :~: ((a + 1) * (b * c))
qed W n
a Any b
b Any c
c where
  qed :: Any a -> Any b -> Any c -> ((a+1)*b)*c :~: (a+1)*(b*c)
  qed :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> (((a + 1) * b) * c) :~: ((a + 1) * (b * c))
qed Any a
a Any b
b Any c
c = Any a -> Any b -> Any c -> (((a + 1) * b) * c) :~: (('S a * b) * c)
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (((a + 1) * b) * c) :~: (('S a * b) * c)
r1 Any a
a Any b
b Any c
c (((b + (a * b)) * c) :~: ((b + (a * b)) * c))
-> (((b + (a * b)) * c) :~: ((b + (a * b)) * c))
-> ((b + (a * b)) * c) :~: ((b + (a * b)) * c)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> Any c -> (('S a * b) * c) :~: ((b + (a * b)) * c)
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (('S a * b) * c) :~: ((b + (a * b)) * c)
r2 Any a
a Any b
b Any c
c (((b + (a * b)) * c) :~: ((b + (a * b)) * c))
-> (((b + (a * b)) * c) :~: ((b * c) + ((a * b) * c)))
-> ((b + (a * b)) * c) :~: ((b * c) + ((a * b) * c))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a
-> Any b
-> Any c
-> ((b + (a * b)) * c) :~: ((b * c) + ((a * b) * c))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + (a * b)) * c) :~: ((b * c) + ((a * b) * c))
r3 Any a
a Any b
b Any c
c (((b + (a * b)) * c) :~: ((b * c) + ((a * b) * c)))
-> (((b * c) + ((a * b) * c)) :~: ((b * c) + (a * (b * c))))
-> ((b + (a * b)) * c) :~: ((b * c) + (a * (b * c)))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a
-> Any b
-> Any c
-> ((b * c) + ((a * b) * c)) :~: ((b * c) + (a * (b * c)))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b * c) + ((a * b) * c)) :~: ((b * c) + (a * (b * c)))
hyp Any a
a Any b
b Any c
c (((b + (a * b)) * c) :~: ((b * c) + (a * (b * c))))
-> (((b * c) + (a * (b * c))) :~: ((b * c) + (a * (b * c))))
-> ((b + (a * b)) * c) :~: ((b * c) + (a * (b * c)))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a
-> Any b -> Any c -> ((b * c) + (a * (b * c))) :~: ('S a * (b * c))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> ((b * c) + (a * (b * c))) :~: ('S a * (b * c))
r4 Any a
a Any b
b Any c
c (((b + (a * b)) * c) :~: ((b * c) + (a * (b * c))))
-> (((b * c) + (a * (b * c))) :~: ((b * c) + (a * (b * c))))
-> ((b + (a * b)) * c) :~: ((b * c) + (a * (b * c)))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> Any c -> ('S a * (b * c)) :~: ((a + 1) * (b * c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S a * (b * c)) :~: ((a + 1) * (b * c))
r5 Any a
a Any b
b Any c
c

  r1  :: Any a -> Any b -> Any c -> ((a+1)*b)*c   :~: (S a * b)*c
  r2  :: Any a -> Any b -> Any c -> (S a * b)*c   :~: (b + a*b)*c 
  r3  :: Any a -> Any b -> Any c -> (b + a*b)*c   :~: b*c + (a*b)*c
  hyp :: Any a -> Any b -> Any c -> b*c + (a*b)*c :~: b*c + a*(b*c)
  r4  :: Any a -> Any b -> Any c -> b*c + a*(b*c) :~: S a * (b*c)
  r5  :: Any a -> Any b -> Any c -> S a * (b*c)   :~: (a+1)*(b*c)

  r1 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (((a + 1) * b) * c) :~: (('S a * b) * c)
r1  Any a
_ Any b
_ Any c
_ = (((a + 1) * b) * c) :~: (('S a * b) * c)
((b + (a * b)) * c) :~: ((b + (a * b)) * c)
forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (('S a * b) * c) :~: ((b + (a * b)) * c)
r2  Any a
_ Any b
_ Any c
_ = (('S a * b) * c) :~: ((b + (a * b)) * c)
((b + (a * b)) * c) :~: ((b + (a * b)) * c)
forall {k} (a :: k). a :~: a
Refl
  r3 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + (a * b)) * c) :~: ((b * c) + ((a * b) * c))
r3  Any a
a Any b
b Any c
c = Any b
-> Any (a * b)
-> Any c
-> ((b + (a * b)) * c) :~: ((b * c) + ((a * b) * c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) * c) :~: ((a * c) + (b * c))
prpDstrL Any b
b (Any a
aAny a -> Any b -> Any (a * b)
forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any b
b) Any c
c
  hyp :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b * c) + ((a * b) * c)) :~: ((b * c) + (a * (b * c)))
hyp Any a
a Any b
b Any c
c = ((b * c) :~: (b * c))
-> (((a * b) * c) :~: (a * (b * c)))
-> ((b * c) + ((a * b) * c)) :~: ((b * c) + (a * (b * c)))
forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (Any (b * c) -> (b * c) :~: (b * c)
forall (x :: N'). Any x -> x :~: x
refl (Any b
bAny b -> Any c -> Any (b * c)
forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any c
c)) (Any a -> Any b -> Any c -> ((a * b) * c) :~: (a * (b * c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a * b) * c) :~: (a * (b * c))
prpMltAssoc Any a
a Any b
b Any c
c)
  r4 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> ((b * c) + (a * (b * c))) :~: ('S a * (b * c))
r4  Any a
_ Any b
_ Any c
_ = ((b * c) + (a * (b * c))) :~: ('S a * (b * c))
((b * c) + (a * (b * c))) :~: ((b * c) + (a * (b * c)))
forall {k} (a :: k). a :~: a
Refl
  r5 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S a * (b * c)) :~: ((a + 1) * (b * c))
r5  Any a
_ Any b
_ Any c
_ = ('S a * (b * c)) :~: ((a + 1) * (b * c))
((b * c) + (a * (b * c))) :~: ((b * c) + (a * (b * c)))
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- lemmaMlt1 -

-- | right multiplication of t'N0' is t'N0'.
lemmaMlt1 :: Any a -> a*N0 :~: N0

-- anchoring -
lemmaMlt1 :: forall (a :: N'). Any a -> (a * N0) :~: N0
lemmaMlt1 W a
W0 = (a * N0) :~: N0
N0 :~: N0
forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
lemmaMlt1 (SW W n
a) = W n -> ((n + 1) * N0) :~: N0
forall (a :: N'). Any a -> ((a + 1) * N0) :~: N0
qed W n
a where
  qed :: Any a -> (a+1)*N0 :~: N0
  qed :: forall (a :: N'). Any a -> ((a + 1) * N0) :~: N0
qed Any a
a = Any a -> ((a + 1) * N0) :~: ('S a * N0)
forall (a :: N'). Any a -> ((a + 1) * N0) :~: ('S a * N0)
r1 Any a
a ((a * N0) :~: (a * N0))
-> ((a * N0) :~: (a * N0)) -> (a * N0) :~: (a * N0)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> ('S a * N0) :~: (N0 + (a * N0))
forall (a :: N'). Any a -> ('S a * N0) :~: (N0 + (a * N0))
r2 Any a
a ((a * N0) :~: (a * N0))
-> ((a * N0) :~: (a * N0)) -> (a * N0) :~: (a * N0)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> (N0 + (a * N0)) :~: (a * N0)
forall (a :: N'). Any a -> (N0 + (a * N0)) :~: (a * N0)
r3 Any a
a ((a * N0) :~: (a * N0)) -> ((a * N0) :~: N0) -> (a * N0) :~: N0
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> (a * N0) :~: N0
forall (a :: N'). Any a -> (a * N0) :~: N0
hyp Any a
a

  r1  :: Any a -> (a+1)*N0  :~: (S a)*N0
  r2  :: Any a -> (S a)*N0  :~: N0 + a*N0
  r3  :: Any a -> N0 + a*N0 :~: a*N0
  hyp :: Any a -> a*N0      :~: N0

  r1 :: forall (a :: N'). Any a -> ((a + 1) * N0) :~: ('S a * N0)
r1  Any a
_ = (a * N0) :~: (a * N0)
((a + 1) * N0) :~: ('S a * N0)
forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N'). Any a -> ('S a * N0) :~: (N0 + (a * N0))
r2  Any a
_ = (a * N0) :~: (a * N0)
('S a * N0) :~: (N0 + (a * N0))
forall {k} (a :: k). a :~: a
Refl
  r3 :: forall (a :: N'). Any a -> (N0 + (a * N0)) :~: (a * N0)
r3  Any a
_ = (a * N0) :~: (a * N0)
(N0 + (a * N0)) :~: (a * N0)
forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N'). Any a -> (a * N0) :~: N0
hyp Any a
a = Any a -> (a * N0) :~: N0
forall (a :: N'). Any a -> (a * N0) :~: N0
lemmaMlt1 Any a
a

--------------------------------------------------------------------------------
-- lemmaAdd2 -

-- | lemma 2 for addition.
lemmaAdd2 :: Any a -> Any b -> Any c -> a + b + c :~: b + a + c
lemmaAdd2 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a + (b + c)) :~: (b + (a + c))
lemmaAdd2 Any a
a Any b
b Any c
c = Any a -> Any b -> Any c -> (a + (b + c)) :~: (b + (a + c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a + (b + c)) :~: (b + (a + c))
qed Any a
a Any b
b Any c
c where
  qed :: Any a -> Any b -> Any c -> a + b + c :~: b + a + c
  qed :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a + (b + c)) :~: (b + (a + c))
qed Any a
a Any b
b Any c
c = Any a -> Any b -> Any c -> (a + (b + c)) :~: ((a + b) + c)
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a + (b + c)) :~: ((a + b) + c)
r1 Any a
a Any b
b Any c
c ((a + (b + c)) :~: ((a + b) + c))
-> (((a + b) + c) :~: ((b + a) + c))
-> (a + (b + c)) :~: ((b + a) + c)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> Any c -> ((a + b) + c) :~: ((b + a) + c)
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: ((b + a) + c)
r2 Any a
a Any b
b Any c
c ((a + (b + c)) :~: ((b + a) + c))
-> (((b + a) + c) :~: (b + (a + c)))
-> (a + (b + c)) :~: (b + (a + c))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> Any c -> ((b + a) + c) :~: (b + (a + c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((b + a) + c) :~: (b + (a + c))
r3 Any a
a Any b
b Any c
c

  r1 :: Any a -> Any b -> Any c -> a + b + c   :~: (a + b) + c
  r2 :: Any a -> Any b -> Any c -> (a + b) + c :~: (b + a) + c
  r3 :: Any a -> Any b -> Any c -> (b + a) + c :~: b + a + c

  r1 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a + (b + c)) :~: ((a + b) + c)
r1 Any a
a Any b
b Any c
c = (((a + b) + c) :~: (a + (b + c)))
-> (a + (b + c)) :~: ((a + b) + c)
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((((a + b) + c) :~: (a + (b + c)))
 -> (a + (b + c)) :~: ((a + b) + c))
-> (((a + b) + c) :~: (a + (b + c)))
-> (a + (b + c)) :~: ((a + b) + c)
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc Any a
a Any b
b Any c
c
  r2 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: ((b + a) + c)
r2 Any a
a Any b
b Any c
c = ((a + b) :~: (b + a))
-> (c :~: c) -> ((a + b) + c) :~: ((b + a) + c)
forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (Any a -> Any b -> (a + b) :~: (b + a)
forall (a :: N') (b :: N'). Any a -> Any b -> (a + b) :~: (b + a)
prpAddComm Any a
a Any b
b) (Any c -> c :~: c
forall (x :: N'). Any x -> x :~: x
refl Any c
c)
  r3 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((b + a) + c) :~: (b + (a + c))
r3 Any a
a Any b
b Any c
c = Any b -> Any a -> Any c -> ((b + a) + c) :~: (b + (a + c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc Any b
b Any a
a Any c
c

--------------------------------------------------------------------------------
-- prpDstrR -

-- | law of right distributivity holds.
prpDstrR :: Any a -> Any b -> Any c -> a*(b + c) :~: a*b + a*c

-- anchoring -
prpDstrR :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a * (b + c)) :~: ((a * b) + (a * c))
prpDstrR W a
W0 Any b
_ Any c
_ = (a * (b + c)) :~: ((a * b) + (a * c))
N0 :~: N0
forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
prpDstrR (SW W n
a) Any b
b Any c
c = W n
-> Any b
-> Any c
-> ((n + 1) * (b + c)) :~: (((n + 1) * b) + ((n + 1) * c))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((a + 1) * (b + c)) :~: (((a + 1) * b) + ((a + 1) * c))
qed W n
a Any b
b Any c
c where
  qed :: Any a -> Any b -> Any c -> (a+1)*(b + c) :~: (a+1)*b + (a+1)*c
  qed :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((a + 1) * (b + c)) :~: (((a + 1) * b) + ((a + 1) * c))
qed Any a
a Any b
b Any c
c = Any a -> Any b -> Any c -> ((a + 1) * (b + c)) :~: ('S a * (b + c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + 1) * (b + c)) :~: ('S a * (b + c))
r1 Any a
a Any b
b Any c
c (((b + c) + (a * (b + c))) :~: ((b + c) + (a * (b + c))))
-> (((b + c) + (a * (b + c))) :~: ((b + c) + (a * (b + c))))
-> ((b + c) + (a * (b + c))) :~: ((b + c) + (a * (b + c)))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a
-> Any b -> Any c -> ('S a * (b + c)) :~: ((b + c) + (a * (b + c)))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> ('S a * (b + c)) :~: ((b + c) + (a * (b + c)))
r2 Any a
a Any b
b Any c
c (((b + c) + (a * (b + c))) :~: ((b + c) + (a * (b + c))))
-> (((b + c) + (a * (b + c))) :~: ((b + c) + ((a * b) + (a * c))))
-> ((b + c) + (a * (b + c))) :~: ((b + c) + ((a * b) + (a * c)))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a
-> Any b
-> Any c
-> ((b + c) + (a * (b + c))) :~: ((b + c) + ((a * b) + (a * c)))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + c) + (a * (b + c))) :~: ((b + c) + ((a * b) + (a * c)))
hyp Any a
a Any b
b Any c
c (((b + c) + (a * (b + c))) :~: ((b + c) + ((a * b) + (a * c))))
-> (((b + c) + ((a * b) + (a * c)))
    :~: (b + (c + ((a * b) + (a * c)))))
-> ((b + c) + (a * (b + c))) :~: (b + (c + ((a * b) + (a * c))))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a
-> Any b
-> Any c
-> ((b + c) + ((a * b) + (a * c)))
   :~: (b + (c + ((a * b) + (a * c))))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + c) + ((a * b) + (a * c)))
   :~: (b + (c + ((a * b) + (a * c))))
r3 Any a
a Any b
b Any c
c (((b + c) + (a * (b + c))) :~: (b + (c + ((a * b) + (a * c)))))
-> ((b + (c + ((a * b) + (a * c))))
    :~: (b + ((a * b) + (c + (a * c)))))
-> ((b + c) + (a * (b + c))) :~: (b + ((a * b) + (c + (a * c))))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a
-> Any b
-> Any c
-> (b + (c + ((a * b) + (a * c))))
   :~: (b + ((a * b) + (c + (a * c))))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (b + (c + ((a * b) + (a * c))))
   :~: (b + ((a * b) + (c + (a * c))))
r4 Any a
a Any b
b Any c
c
           (((b + c) + (a * (b + c))) :~: (b + ((a * b) + (c + (a * c)))))
-> ((b + ((a * b) + (c + (a * c))))
    :~: ((b + (a * b)) + (c + (a * c))))
-> ((b + c) + (a * (b + c))) :~: ((b + (a * b)) + (c + (a * c)))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a
-> Any b
-> Any c
-> (b + ((a * b) + (c + (a * c))))
   :~: ((b + (a * b)) + (c + (a * c)))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (b + ((a * b) + (c + (a * c))))
   :~: ((b + (a * b)) + (c + (a * c)))
r5 Any a
a Any b
b Any c
c (((b + c) + (a * (b + c))) :~: ((b + (a * b)) + (c + (a * c))))
-> (((b + (a * b)) + (c + (a * c)))
    :~: ((b + (a * b)) + (c + (a * c))))
-> ((b + c) + (a * (b + c))) :~: ((b + (a * b)) + (c + (a * c)))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a
-> Any b
-> Any c
-> ((b + (a * b)) + (c + (a * c))) :~: (('S a * b) + ('S a * c))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + (a * b)) + (c + (a * c))) :~: (('S a * b) + ('S a * c))
r6 Any a
a Any b
b Any c
c (((b + c) + (a * (b + c))) :~: ((b + (a * b)) + (c + (a * c))))
-> (((b + (a * b)) + (c + (a * c)))
    :~: ((b + (a * b)) + (c + (a * c))))
-> ((b + c) + (a * (b + c))) :~: ((b + (a * b)) + (c + (a * c)))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a
-> Any b
-> Any c
-> (('S a * b) + ('S a * c)) :~: (((a + 1) * b) + ((a + 1) * c))
forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (('S a * b) + ('S a * c)) :~: (((a + 1) * b) + ((a + 1) * c))
r7 Any a
a Any b
b Any c
c

  r1  :: Any a -> Any b -> Any c -> (a+1)*(b + c)          :~: S a * (b + c)
  r2  :: Any a -> Any b -> Any c -> S a * (b + c)          :~: (b + c) + a*(b + c) 
  hyp :: Any a -> Any b -> Any c -> (b + c) + a*(b + c)    :~: (b + c) + (a*b + a*c)
  r3  :: Any a -> Any b -> Any c -> (b + c) + (a*b + a*c)  :~: b + c + a*b + a*c  
  r4  :: Any a -> Any b -> Any c ->  b + c + a*b + a*c     :~: b + a*b + c + a*c
  r5  :: Any a -> Any b -> Any c ->  b + a*b + c + a*c     :~: (b + a*b) + (c + a*c) 
  r6  :: Any a -> Any b -> Any c ->  (b + a*b) + (c + a*c) :~: (S a)*b + (S a)*c
  r7  :: Any a -> Any b -> Any c ->  (S a)*b + (S a)*c     :~: (a+1)*b + (a+1)*c

  r1 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + 1) * (b + c)) :~: ('S a * (b + c))
r1  Any a
_ Any b
_ Any c
_ = ((a + 1) * (b + c)) :~: ('S a * (b + c))
((b + c) + (a * (b + c))) :~: ((b + c) + (a * (b + c)))
forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> ('S a * (b + c)) :~: ((b + c) + (a * (b + c)))
r2  Any a
_ Any b
_ Any c
_ = ('S a * (b + c)) :~: ((b + c) + (a * (b + c)))
((b + c) + (a * (b + c))) :~: ((b + c) + (a * (b + c)))
forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + c) + (a * (b + c))) :~: ((b + c) + ((a * b) + (a * c)))
hyp Any a
a Any b
b Any c
c = ((b + c) :~: (b + c))
-> ((a * (b + c)) :~: ((a * b) + (a * c)))
-> ((b + c) + (a * (b + c))) :~: ((b + c) + ((a * b) + (a * c)))
forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (Any (b + c) -> (b + c) :~: (b + c)
forall (x :: N'). Any x -> x :~: x
refl (Any b
bAny b -> Any c -> Any (b + c)
forall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++Any c
c)) (Any a -> Any b -> Any c -> (a * (b + c)) :~: ((a * b) + (a * c))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a * (b + c)) :~: ((a * b) + (a * c))
prpDstrR Any a
a Any b
b Any c
c) 
  r3 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + c) + ((a * b) + (a * c)))
   :~: (b + (c + ((a * b) + (a * c))))
r3  Any a
a Any b
b Any c
c = Any b
-> Any c
-> Any ((a * b) + (a * c))
-> ((b + c) + ((a * b) + (a * c)))
   :~: (b + (c + ((a * b) + (a * c))))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc Any b
b Any c
c (Any a
aAny a -> Any b -> W (a * b)
forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any b
b W (a * b) -> W (a * c) -> Any ((a * b) + (a * c))
forall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++ Any a
aAny a -> Any c -> W (a * c)
forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any c
c)
  r4 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (b + (c + ((a * b) + (a * c))))
   :~: (b + ((a * b) + (c + (a * c))))
r4  Any a
a Any b
b Any c
c = (b :~: b)
-> ((c + ((a * b) + (a * c))) :~: ((a * b) + (c + (a * c))))
-> (b + (c + ((a * b) + (a * c))))
   :~: (b + ((a * b) + (c + (a * c))))
forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (Any b -> b :~: b
forall (x :: N'). Any x -> x :~: x
refl Any b
b) (((c + ((a * b) + (a * c))) :~: ((a * b) + (c + (a * c))))
 -> (b + (c + ((a * b) + (a * c))))
    :~: (b + ((a * b) + (c + (a * c)))))
-> ((c + ((a * b) + (a * c))) :~: ((a * b) + (c + (a * c))))
-> (b + (c + ((a * b) + (a * c))))
   :~: (b + ((a * b) + (c + (a * c))))
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any c
-> Any (a * b)
-> Any (a * c)
-> (c + ((a * b) + (a * c))) :~: ((a * b) + (c + (a * c)))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a + (b + c)) :~: (b + (a + c))
lemmaAdd2 Any c
c (Any a
aAny a -> Any b -> Any (a * b)
forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any b
b) (Any a
aAny a -> Any c -> Any (a * c)
forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any c
c)
  r5 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (b + ((a * b) + (c + (a * c))))
   :~: ((b + (a * b)) + (c + (a * c)))
r5  Any a
a Any b
b Any c
c = (((b + (a * b)) + (c + (a * c)))
 :~: (b + ((a * b) + (c + (a * c)))))
-> (b + ((a * b) + (c + (a * c))))
   :~: ((b + (a * b)) + (c + (a * c)))
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((((b + (a * b)) + (c + (a * c)))
  :~: (b + ((a * b) + (c + (a * c)))))
 -> (b + ((a * b) + (c + (a * c))))
    :~: ((b + (a * b)) + (c + (a * c))))
-> (((b + (a * b)) + (c + (a * c)))
    :~: (b + ((a * b) + (c + (a * c)))))
-> (b + ((a * b) + (c + (a * c))))
   :~: ((b + (a * b)) + (c + (a * c)))
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any b
-> Any (a * b)
-> Any (c + (a * c))
-> ((b + (a * b)) + (c + (a * c)))
   :~: (b + ((a * b) + (c + (a * c))))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc Any b
b (Any a
aAny a -> Any b -> Any (a * b)
forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any b
b) (Any c
c Any c -> W (a * c) -> Any (c + (a * c))
forall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++ Any a
aAny a -> Any c -> W (a * c)
forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any c
c)
  r6 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + (a * b)) + (c + (a * c))) :~: (('S a * b) + ('S a * c))
r6  Any a
_ Any b
_ Any c
_ = ((b + (a * b)) + (c + (a * c))) :~: (('S a * b) + ('S a * c))
((b + (a * b)) + (c + (a * c))) :~: ((b + (a * b)) + (c + (a * c)))
forall {k} (a :: k). a :~: a
Refl
  r7 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (('S a * b) + ('S a * c)) :~: (((a + 1) * b) + ((a + 1) * c))
r7  Any a
_ Any b
_ Any c
_ = (('S a * b) + ('S a * c)) :~: (((a + 1) * b) + ((a + 1) * c))
((b + (a * b)) + (c + (a * c))) :~: ((b + (a * b)) + (c + (a * c)))
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpMltComm -

-- | multiplication is commutative.
prpMltComm :: Any a -> Any b -> a*b :~: b*a

-- anchoring -
prpMltComm :: forall (a :: N') (b :: N'). Any a -> Any b -> (a * b) :~: (b * a)
prpMltComm W a
W0 Any b
b = Any b -> (N0 * b) :~: (b * N0)
forall (b :: N'). Any b -> (N0 * b) :~: (b * N0)
qed Any b
b where
  qed :: Any b -> N0 * b :~: b * N0
  qed :: forall (b :: N'). Any b -> (N0 * b) :~: (b * N0)
qed Any b
b = Any b -> (N0 * b) :~: N0
forall (b :: N'). Any b -> (N0 * b) :~: N0
r1 Any b
b (N0 :~: N0) -> (N0 :~: (b * N0)) -> N0 :~: (b * N0)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any b -> N0 :~: (b * N0)
forall (b :: N'). Any b -> N0 :~: (b * N0)
r2 Any b
b

  r1  :: Any b -> N0 * b :~: N0
  r2  :: Any b -> N0     :~: b * N0

  r1 :: forall (b :: N'). Any b -> (N0 * b) :~: N0
r1 Any b
_ = (N0 * b) :~: N0
N0 :~: N0
forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (b :: N'). Any b -> N0 :~: (b * N0)
r2 Any b
b = ((b * N0) :~: N0) -> N0 :~: (b * N0)
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (((b * N0) :~: N0) -> N0 :~: (b * N0))
-> ((b * N0) :~: N0) -> N0 :~: (b * N0)
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any b -> (b * N0) :~: N0
forall (a :: N'). Any a -> (a * N0) :~: N0
lemmaMlt1 Any b
b

-- hypothesis -
prpMltComm (SW W n
a) Any b
b = W n -> Any b -> ((n + 1) * b) :~: (b * (n + 1))
forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) * b) :~: (b * (a + 1))
qed W n
a Any b
b where
  qed :: Any a -> Any b -> (a+1)*b :~: b*(a+1)
  qed :: forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) * b) :~: (b * (a + 1))
qed Any a
a Any b
b =  Any a -> Any b -> ((a + 1) * b) :~: ('S a * b)
forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) * b) :~: ('S a * b)
r1 Any a
a Any b
b ((b + (a * b)) :~: (b + (a * b)))
-> ((b + (a * b)) :~: (b + (a * b)))
-> (b + (a * b)) :~: (b + (a * b))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> ('S a * b) :~: (b + (a * b))
forall (a :: N') (b :: N').
Any a -> Any b -> ('S a * b) :~: (b + (a * b))
r2 Any a
a Any b
b ((b + (a * b)) :~: (b + (a * b)))
-> ((b + (a * b)) :~: (b + (b * a)))
-> (b + (a * b)) :~: (b + (b * a))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> (b + (a * b)) :~: (b + (b * a))
forall (a :: N') (b :: N').
Any a -> Any b -> (b + (a * b)) :~: (b + (b * a))
hyp Any a
a Any b
b ((b + (a * b)) :~: (b + (b * a)))
-> ((b + (b * a)) :~: ((b * N1) + (b * a)))
-> (b + (a * b)) :~: ((b * N1) + (b * a))
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> (b + (b * a)) :~: ((b * N1) + (b * a))
forall (a :: N') (b :: N').
Any a -> Any b -> (b + (b * a)) :~: ((b * N1) + (b * a))
r3 Any a
a Any b
b ((b + (a * b)) :~: ((b * N1) + (b * a)))
-> (((b * N1) + (b * a)) :~: (b * 'S a))
-> (b + (a * b)) :~: (b * 'S a)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> ((b * N1) + (b * a)) :~: (b * (N1 + a))
forall (a :: N') (b :: N').
Any a -> Any b -> ((b * N1) + (b * a)) :~: (b * (N1 + a))
r4 Any a
a Any b
b
          ((b + (a * b)) :~: (b * 'S a))
-> ((b * 'S a) :~: (b * 'S a)) -> (b + (a * b)) :~: (b * 'S a)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> (b * (N1 + a)) :~: (b * (N1 + a))
forall (a :: N') (b :: N').
Any a -> Any b -> (b * (N1 + a)) :~: (b * (N1 + a))
r5 Any a
a Any b
b ((b + (a * b)) :~: (b * 'S a))
-> ((b * 'S a) :~: (b * 'S a)) -> (b + (a * b)) :~: (b * 'S a)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> (b * (N1 + a)) :~: (b * 'S (N0 + a))
forall (a :: N') (b :: N').
Any a -> Any b -> (b * (N1 + a)) :~: (b * 'S (N0 + a))
r6 Any a
a Any b
b ((b + (a * b)) :~: (b * 'S a))
-> ((b * 'S a) :~: (b * 'S a)) -> (b + (a * b)) :~: (b * 'S a)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> (b * 'S (N0 + a)) :~: (b * 'S a)
forall (a :: N') (b :: N').
Any a -> Any b -> (b * 'S (N0 + a)) :~: (b * 'S a)
r7 Any a
a Any b
b ((b + (a * b)) :~: (b * 'S a))
-> ((b * 'S a) :~: (b * 'S a)) -> (b + (a * b)) :~: (b * 'S a)
forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> Any a -> Any b -> (b * 'S a) :~: (b * (a + 1))
forall (a :: N') (b :: N').
Any a -> Any b -> (b * 'S a) :~: (b * (a + 1))
r8 Any a
a Any b
b

  r1  :: Any a -> Any b -> (a+1)*b        :~: (S a) * b
  r2  :: Any a -> Any b -> (S a) * b      :~: b + a*b
  hyp :: Any a -> Any b -> b + a*b        :~: b + b*a
  r3  :: Any a -> Any b -> b + b*a        :~: b*N1 + b*a
  r4  :: Any a -> Any b -> b*N1 + b*a     :~: b*(N1 + a)
  r5  :: Any a -> Any b -> b*(N1 + a)     :~: b*(S N0 + a)
  r6  :: Any a -> Any b -> b*(S N0 + a)   :~: b*(S (N0 + a))
  r7  :: Any a -> Any b -> b*(S (N0 + a)) :~: b*(S a) 
  r8  :: Any a -> Any b -> b*(S a)        :~: b*(a+1)

  r1 :: forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) * b) :~: ('S a * b)
r1  Any a
_ Any b
_ = ((a + 1) * b) :~: ('S a * b)
(b + (a * b)) :~: (b + (a * b))
forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S a * b) :~: (b + (a * b))
r2  Any a
_ Any b
_ = ('S a * b) :~: (b + (a * b))
(b + (a * b)) :~: (b + (a * b))
forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N') (b :: N').
Any a -> Any b -> (b + (a * b)) :~: (b + (b * a))
hyp Any a
a Any b
b = (b :~: b)
-> ((a * b) :~: (b * a)) -> (b + (a * b)) :~: (b + (b * a))
forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (Any b -> b :~: b
forall (x :: N'). Any x -> x :~: x
refl Any b
b) (Any a -> Any b -> (a * b) :~: (b * a)
forall (a :: N') (b :: N'). Any a -> Any b -> (a * b) :~: (b * a)
prpMltComm Any a
a Any b
b)
  r3 :: forall (a :: N') (b :: N').
Any a -> Any b -> (b + (b * a)) :~: ((b * N1) + (b * a))
r3  Any a
a Any b
b = (b :~: (b * N1))
-> ((b * a) :~: (b * a)) -> (b + (b * a)) :~: ((b * N1) + (b * a))
forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (((b * N1) :~: b) -> b :~: (b * N1)
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (((b * N1) :~: b) -> b :~: (b * N1))
-> ((b * N1) :~: b) -> b :~: (b * N1)
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any b -> (b * N1) :~: b
forall (a :: N'). Any a -> (a * N1) :~: a
prpMltNtrlR Any b
b) (Any (b * a) -> (b * a) :~: (b * a)
forall (x :: N'). Any x -> x :~: x
refl (Any b
bAny b -> Any a -> Any (b * a)
forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any a
a))
  r4 :: forall (a :: N') (b :: N').
Any a -> Any b -> ((b * N1) + (b * a)) :~: (b * (N1 + a))
r4  Any a
a Any b
b = ((b * 'S a) :~: ((b * N1) + (b * a)))
-> ((b * N1) + (b * a)) :~: (b * 'S a)
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (((b * 'S a) :~: ((b * N1) + (b * a)))
 -> ((b * N1) + (b * a)) :~: (b * 'S a))
-> ((b * 'S a) :~: ((b * N1) + (b * a)))
-> ((b * N1) + (b * a)) :~: (b * 'S a)
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any b -> Any N1 -> Any a -> (b * (N1 + a)) :~: ((b * N1) + (b * a))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a * (b + c)) :~: ((a * b) + (a * c))
prpDstrR Any b
b Any N1
w1 Any a
a 
  r5 :: forall (a :: N') (b :: N').
Any a -> Any b -> (b * (N1 + a)) :~: (b * (N1 + a))
r5  Any a
_ Any b
_ = (b * (N1 + a)) :~: (b * (N1 + a))
(b * 'S a) :~: (b * 'S a)
forall {k} (a :: k). a :~: a
Refl
  r6 :: forall (a :: N') (b :: N').
Any a -> Any b -> (b * (N1 + a)) :~: (b * 'S (N0 + a))
r6  Any a
_ Any b
_ = (b * (N1 + a)) :~: (b * 'S (N0 + a))
(b * 'S a) :~: (b * 'S a)
forall {k} (a :: k). a :~: a
Refl
  r7 :: forall (a :: N') (b :: N').
Any a -> Any b -> (b * 'S (N0 + a)) :~: (b * 'S a)
r7  Any a
_ Any b
_ = (b * 'S a) :~: (b * 'S a)
(b * 'S (N0 + a)) :~: (b * 'S a)
forall {k} (a :: k). a :~: a
Refl
  r8 :: forall (a :: N') (b :: N').
Any a -> Any b -> (b * 'S a) :~: (b * (a + 1))
r8  Any a
_ Any b
_ = (b * 'S a) :~: (b * (a + 1))
(b * 'S a) :~: (b * 'S a)
forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- codeW -

-- | @codeW n m@ generates the haskell code for the witnesses 'W' of 'N'' from @n@ to @m@.
codeW :: N -> N -> String
codeW :: N -> N -> String
codeW N
i N
n = [String] -> String
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join ([String] -> String) -> [String] -> String
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
tween String
"\n" ([String] -> [String]) -> [String] -> [String]
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ N -> [String]
cdn N
i where
  cdn :: N -> [String]
cdn N
0 = String
"type N0 = 'N0"
        String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
"w0 :: W N0"
        String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
"w0 = W0"
        String -> [String] -> [String]
forall a. a -> [a] -> [a]
: N -> [String]
cdn N
1
  cdn N
i | N
i N -> N -> Bool
forall a. Ord a => a -> a -> Bool
<= N
n    = String
cdType String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
cdDcl String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
cdDef String -> [String] -> [String]
forall a. a -> [a] -> [a]
: N -> [String]
cdn (N
i N -> N -> N
forall a. Additive a => a -> a -> a
+ N
1)
        | Bool
otherwise = []
    where i' :: N
i' = N
iN -> N -> N
>-N
1
          ++ :: [a] -> [a] -> [a]
(++) = [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(L.++)
          cdType :: String
cdType = String
"type N" String -> ShowS
forall a. [a] -> [a] -> [a]
++ N -> String
forall a. Show a => a -> String
show N
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = S N" String -> ShowS
forall a. [a] -> [a] -> [a]
++ N -> String
forall a. Show a => a -> String
show N
i'
          cdDcl :: String
cdDcl  = String
"w" String -> ShowS
forall a. [a] -> [a] -> [a]
++ N -> String
forall a. Show a => a -> String
show N
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: W N" String -> ShowS
forall a. [a] -> [a] -> [a]
++ N -> String
forall a. Show a => a -> String
show N
i
          cdDef :: String
cdDef  = String
"w" String -> ShowS
forall a. [a] -> [a] -> [a]
++ N -> String
forall a. Show a => a -> String
show N
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = SW " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"w" String -> ShowS
forall a. [a] -> [a] -> [a]
++ N -> String
forall a. Show a => a -> String
show N
i'  

--------------------------------------------------------------------------------
-- itfW -

-- | @itfW n m@ generates the haskell interface for the witnesses 'W' from @n@ to @m@.
itfW :: N -> N -> String
itfW :: N -> N -> String
itfW N
n N
m = [String] -> String
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join ([String] -> String) -> [String] -> String
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
tween String
"\n" ([String] -> [String]) -> [String] -> [String]
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ ([String] -> String) -> [[String]] -> [String]
forall a b. (a -> b) -> [a] -> [b]
L.map [String] -> String
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join ([[String]] -> [String]) -> [[String]] -> [String]
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ [String] -> [[String]]
forall {a}. [a] -> [[a]]
splt [String]
nats where
  ++ :: [a] -> [a] -> [a]
(++) = [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(L.++)
  nats :: [String]
nats = [String
", type N" String -> ShowS
forall a. [a] -> [a] -> [a]
++ N -> String
forall a. Show a => a -> String
show N
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", w" String -> ShowS
forall a. [a] -> [a] -> [a]
++ N -> String
forall a. Show a => a -> String
show N
i | N
i <- [N
n..N
m]]
  splt :: [a] -> [[a]]
splt [] = []
  splt [a]
ss = [a]
s [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [a] -> [[a]]
splt [a]
ss' where
    ([a]
s,[a]
ss') = Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
L.splitAt Int
4 [a]
ss

--------------------------------------------------------------------------------
-- (:<=:) -

infix 4 :<=:
  
-- | ordering relation for naturals 'N''.
data n :<=: m where
  Add :: Any n -> Any d -> n :<=: (n + d)

instance Show (n :<=: m) where
  show :: (n :<=: m) -> String
show (Add Any n
n Any d
d) = [String] -> String
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join [Any n -> String
forall a. Show a => a -> String
show Any n
n,String
" <= ",W m -> String
forall a. Show a => a -> String
show (Any n
nAny n -> Any d -> W (n + d)
forall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++Any d
d)]

--------------------------------------------------------------------------------
-- nodAnyFst -

-- | the induced witness of the first component.
nodAnyFst :: i :<=: n -> Any i
nodAnyFst :: forall (i :: N') (n :: N'). (i :<=: n) -> Any i
nodAnyFst (Add Any i
i Any d
_) = Any i
i

--------------------------------------------------------------------------------
-- nodAnySnd -

-- | the induced witness of the second component.
nodAnySnd :: i :<=: n -> Any n
nodAnySnd :: forall (i :: N') (n :: N'). (i :<=: n) -> Any n
nodAnySnd (Add Any i
i Any d
d) = Any i
iAny i -> Any d -> W (i + d)
forall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++Any d
d

--------------------------------------------------------------------------------
-- nodRefl -

-- | for any @__n__@ holds that @(':<=:')@ is reflexive.
nodRefl :: Any n -> n :<=: n
nodRefl :: forall (n :: N'). Any n -> n :<=: n
nodRefl Any n
n = case Any n -> (n + N0) :~: n
forall (a :: N'). Any a -> (a + N0) :~: a
prpAddNtrlR Any n
n of (n + N0) :~: n
Refl -> Any n -> W N0 -> n :<=: (n + N0)
forall (n :: N') (d :: N'). Any n -> W d -> n :<=: (n + d)
Add Any n
n W N0
W0

--------------------------------------------------------------------------------
-- nodPred -

-- | if @__n__ t'+' __1__@ is smaler or equal to @__m__@ then @__n__@ is also smaler of equal
-- to @__m__@.
nodPred :: n + 1 :<=: m -> n :<=: m
nodPred :: forall (n :: N') (m :: N'). ((n + 1) :<=: m) -> n :<=: m
nodPred (Add (SW W n
n) Any d
d) = case W n -> Any d -> (n + 'S d) :~: 'S (n + d)
forall (n :: N') (d :: N').
Any n -> Any d -> (n + 'S d) :~: 'S (n + d)
lemma1 W n
n Any d
d of (n + 'S d) :~: 'S (n + d)
Refl -> Any n -> Any ('S d) -> n :<=: (n + 'S d)
forall (n :: N') (d :: N'). Any n -> W d -> n :<=: (n + d)
Add Any n
W n
n (Any d -> W (d + 1)
forall (d :: N'). W d -> W (d + 1)
SW Any d
d)
  where

    lemma1 :: Any n -> Any d -> (n + S d) :~: S (n + d)
    lemma1 :: forall (n :: N') (d :: N').
Any n -> Any d -> (n + 'S d) :~: 'S (n + d)
lemma1 Any n
n Any d
d = ((n + (d + N1)) :~: ((n + d) + N1))
-> ((n + (d + N1)) :~: (n + 'S d))
-> (((n + d) + N1) :~: 'S (n + d))
-> (n + 'S d) :~: 'S (n + d)
forall {k} (a :: k) (b :: k) (a' :: k) (b' :: k).
(a :~: b) -> (a :~: a') -> (b :~: b') -> a' :~: b'
lemma6 (Any n -> Any d -> (n + (d + N1)) :~: ((n + d) + N1)
forall (n :: N') (d :: N').
Any n -> Any d -> (n + (d + N1)) :~: ((n + d) + N1)
lemma5 Any n
n Any d
d) (((n + 'S d) :~: (n + (d + N1))) -> (n + (d + N1)) :~: (n + 'S d)
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (((n + 'S d) :~: (n + (d + N1))) -> (n + (d + N1)) :~: (n + 'S d))
-> ((n + 'S d) :~: (n + (d + N1))) -> (n + (d + N1)) :~: (n + 'S d)
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any n -> Any d -> (n + 'S d) :~: (n + (d + N1))
forall (n :: N') (d :: N').
Any n -> Any d -> (n + 'S d) :~: (n + (d + N1))
lemma2 Any n
n Any d
d) (('S (n + d) :~: ((n + d) + N1)) -> ((n + d) + N1) :~: 'S (n + d)
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (('S (n + d) :~: ((n + d) + N1)) -> ((n + d) + N1) :~: 'S (n + d))
-> ('S (n + d) :~: ((n + d) + N1)) -> ((n + d) + N1) :~: 'S (n + d)
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any n -> Any d -> 'S (n + d) :~: ((n + d) + N1)
forall (n :: N') (d :: N').
Any n -> Any d -> 'S (n + d) :~: ((n + d) + N1)
lemma3 Any n
n Any d
d)
    
    lemma2 :: Any n -> Any d -> (n + S d) :~: (n + (d + N1))
    lemma2 :: forall (n :: N') (d :: N').
Any n -> Any d -> (n + 'S d) :~: (n + (d + N1))
lemma2 Any n
n Any d
d = (n :~: n) -> ('S d :~: (d + N1)) -> (n + 'S d) :~: (n + (d + N1))
forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (Any n -> n :~: n
forall (x :: N'). Any x -> x :~: x
refl Any n
n) (Any d -> 'S d :~: (d + N1)
forall (n :: N'). Any n -> 'S n :~: (n + N1)
lemma7 Any d
d)
    
    lemma3 :: Any n -> Any d -> S (n + d) :~: ((n + d) + N1)
    lemma3 :: forall (n :: N') (d :: N').
Any n -> Any d -> 'S (n + d) :~: ((n + d) + N1)
lemma3 Any n
n Any d
d = Any (n + d) -> 'S (n + d) :~: ((n + d) + N1)
forall (n :: N'). Any n -> 'S n :~: (n + N1)
lemma7 (Any n
nAny n -> Any d -> Any (n + d)
forall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++Any d
d)
    
    lemma5 :: Any n -> Any d -> (n + (d + N1)) :~: ((n + d) + N1)
    lemma5 :: forall (n :: N') (d :: N').
Any n -> Any d -> (n + (d + N1)) :~: ((n + d) + N1)
lemma5 Any n
n Any d
d = (((n + d) + N1) :~: (n + (d + N1)))
-> (n + (d + N1)) :~: ((n + d) + N1)
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym ((((n + d) + N1) :~: (n + (d + N1)))
 -> (n + (d + N1)) :~: ((n + d) + N1))
-> (((n + d) + N1) :~: (n + (d + N1)))
-> (n + (d + N1)) :~: ((n + d) + N1)
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ Any n -> Any d -> Any N1 -> ((n + d) + N1) :~: (n + (d + N1))
forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc Any n
n Any d
d (W N0 -> W (N0 + 1)
forall (d :: N'). W d -> W (d + 1)
SW W N0
W0)
    
    lemma6 :: forall {k} (a :: k) (b :: k) (a' :: k) (b' :: k)
            . a :~: b -> a :~: a' -> b :~: b' -> a' :~: b'
    lemma6 :: forall {k} (a :: k) (b :: k) (a' :: k) (b' :: k).
(a :~: b) -> (a :~: a') -> (b :~: b') -> a' :~: b'
lemma6 a :~: b
Refl a :~: a'
Refl b :~: b'
Refl = a' :~: a'
a' :~: b'
forall {k} (a :: k). a :~: a
Refl
    
    lemma7 :: Any n -> S n :~: n + S N0
    lemma7 :: forall (n :: N'). Any n -> 'S n :~: (n + N1)
lemma7 Any n
n = ('S (n + N0) :~: (n + N1))
-> ('S (n + N0) :~: 'S n)
-> ((n + N1) :~: (n + N1))
-> 'S n :~: (n + N1)
forall {k} (a :: k) (b :: k) (a' :: k) (b' :: k).
(a :~: b) -> (a :~: a') -> (b :~: b') -> a' :~: b'
lemma6 (Any n -> ('S n + N0) :~: (n + N1)
forall (n :: N'). Any n -> ('S n + N0) :~: (n + N1)
lemma8 Any n
n) (Any n -> ('S n + N0) :~: 'S n
forall (n :: N'). Any n -> ('S n + N0) :~: 'S n
lemma9 Any n
n) (n + N1) :~: (n + N1)
forall {k} (a :: k). a :~: a
Refl
    
    lemma8 :: Any n -> S n + N0 :~: n + S N0
    lemma8 :: forall (n :: N'). Any n -> ('S n + N0) :~: (n + N1)
lemma8 Any n
n = Any n -> W N0 -> ('S n + N0) :~: (n + N1)
forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + b) :~: (a + 'S b)
lemmaAdd1 Any n
n W N0
W0
    
    lemma9 :: Any n -> S n + N0 :~: S n
    lemma9 :: forall (n :: N'). Any n -> ('S n + N0) :~: 'S n
lemma9 Any n
n = Any ('S n) -> ('S n + N0) :~: 'S n
forall (a :: N'). Any a -> (a + N0) :~: a
prpAddNtrlR (Any n -> W (n + 1)
forall (d :: N'). W d -> W (d + 1)
SW Any n
n)

{-  
nodTrans :: x :<=: y -> y :<=: z -> x :<=: z
nodTrans = error "nyi" -- Add x (d++d')
-}

----------------------------------------
-- wi -

-- | @0@.
type N0 = 'N0
w0 :: W N0
w0 :: W N0
w0 = W N0
W0

-- | @1@.
type N1 = S N0
w1 :: W N1
w1 :: Any N1
w1 = W N0 -> W (N0 + 1)
forall (d :: N'). W d -> W (d + 1)
SW W N0
w0

-- | @2@.
type N2 = S N1

-- | @3@.
type N3 = S N2

-- | @4@.
type N4 = S N3

-- | @5@.
type N5 = S N4

-- | @6@.
type N6 = S N5

-- | @7@.
type N7 = S N6

-- | @8@.
type N8 = S N7

-- | @9@.
type N9 = S N8

-- | @10@.
type N10 = S N9


{-
type N0 = 'N0
w0 :: W N0
w0 = W0
type N1 = S N0
w1 :: W N1
w1 = SW w0
type N2 = S N1
w2 :: W N2
w2 = SW w1
type N3 = S N2
w3 :: W N3
w3 = SW w2
type N4 = S N3
w4 :: W N4
w4 = SW w3
type N5 = S N4
w5 :: W N5
w5 = SW w4
type N6 = S N5
w6 :: W N6
w6 = SW w5
type N7 = S N6
w7 :: W N7
w7 = SW w6
type N8 = S N7
w8 :: W N8
w8 = SW w7
type N9 = S N8
w9 :: W N9
w9 = SW w8
type N10 = S N9
w10 :: W N10
w10 = SW w9
type N11 = S N10
w11 :: W N11
w11 = SW w10
type N12 = S N11
w12 :: W N12
w12 = SW w11
type N13 = S N12
w13 :: W N13
w13 = SW w12
type N14 = S N13
w14 :: W N14
w14 = SW w13
type N15 = S N14
w15 :: W N15
w15 = SW w14
type N16 = S N15
w16 :: W N16
w16 = SW w15
type N17 = S N16
w17 :: W N17
w17 = SW w16
type N18 = S N17
w18 :: W N18
w18 = SW w17
type N19 = S N18
w19 :: W N19
w19 = SW w18
type N20 = S N19
w20 :: W N20
w20 = SW w19
type N21 = S N20
w21 :: W N21
w21 = SW w20
type N22 = S N21
w22 :: W N22
w22 = SW w21
type N23 = S N22
w23 :: W N23
w23 = SW w22
type N24 = S N23
w24 :: W N24
w24 = SW w23
type N25 = S N24
w25 :: W N25
w25 = SW w24
type N26 = S N25
w26 :: W N26
w26 = SW w25
type N27 = S N26
w27 :: W N27
w27 = SW w26
type N28 = S N27
w28 :: W N28
w28 = SW w27
type N29 = S N28
w29 :: W N29
w29 = SW w28
type N30 = S N29
w30 :: W N30
w30 = SW w29
type N31 = S N30
w31 :: W N31
w31 = SW w30
type N32 = S N31
w32 :: W N32
w32 = SW w31
type N33 = S N32
w33 :: W N33
w33 = SW w32
type N34 = S N33
w34 :: W N34
w34 = SW w33
type N35 = S N34
w35 :: W N35
w35 = SW w34
type N36 = S N35
w36 :: W N36
w36 = SW w35
type N37 = S N36
w37 :: W N37
w37 = SW w36
type N38 = S N37
w38 :: W N38
w38 = SW w37
type N39 = S N38
w39 :: W N39
w39 = SW w38
type N40 = S N39
w40 :: W N40
w40 = SW w39
type N41 = S N40
w41 :: W N41
w41 = SW w40
type N42 = S N41
w42 :: W N42
w42 = SW w41
type N43 = S N42
w43 :: W N43
w43 = SW w42
type N44 = S N43
w44 :: W N44
w44 = SW w43
type N45 = S N44
w45 :: W N45
w45 = SW w44
type N46 = S N45
w46 :: W N46
w46 = SW w45
type N47 = S N46
w47 :: W N47
w47 = SW w46
type N48 = S N47
w48 :: W N48
w48 = SW w47
type N49 = S N48
w49 :: W N49
w49 = SW w48
type N50 = S N49
w50 :: W N50
w50 = SW w49
type N51 = S N50
w51 :: W N51
w51 = SW w50
type N52 = S N51
w52 :: W N52
w52 = SW w51
type N53 = S N52
w53 :: W N53
w53 = SW w52
type N54 = S N53
w54 :: W N54
w54 = SW w53
type N55 = S N54
w55 :: W N55
w55 = SW w54
type N56 = S N55
w56 :: W N56
w56 = SW w55
type N57 = S N56
w57 :: W N57
w57 = SW w56
type N58 = S N57
w58 :: W N58
w58 = SW w57
type N59 = S N58
w59 :: W N59
w59 = SW w58
type N60 = S N59
w60 :: W N60
w60 = SW w59
type N61 = S N60
w61 :: W N61
w61 = SW w60
type N62 = S N61
w62 :: W N62
w62 = SW w61
type N63 = S N62
w63 :: W N63
w63 = SW w62
-}