{-# OPTIONS_HADDOCK not-home #-}
module Morley.Michelson.Typed.Instr.Internal.Proofs
( module Morley.Michelson.Typed.Instr.Internal.Proofs
) where
import Prelude hiding (EQ, GT, LT)
import Data.Constraint (Dict(..), (\\))
import Data.Type.Equality ((:~:)(..))
import Morley.Michelson.Typed.Instr.Constraints
import Morley.Michelson.Typed.TypeLevel
import Morley.Util.Peano
import Morley.Util.PeanoNatural
import Morley.Util.StubbedProof
import Morley.Util.Type (KList(..), type (++))
assocThm :: forall a b c. (a ++ b) ++ c :~: a ++ (b ++ c)
assocThm :: forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm = (Stubbed => ((a ++ b) ++ c) :~: (a ++ (b ++ c)))
-> ((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => ((a ++ b) ++ c) :~: (a ++ (b ++ c)))
-> ((a ++ b) ++ c) :~: (a ++ (b ++ c)))
-> (Stubbed => ((a ++ b) ++ c) :~: (a ++ (b ++ c)))
-> ((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall a b. (a -> b) -> a -> b
$ case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
assumeKnown @a of
KList a
KNil -> ((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: k). a :~: a
Refl
KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> (((xs ++ b) ++ c) ~ (xs ++ (b ++ c))) =>
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: k). a :~: a
Refl ((((xs ++ b) ++ c) ~ (xs ++ (b ++ c))) =>
((a ++ b) ++ c) :~: (a ++ (b ++ c)))
-> (((xs ++ b) ++ c) :~: (xs ++ (b ++ c)))
-> ((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @xs @b @c
takeExtensionThm
:: forall a s n. IsLongerOrSameLength a n ~ 'True
=> PeanoNatural n
-> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm :: forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm PeanoNatural n
n = (Stubbed => LazyTake n (a ++ s) :~: LazyTake n a)
-> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => LazyTake n (a ++ s) :~: LazyTake n a)
-> LazyTake n (a ++ s) :~: LazyTake n a)
-> (Stubbed => LazyTake n (a ++ s) :~: LazyTake n a)
-> LazyTake n (a ++ s) :~: LazyTake n a
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
PeanoNatural n
Zero -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: k). a :~: a
Refl
Succ PeanoNatural m
m -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
assumeKnown @a of
KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> (LazyTake m (xs ++ s) ~ LazyTake m xs) =>
LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: k). a :~: a
Refl ((LazyTake m (xs ++ s) ~ LazyTake m xs) =>
LazyTake n (a ++ s) :~: LazyTake n a)
-> (LazyTake m (xs ++ s) :~: LazyTake m xs)
-> LazyTake n (a ++ s) :~: LazyTake n a
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @xs @s PeanoNatural m
m
dropExtensionThm
:: forall a s n. IsLongerOrSameLength a n ~ 'True
=> PeanoNatural n
-> Drop n (a ++ s) :~: Drop n a ++ s
dropExtensionThm :: forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm PeanoNatural n
n = (Stubbed => Drop n (a ++ s) :~: (Drop n a ++ s))
-> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => Drop n (a ++ s) :~: (Drop n a ++ s))
-> Drop n (a ++ s) :~: (Drop n a ++ s))
-> (Stubbed => Drop n (a ++ s) :~: (Drop n a ++ s))
-> Drop n (a ++ s) :~: (Drop n a ++ s)
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
PeanoNatural n
Zero -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: k). a :~: a
Refl
Succ PeanoNatural m
m -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
assumeKnown @a of
KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> (Drop m (xs ++ s) ~ (Drop m xs ++ s)) =>
Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: k). a :~: a
Refl ((Drop m (xs ++ s) ~ (Drop m xs ++ s)) =>
Drop n (a ++ s) :~: (Drop n a ++ s))
-> (Drop m (xs ++ s) :~: (Drop m xs ++ s))
-> Drop n (a ++ s) :~: (Drop n a ++ s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @xs @s PeanoNatural m
m
isLongerOrSameLengthExtThm
:: forall a s n. IsLongerOrSameLength a n ~ 'True
=> PeanoNatural n
-> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm :: forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm PeanoNatural n
n = (Stubbed => IsLongerOrSameLength (a ++ s) n :~: 'True)
-> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => IsLongerOrSameLength (a ++ s) n :~: 'True)
-> IsLongerOrSameLength (a ++ s) n :~: 'True)
-> (Stubbed => IsLongerOrSameLength (a ++ s) n :~: 'True)
-> IsLongerOrSameLength (a ++ s) n :~: 'True
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
PeanoNatural n
Zero -> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: k). a :~: a
Refl
Succ PeanoNatural m
m -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
assumeKnown @a of
KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> (IsLongerOrSameLength (xs ++ s) m ~ 'True) =>
IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: k). a :~: a
Refl ((IsLongerOrSameLength (xs ++ s) m ~ 'True) =>
IsLongerOrSameLength (a ++ s) n :~: 'True)
-> (IsLongerOrSameLength (xs ++ s) m :~: 'True)
-> IsLongerOrSameLength (a ++ s) n :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm @xs @s PeanoNatural m
m
isLongerOrSameLengthDecThm
:: forall a m. IsLongerOrSameLength a ('S m) ~ 'True
=> PeanoNatural ('S m)
-> IsLongerOrSameLength a m :~: 'True
isLongerOrSameLengthDecThm :: forall {k} (a :: [k]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
isLongerOrSameLengthDecThm PeanoNatural ('S m)
n = (Stubbed => IsLongerOrSameLength a m :~: 'True)
-> IsLongerOrSameLength a m :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => IsLongerOrSameLength a m :~: 'True)
-> IsLongerOrSameLength a m :~: 'True)
-> (Stubbed => IsLongerOrSameLength a m :~: 'True)
-> IsLongerOrSameLength a m :~: 'True
forall a b. (a -> b) -> a -> b
$ case PeanoNatural ('S m)
n of
Succ PeanoNatural m
Zero -> IsLongerOrSameLength a m :~: 'True
forall {k} (a :: k). a :~: a
Refl
Succ (Succ PeanoNatural m
m) -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
assumeKnown @a of
KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> (IsLongerOrSameLength xs m ~ 'True) =>
IsLongerOrSameLength a m :~: 'True
forall {k} (a :: k). a :~: a
Refl ((IsLongerOrSameLength xs m ~ 'True) =>
IsLongerOrSameLength a m :~: 'True)
-> (IsLongerOrSameLength xs m :~: 'True)
-> IsLongerOrSameLength a m :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
forall {k} (a :: [k]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
isLongerOrSameLengthDecThm @xs (PeanoNatural m -> PeanoNatural ('S m)
forall (n :: Peano) (m :: Peano).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural m
m)
isLongerThanExtThm
:: forall a s n. IsLongerThan a n ~ 'True
=> PeanoNatural n
-> IsLongerThan (a ++ s) n :~: 'True
isLongerThanExtThm :: forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
isLongerThanExtThm PeanoNatural n
n = (Stubbed => IsLongerThan (a ++ s) n :~: 'True)
-> IsLongerThan (a ++ s) n :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => IsLongerThan (a ++ s) n :~: 'True)
-> IsLongerThan (a ++ s) n :~: 'True)
-> (Stubbed => IsLongerThan (a ++ s) n :~: 'True)
-> IsLongerThan (a ++ s) n :~: 'True
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
PeanoNatural n
Zero -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
assumeKnown @a of
KCons{} -> IsLongerThan (a ++ s) n :~: 'True
forall {k} (a :: k). a :~: a
Refl
Succ PeanoNatural m
m -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
assumeKnown @a of
KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> (IsLongerThan (xs ++ s) m ~ 'True) =>
IsLongerThan (a ++ s) n :~: 'True
forall {k} (a :: k). a :~: a
Refl ((IsLongerThan (xs ++ s) m ~ 'True) =>
IsLongerThan (a ++ s) n :~: 'True)
-> (IsLongerThan (xs ++ s) m :~: 'True)
-> IsLongerThan (a ++ s) n :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
isLongerThanExtThm @xs @s PeanoNatural m
m
dropHeadThm
:: forall x a n. IsLongerThan (x : a) n ~ 'True
=> PeanoNatural n
-> IsLongerOrSameLength a n :~: 'True
dropHeadThm :: forall {k} (x :: k) (a :: [k]) (n :: Peano).
(IsLongerThan (x : a) n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a n :~: 'True
dropHeadThm PeanoNatural n
n = (Stubbed => IsLongerOrSameLength a n :~: 'True)
-> IsLongerOrSameLength a n :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => IsLongerOrSameLength a n :~: 'True)
-> IsLongerOrSameLength a n :~: 'True)
-> (Stubbed => IsLongerOrSameLength a n :~: 'True)
-> IsLongerOrSameLength a n :~: 'True
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
PeanoNatural n
Zero -> IsLongerOrSameLength a n :~: 'True
forall {k} (a :: k). a :~: a
Refl
Succ PeanoNatural m
m -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
assumeKnown @a of
KCons (Proxy x
_ :: Proxy y) (Proxy xs
_ :: Proxy xs) -> (IsLongerOrSameLength xs m ~ 'True) =>
IsLongerOrSameLength a n :~: 'True
forall {k} (a :: k). a :~: a
Refl ((IsLongerOrSameLength xs m ~ 'True) =>
IsLongerOrSameLength a n :~: 'True)
-> (IsLongerOrSameLength xs m :~: 'True)
-> IsLongerOrSameLength a n :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (x :: k) (a :: [k]) (n :: Peano).
(IsLongerThan (x : a) n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a n :~: 'True
forall {k} (x :: k) (a :: [k]) (n :: Peano).
(IsLongerThan (x : a) n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a n :~: 'True
dropHeadThm @y @xs PeanoNatural m
m
isLongerThanIncThm
:: forall a n. IsLongerThan a n ~ 'True
=> PeanoNatural n
-> IsLongerOrSameLength a ('S n) :~: 'True
isLongerThanIncThm :: forall {k} (a :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True
isLongerThanIncThm PeanoNatural n
n = (Stubbed => IsLongerOrSameLength a ('S n) :~: 'True)
-> IsLongerOrSameLength a ('S n) :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => IsLongerOrSameLength a ('S n) :~: 'True)
-> IsLongerOrSameLength a ('S n) :~: 'True)
-> (Stubbed => IsLongerOrSameLength a ('S n) :~: 'True)
-> IsLongerOrSameLength a ('S n) :~: 'True
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
PeanoNatural n
Zero -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
assumeKnown @a of
KCons{} -> IsLongerOrSameLength a ('S n) :~: 'True
forall {k} (a :: k). a :~: a
Refl
Succ PeanoNatural m
m -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
assumeKnown @a of
KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> (IsLongerOrSameLength xs ('S m) ~ 'True) =>
IsLongerOrSameLength a ('S n) :~: 'True
forall {k} (a :: k). a :~: a
Refl ((IsLongerOrSameLength xs ('S m) ~ 'True) =>
IsLongerOrSameLength a ('S n) :~: 'True)
-> (IsLongerOrSameLength xs ('S m) :~: 'True)
-> IsLongerOrSameLength a ('S n) :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True
forall {k} (a :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True
isLongerThanIncThm @xs PeanoNatural m
m
dugLengthThm
:: forall b x n. IsLongerThan b n ~ 'True
=> PeanoNatural n
-> IsLongerThan (x ': LazyTake n b ++ Drop ('S n) b) n :~: 'True
dugLengthThm :: forall {k} (b :: [k]) (x :: k) (n :: Peano).
(IsLongerThan b n ~ 'True) =>
PeanoNatural n
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
dugLengthThm PeanoNatural n
n = (Stubbed =>
IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True)
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed =>
IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True)
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True)
-> (Stubbed =>
IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True)
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
PeanoNatural n
Zero -> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl
Succ PeanoNatural m
m -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
assumeKnown @b of
KCons (Proxy x
_ :: Proxy y) (Proxy xs
_ :: Proxy xs) -> (IsLongerThan (x : (LazyTake m xs ++ Drop ('S m) xs)) m ~ 'True) =>
IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl ((IsLongerThan (x : (LazyTake m xs ++ Drop ('S m) xs)) m
~ 'True) =>
IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True)
-> (IsLongerThan (x : (LazyTake m xs ++ Drop ('S m) xs)) m
:~: 'True)
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (b :: [k]) (x :: k) (n :: Peano).
(IsLongerThan b n ~ 'True) =>
PeanoNatural n
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
forall {k} (b :: [k]) (x :: k) (n :: Peano).
(IsLongerThan b n ~ 'True) =>
PeanoNatural n
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
dugLengthThm @xs @y PeanoNatural m
m
dropNExtensionThm
:: forall s a b n. (Drop n a ~ b, IsLongerOrSameLength a n ~ 'True)
=> PeanoNatural n
-> Dict (Drop n (a ++ s) ~ b ++ s, IsLongerOrSameLength (a ++ s) n ~ 'True)
dropNExtensionThm :: forall {k} (s :: [k]) (a :: [k]) (b :: [k]) (n :: Peano).
(Drop n a ~ b, IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n
-> Dict
(Drop n (a ++ s) ~ (b ++ s),
IsLongerOrSameLength (a ++ s) n ~ 'True)
dropNExtensionThm PeanoNatural n
n = (Drop n (a ++ s) ~ (b ++ s)) =>
Dict
(Drop n (a ++ s) ~ (b ++ s),
IsLongerOrSameLength (a ++ s) n ~ 'True)
forall (a :: Constraint). a => Dict a
Dict
((Drop n (a ++ s) ~ (b ++ s)) =>
Dict
(Drop n (a ++ s) ~ (b ++ s),
IsLongerOrSameLength (a ++ s) n ~ 'True))
-> (Drop n (a ++ s) :~: (b ++ s))
-> Dict
(Drop n (a ++ s) ~ (b ++ s),
IsLongerOrSameLength (a ++ s) n ~ 'True)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @a @s PeanoNatural n
n
((IsLongerOrSameLength (a ++ s) n ~ 'True) =>
Dict
(Drop n (a ++ s) ~ (b ++ s),
IsLongerOrSameLength (a ++ s) n ~ 'True))
-> (IsLongerOrSameLength (a ++ s) n :~: 'True)
-> Dict
(Drop n (a ++ s) ~ (b ++ s),
IsLongerOrSameLength (a ++ s) n ~ 'True)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm @a @s PeanoNatural n
n
dupNExtensionThm
:: forall s a b n x. (b ~ x : a, ConstraintDUPN n a b x)
=> PeanoNatural n
-> Dict (ConstraintDUPN n (a ++ s) (b ++ s) x)
dupNExtensionThm :: forall (s :: [T]) (a :: [T]) (b :: [T]) (n :: Peano) (x :: T).
(b ~ (x : a), ConstraintDUPN n a b x) =>
PeanoNatural n -> Dict (ConstraintDUPN n (a ++ s) (b ++ s) x)
dupNExtensionThm n :: PeanoNatural n
n@(Succ PeanoNatural m
m) = (IsLongerOrSameLength (a ++ s) ('S (Decrement n)) ~ 'True) =>
Dict
(RequireLongerOrSameLength (a ++ s) ('S (Decrement n)),
'True ~ 'True,
(a ++ s)
~ (LazyTake (Decrement n) (a ++ s)
++ (x : Drop ('S (Decrement n)) (a ++ s))),
(x : (a ++ s)) ~ (x : (a ++ s)))
forall (a :: Constraint). a => Dict a
Dict
((IsLongerOrSameLength (a ++ s) ('S (Decrement n)) ~ 'True) =>
Dict
(RequireLongerOrSameLength (a ++ s) ('S (Decrement n)),
'True ~ 'True,
(a ++ s)
~ (LazyTake (Decrement n) (a ++ s)
++ (x : Drop ('S (Decrement n)) (a ++ s))),
(x : (a ++ s)) ~ (x : (a ++ s))))
-> (IsLongerOrSameLength (a ++ s) ('S (Decrement n)) :~: 'True)
-> Dict
(RequireLongerOrSameLength (a ++ s) ('S (Decrement n)),
'True ~ 'True,
(a ++ s)
~ (LazyTake (Decrement n) (a ++ s)
++ (x : Drop ('S (Decrement n)) (a ++ s))),
(x : (a ++ s)) ~ (x : (a ++ s)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm @a @s PeanoNatural n
n
(((a ++ s)
~ (LazyTake (Decrement n) a ++ (x : (Drop n a ++ s)))) =>
Dict
(RequireLongerOrSameLength (a ++ s) ('S (Decrement n)),
'True ~ 'True,
(a ++ s)
~ (LazyTake (Decrement n) (a ++ s)
++ (x : Drop ('S (Decrement n)) (a ++ s))),
(x : (a ++ s)) ~ (x : (a ++ s))))
-> ((a ++ s)
:~: (LazyTake (Decrement n) a ++ (x : (Drop n a ++ s))))
-> Dict
(RequireLongerOrSameLength (a ++ s) ('S (Decrement n)),
'True ~ 'True,
(a ++ s)
~ (LazyTake (Decrement n) (a ++ s)
++ (x : Drop ('S (Decrement n)) (a ++ s))),
(x : (a ++ s)) ~ (x : (a ++ s)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(LazyTake (Decrement n) a) @(x : Drop n a) @s
((LazyTake (Decrement n) (a ++ s) ~ LazyTake (Decrement n) a) =>
Dict
(RequireLongerOrSameLength (a ++ s) ('S (Decrement n)),
'True ~ 'True,
(a ++ s)
~ (LazyTake (Decrement n) (a ++ s)
++ (x : Drop ('S (Decrement n)) (a ++ s))),
(x : (a ++ s)) ~ (x : (a ++ s))))
-> (LazyTake (Decrement n) (a ++ s) :~: LazyTake (Decrement n) a)
-> Dict
(RequireLongerOrSameLength (a ++ s) ('S (Decrement n)),
'True ~ 'True,
(a ++ s)
~ (LazyTake (Decrement n) (a ++ s)
++ (x : Drop ('S (Decrement n)) (a ++ s))),
(x : (a ++ s)) ~ (x : (a ++ s)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @a @s PeanoNatural m
m ((IsLongerOrSameLength a (Decrement n) ~ 'True) =>
Dict
(RequireLongerOrSameLength (a ++ s) ('S (Decrement n)),
'True ~ 'True,
(a ++ s)
~ (LazyTake (Decrement n) (a ++ s)
++ (x : Drop ('S (Decrement n)) (a ++ s))),
(x : (a ++ s)) ~ (x : (a ++ s))))
-> (IsLongerOrSameLength a (Decrement n) :~: 'True)
-> Dict
(RequireLongerOrSameLength (a ++ s) ('S (Decrement n)),
'True ~ 'True,
(a ++ s)
~ (LazyTake (Decrement n) (a ++ s)
++ (x : Drop ('S (Decrement n)) (a ++ s))),
(x : (a ++ s)) ~ (x : (a ++ s)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
forall {k} (a :: [k]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
isLongerOrSameLengthDecThm @a PeanoNatural n
PeanoNatural ('S (Decrement n))
n
((Drop ('S (Decrement n)) (a ++ s) ~ (Drop n a ++ s)) =>
Dict
(RequireLongerOrSameLength (a ++ s) ('S (Decrement n)),
'True ~ 'True,
(a ++ s)
~ (LazyTake (Decrement n) (a ++ s)
++ (x : Drop ('S (Decrement n)) (a ++ s))),
(x : (a ++ s)) ~ (x : (a ++ s))))
-> (Drop ('S (Decrement n)) (a ++ s) :~: (Drop n a ++ s))
-> Dict
(RequireLongerOrSameLength (a ++ s) ('S (Decrement n)),
'True ~ 'True,
(a ++ s)
~ (LazyTake (Decrement n) (a ++ s)
++ (x : Drop ('S (Decrement n)) (a ++ s))),
(x : (a ++ s)) ~ (x : (a ++ s)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @a @s PeanoNatural n
n
dugNExtensionThm
:: forall s a b x r n. (a ~ x : r, ConstraintDUG n a b x)
=> PeanoNatural n
-> Dict (ConstraintDUG n (a ++ s) (b ++ s) x)
dugNExtensionThm :: forall (s :: [T]) (a :: [T]) (b :: [T]) (x :: T) (r :: [T])
(n :: Peano).
(a ~ (x : r), ConstraintDUG n a b x) =>
PeanoNatural n -> Dict (ConstraintDUG n (a ++ s) (b ++ s) x)
dugNExtensionThm PeanoNatural n
n = (IsLongerThan (LazyTake n r ++ (x : (Drop n r ++ s))) n ~ 'True) =>
Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (a :: Constraint). a => Dict a
Dict
((IsLongerThan (LazyTake n r ++ (x : (Drop n r ++ s))) n
~ 'True) =>
Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerThan (LazyTake n r ++ (x : (Drop n r ++ s))) n
:~: 'True)
-> Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
isLongerThanExtThm @b @s PeanoNatural n
n
(((r ++ s) ~ (LazyTake n b ++ (Drop ('S n) b ++ s))) =>
Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> ((r ++ s) :~: (LazyTake n b ++ (Drop ('S n) b ++ s)))
-> Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(LazyTake n b) @(Drop ('S n) b) @s
((LazyTake n (LazyTake n r ++ (x : (Drop n r ++ s)))
~ LazyTake n b) =>
Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (LazyTake n (LazyTake n r ++ (x : (Drop n r ++ s)))
:~: LazyTake n b)
-> Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @b @s PeanoNatural n
n ((IsLongerOrSameLength b n ~ 'True) =>
Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerOrSameLength b n :~: 'True)
-> Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
forall {k} (a :: [k]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
isLongerOrSameLengthDecThm @b (PeanoNatural n -> PeanoNatural ('S n)
forall (n :: Peano) (m :: Peano).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural n
n)
((Drop ('S n) (LazyTake n r ++ (x : (Drop n r ++ s)))
~ (Drop ('S n) b ++ s)) =>
Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (Drop ('S n) (LazyTake n r ++ (x : (Drop n r ++ s)))
:~: (Drop ('S n) b ++ s))
-> Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @b @s (PeanoNatural n -> PeanoNatural ('S n)
forall (n :: Peano) (m :: Peano).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural n
n)
((IsLongerOrSameLength b ('S n) ~ 'True) =>
Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerOrSameLength b ('S n) :~: 'True)
-> Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True
forall {k} (a :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True
isLongerThanIncThm @b PeanoNatural n
n
(((b ++ s) ~ (LazyTake n r ++ (x : (Drop n r ++ s)))) =>
Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> ((b ++ s) :~: (LazyTake n r ++ (x : (Drop n r ++ s))))
-> Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(LazyTake n r) @(x : Drop n r) @s
((LazyTake n (r ++ s) ~ LazyTake n r) =>
Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (LazyTake n (r ++ s) :~: LazyTake n r)
-> Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @r @s PeanoNatural n
n ((Drop n (r ++ s) ~ (Drop n r ++ s)) =>
Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (Drop n (r ++ s) :~: (Drop n r ++ s))
-> Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @r @s PeanoNatural n
n ((IsLongerOrSameLength r n ~ 'True) =>
Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerOrSameLength r n :~: 'True)
-> Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (x :: k) (a :: [k]) (n :: Peano).
(IsLongerThan (x : a) n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a n :~: 'True
forall (x :: T) (a :: [T]) (n :: Peano).
(IsLongerThan (x : a) n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a n :~: 'True
dropHeadThm @x @r PeanoNatural n
n
((IsLongerThan (x : r) n ~ 'True) =>
Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerThan (x : r) n :~: 'True)
-> Dict
(RequireLongerThan (b ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (b :: [T]) (x :: T) (n :: Peano).
(IsLongerThan b n ~ 'True) =>
PeanoNatural n
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
forall {k} (b :: [k]) (x :: k) (n :: Peano).
(IsLongerThan b n ~ 'True) =>
PeanoNatural n
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
dugLengthThm @b @x PeanoNatural n
n
digNExtensionThm
:: forall s a b x r n. (b ~ x : r, ConstraintDIG n a b x)
=> PeanoNatural n
-> Dict (ConstraintDIG n (a ++ s) (b ++ s) x)
digNExtensionThm :: forall (s :: [T]) (a :: [T]) (b :: [T]) (x :: T) (r :: [T])
(n :: Peano).
(b ~ (x : r), ConstraintDIG n a b x) =>
PeanoNatural n -> Dict (ConstraintDIG n (a ++ s) (b ++ s) x)
digNExtensionThm PeanoNatural n
n = (IsLongerThan (LazyTake n r ++ (x : (Drop n r ++ s))) n ~ 'True) =>
Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (a :: Constraint). a => Dict a
Dict
((IsLongerThan (LazyTake n r ++ (x : (Drop n r ++ s))) n
~ 'True) =>
Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerThan (LazyTake n r ++ (x : (Drop n r ++ s))) n
:~: 'True)
-> Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
isLongerThanExtThm @a @s PeanoNatural n
n
(((r ++ s) ~ (LazyTake n a ++ (Drop ('S n) a ++ s))) =>
Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> ((r ++ s) :~: (LazyTake n a ++ (Drop ('S n) a ++ s)))
-> Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(LazyTake n a) @(Drop ('S n) a) @s
((LazyTake n (LazyTake n r ++ (x : (Drop n r ++ s)))
~ LazyTake n a) =>
Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (LazyTake n (LazyTake n r ++ (x : (Drop n r ++ s)))
:~: LazyTake n a)
-> Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @a @s PeanoNatural n
n ((IsLongerOrSameLength a n ~ 'True) =>
Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerOrSameLength a n :~: 'True)
-> Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
forall {k} (a :: [k]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
isLongerOrSameLengthDecThm @a (PeanoNatural n -> PeanoNatural ('S n)
forall (n :: Peano) (m :: Peano).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural n
n)
((Drop ('S n) (LazyTake n r ++ (x : (Drop n r ++ s)))
~ (Drop ('S n) a ++ s)) =>
Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (Drop ('S n) (LazyTake n r ++ (x : (Drop n r ++ s)))
:~: (Drop ('S n) a ++ s))
-> Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @a @s (PeanoNatural n -> PeanoNatural ('S n)
forall (n :: Peano) (m :: Peano).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural n
n)
((IsLongerOrSameLength a ('S n) ~ 'True) =>
Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerOrSameLength a ('S n) :~: 'True)
-> Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True
forall {k} (a :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True
isLongerThanIncThm @a PeanoNatural n
n
(((a ++ s) ~ (LazyTake n r ++ (x : (Drop n r ++ s)))) =>
Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> ((a ++ s) :~: (LazyTake n r ++ (x : (Drop n r ++ s))))
-> Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(LazyTake n r) @(x : Drop n r) @s
((LazyTake n (r ++ s) ~ LazyTake n r) =>
Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (LazyTake n (r ++ s) :~: LazyTake n r)
-> Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @r @s PeanoNatural n
n ((Drop n (r ++ s) ~ (Drop n r ++ s)) =>
Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (Drop n (r ++ s) :~: (Drop n r ++ s))
-> Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @r @s PeanoNatural n
n ((IsLongerOrSameLength r n ~ 'True) =>
Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerOrSameLength r n :~: 'True)
-> Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (x :: k) (a :: [k]) (n :: Peano).
(IsLongerThan (x : a) n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a n :~: 'True
forall (x :: T) (a :: [T]) (n :: Peano).
(IsLongerThan (x : a) n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a n :~: 'True
dropHeadThm @x @r PeanoNatural n
n
((IsLongerThan (x : r) n ~ 'True) =>
Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerThan (x : r) n :~: 'True)
-> Dict
(RequireLongerThan (a ++ s) n,
(x : (r ++ s))
~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (b :: [T]) (x :: T) (n :: Peano).
(IsLongerThan b n ~ 'True) =>
PeanoNatural n
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
forall {k} (b :: [k]) (x :: k) (n :: Peano).
(IsLongerThan b n ~ 'True) =>
PeanoNatural n
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
dugLengthThm @a @x PeanoNatural n
n
dipNExtensionThm
:: forall s a b s1 s1' n. ConstraintDIPN n a b s1 s1'
=> PeanoNatural n
-> Dict (ConstraintDIPN n (a ++ s) (b ++ s) (s1 ++ s) (s1' ++ s))
dipNExtensionThm :: forall (s :: [T]) (a :: [T]) (b :: [T]) (s1 :: [T]) (s1' :: [T])
(n :: Peano).
ConstraintDIPN n a b s1 s1' =>
PeanoNatural n
-> Dict (ConstraintDIPN n (a ++ s) (b ++ s) (s1 ++ s) (s1' ++ s))
dipNExtensionThm PeanoNatural n
n = (IsLongerOrSameLength (LazyTake n a ++ (s1 ++ s)) n ~ 'True) =>
Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (a :: Constraint). a => Dict a
Dict
((IsLongerOrSameLength (LazyTake n a ++ (s1 ++ s)) n ~ 'True) =>
Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> (IsLongerOrSameLength (LazyTake n a ++ (s1 ++ s)) n :~: 'True)
-> Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm @a @s PeanoNatural n
n
((Drop n (LazyTake n a ++ (s1 ++ s)) ~ (s1 ++ s)) =>
Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> (Drop n (LazyTake n a ++ (s1 ++ s)) :~: (s1 ++ s))
-> Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @a @s PeanoNatural n
n
(((b ++ s) ~ (LazyTake n a ++ (s1' ++ s))) =>
Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> ((b ++ s) :~: (LazyTake n a ++ (s1' ++ s)))
-> Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(LazyTake n a) @s1' @s
((LazyTake n (LazyTake n a ++ (s1 ++ s)) ~ LazyTake n a) =>
Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> (LazyTake n (LazyTake n a ++ (s1 ++ s)) :~: LazyTake n a)
-> Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @a @s PeanoNatural n
n
(((a ++ s) ~ (LazyTake n a ++ (s1 ++ s))) =>
Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> ((a ++ s) :~: (LazyTake n a ++ (s1 ++ s)))
-> Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(LazyTake n a) @s1 @s
((Drop n (b ++ s) ~ (s1' ++ s)) =>
Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> (Drop n (b ++ s) :~: (s1' ++ s))
-> Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @b @s PeanoNatural n
n
((IsLongerOrSameLength (b ++ s) n ~ 'True) =>
Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> (IsLongerOrSameLength (b ++ s) n :~: 'True)
-> Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm @b @s PeanoNatural n
n
((IsLongerOrSameLength b n ~ 'True) =>
Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> (IsLongerOrSameLength b n :~: 'True)
-> Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
(s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]) (out :: [T]) (s :: [T]) (n :: Peano).
(RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ out) =>
PeanoNatural n -> IsLongerOrSameLength out n :~: 'True
forall {k} (inp :: [k]) (out :: [k]) (s :: [k]) (n :: Peano).
(RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ out) =>
PeanoNatural n -> IsLongerOrSameLength out n :~: 'True
dipNExtensionLemma @a @b @s1' PeanoNatural n
n
dipNExtensionLemma ::
forall inp out s n.
( RequireLongerOrSameLength inp n
, LazyTake n inp ++ s ~ out)
=> PeanoNatural n
-> IsLongerOrSameLength out n :~: 'True
dipNExtensionLemma :: forall {k} (inp :: [k]) (out :: [k]) (s :: [k]) (n :: Peano).
(RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ out) =>
PeanoNatural n -> IsLongerOrSameLength out n :~: 'True
dipNExtensionLemma PeanoNatural n
n = (Stubbed => IsLongerOrSameLength out n :~: 'True)
-> IsLongerOrSameLength out n :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => IsLongerOrSameLength out n :~: 'True)
-> IsLongerOrSameLength out n :~: 'True)
-> (Stubbed => IsLongerOrSameLength out n :~: 'True)
-> IsLongerOrSameLength out n :~: 'True
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
PeanoNatural n
Zero -> IsLongerOrSameLength out n :~: 'True
forall {k} (a :: k). a :~: a
Refl
Succ PeanoNatural m
m -> case (forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
assumeKnown @inp, forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
assumeKnown @out) of
(KCons Proxy x
_ (Proxy xs
_ :: Proxy inp'), KCons Proxy x
_ (Proxy xs
_ :: Proxy out')) ->
(IsLongerOrSameLength (LazyTake m (Tail inp) ++ s) m ~ 'True) =>
IsLongerOrSameLength out n :~: 'True
forall {k} (a :: k). a :~: a
Refl ((IsLongerOrSameLength (LazyTake m (Tail inp) ++ s) m ~ 'True) =>
IsLongerOrSameLength out n :~: 'True)
-> (IsLongerOrSameLength (LazyTake m (Tail inp) ++ s) m :~: 'True)
-> IsLongerOrSameLength out n :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [k]) (out :: [k]) (s :: [k]) (n :: Peano).
(RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ out) =>
PeanoNatural n -> IsLongerOrSameLength out n :~: 'True
forall {k} (inp :: [k]) (out :: [k]) (s :: [k]) (n :: Peano).
(RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ out) =>
PeanoNatural n -> IsLongerOrSameLength out n :~: 'True
dipNExtensionLemma @inp' @out' @s PeanoNatural m
m
pairNExtensionThm
:: forall s a n. (n >= ToPeano 2 ~ 'True, IsLongerOrSameLength a n ~ 'True)
=> PeanoNatural n
-> Dict (ConstraintPairN n (a ++ s)
, RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a)
, Drop n (a ++ s) ~ (Drop n a ++ s)
)
pairNExtensionThm :: forall (s :: [T]) (a :: [T]) (n :: Peano).
((n >= ToPeano 2) ~ 'True, IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n
-> Dict
(ConstraintPairN n (a ++ s),
RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
Drop n (a ++ s) ~ (Drop n a ++ s))
pairNExtensionThm PeanoNatural n
n = (IsLongerOrSameLength (a ++ s) n ~ 'True) =>
Dict
((RequireLongerOrSameLength (a ++ s) n,
(() :: Constraint, 'True ~ 'True)),
RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
Drop n (a ++ s) ~ (Drop n a ++ s))
forall (a :: Constraint). a => Dict a
Dict
((IsLongerOrSameLength (a ++ s) n ~ 'True) =>
Dict
((RequireLongerOrSameLength (a ++ s) n,
(() :: Constraint, 'True ~ 'True)),
RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
Drop n (a ++ s) ~ (Drop n a ++ s)))
-> (IsLongerOrSameLength (a ++ s) n :~: 'True)
-> Dict
((RequireLongerOrSameLength (a ++ s) n,
(() :: Constraint, 'True ~ 'True)),
RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
Drop n (a ++ s) ~ (Drop n a ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm @a @s PeanoNatural n
n
((Drop n (a ++ s) ~ (Drop n a ++ s)) =>
Dict
((RequireLongerOrSameLength (a ++ s) n,
(() :: Constraint, 'True ~ 'True)),
RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
Drop n (a ++ s) ~ (Drop n a ++ s)))
-> (Drop n (a ++ s) :~: (Drop n a ++ s))
-> Dict
((RequireLongerOrSameLength (a ++ s) n,
(() :: Constraint, 'True ~ 'True)),
RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
Drop n (a ++ s) ~ (Drop n a ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @a @s PeanoNatural n
n
((LazyTake n (a ++ s) ~ LazyTake n a) =>
Dict
((RequireLongerOrSameLength (a ++ s) n,
(() :: Constraint, 'True ~ 'True)),
RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
Drop n (a ++ s) ~ (Drop n a ++ s)))
-> (LazyTake n (a ++ s) :~: LazyTake n a)
-> Dict
((RequireLongerOrSameLength (a ++ s) n,
(() :: Constraint, 'True ~ 'True)),
RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
Drop n (a ++ s) ~ (Drop n a ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @a @s PeanoNatural n
n
unpairNExtensionThm
:: forall s a b n x r
. ( a ~ x : r, CombedPairLeafCountIsAtLeast n x ~ 'True
, n >= ToPeano 2 ~ 'True, UnpairN n x ++ r ~ b
)
=> PeanoNatural n
-> Dict (ConstraintUnpairN n x, UnpairN n x ++ r ++ s ~ b ++ s)
unpairNExtensionThm :: forall (s :: [T]) (a :: [T]) (b :: [T]) (n :: Peano) (x :: T)
(r :: [T]).
(a ~ (x : r), CombedPairLeafCountIsAtLeast n x ~ 'True,
(n >= ToPeano 2) ~ 'True, (UnpairN n x ++ r) ~ b) =>
PeanoNatural n
-> Dict
(ConstraintUnpairN n x, (UnpairN n x ++ (r ++ s)) ~ (b ++ s))
unpairNExtensionThm PeanoNatural n
_ = ((b ++ s) ~ (UnpairN n x ++ (r ++ s))) =>
Dict
(((() :: Constraint, 'True ~ 'True),
(() :: Constraint, 'True ~ 'True)),
(UnpairN n x ++ (r ++ s)) ~ (b ++ s))
forall (a :: Constraint). a => Dict a
Dict (((b ++ s) ~ (UnpairN n x ++ (r ++ s))) =>
Dict
(((() :: Constraint, 'True ~ 'True),
(() :: Constraint, 'True ~ 'True)),
(UnpairN n x ++ (r ++ s)) ~ (b ++ s)))
-> ((b ++ s) :~: (UnpairN n x ++ (r ++ s)))
-> Dict
(((() :: Constraint, 'True ~ 'True),
(() :: Constraint, 'True ~ 'True)),
(UnpairN n x ++ (r ++ s)) ~ (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(UnpairN n x) @r @s
where Dict (a ~ (x : r))
_ = forall (a :: Constraint). a => Dict a
Dict @(a ~ x : r)