Portability	non-portable (MPTC, FD, TH, undecidable instances, missing constructors)
Stability	experimental
Maintainer	Edward Kmett <ekmett@gmail.com>
Safe Haskell	None

Data.Type.Hex.Stage1

Description

Stage1: Lay the ground work for all sorts of Template Haskell hackery in the later stages. Only a handful of class specifications in this file are for later public consumption, and none of those are fleshed out here.

This multiple-stage implementation is necessitated by the way Template Haskell is implemented in GHC.

Documentation

t, f :: Name Source

hex :: String Source

xn, hn :: [Name]Source

x, h :: [Type]Source

xh :: [(Type, Type)]Source

x0, h0 :: [Type]Source

xh0 :: [(Type, Type)]Source

xF, hF :: [Type]Source

xhF :: [(Type, Type)]Source

x0F :: [Type]Source

a, d, c, b :: Name Source

mkXT :: Name -> Dec Source

mkHT :: Name -> Dec Source

tnot, signzero, negative, positive :: Name Source

class LSN a d a' | a -> d a', d a' -> aSource

Instances

LSN F H0 F	extract the least signficant nybble from a hex number
LSN T HF T
LSN (DF F) HF F
LSN (DE F) HE F
LSN (DE T) HE T
LSN (DD F) HD F
LSN (DD T) HD T
LSN (DC F) HC F
LSN (DC T) HC T
LSN (DB F) HB F
LSN (DB T) HB T
LSN (DA F) HA F
LSN (DA T) HA T
LSN (D9 F) H9 F
LSN (D9 T) H9 T
LSN (D8 F) H8 F
LSN (D8 T) H8 T
LSN (D7 F) H7 F
LSN (D7 T) H7 T
LSN (D6 F) H6 F
LSN (D6 T) H6 T
LSN (D5 F) H5 F
LSN (D5 T) H5 T
LSN (D4 F) H4 F
LSN (D4 T) H4 T
LSN (D3 F) H3 F
LSN (D3 T) H3 T
LSN (D2 F) H2 F
LSN (D2 T) H2 T
LSN (D1 F) H1 F
LSN (D1 T) H1 T
LSN (D0 T) H0 T
LSN (DF (DF a)) HF (DF a)
LSN (DE (DE a)) HE (DE a)
LSN (DD (DD a)) HD (DD a)
LSN (DC (DC a)) HC (DC a)
LSN (DB (DB a)) HB (DB a)
LSN (DA (DA a)) HA (DA a)
LSN (D9 (D9 a)) H9 (D9 a)
LSN (D8 (D8 a)) H8 (D8 a)
LSN (D7 (D7 a)) H7 (D7 a)
LSN (D6 (D6 a)) H6 (D6 a)
LSN (D5 (D5 a)) H5 (D5 a)
LSN (D4 (D4 a)) H4 (D4 a)
LSN (D3 (D3 a)) H3 (D3 a)
LSN (D2 (D2 a)) H2 (D2 a)
LSN (D1 (D1 a)) H1 (D1 a)
LSN (D0 (D0 a)) H0 (D0 a)

class Trichotomy n s | n -> sSource

Instances

Trichotomy F SignZero
Trichotomy T Negative
Trichotomy (DF F) Positive
Trichotomy (DE F) Positive
Trichotomy (DE T) Negative
Trichotomy (DD F) Positive
Trichotomy (DD T) Negative
Trichotomy (DC F) Positive
Trichotomy (DC T) Negative
Trichotomy (DB F) Positive
Trichotomy (DB T) Negative
Trichotomy (DA F) Positive
Trichotomy (DA T) Negative
Trichotomy (D9 F) Positive
Trichotomy (D9 T) Negative
Trichotomy (D8 F) Positive
Trichotomy (D8 T) Negative
Trichotomy (D7 F) Positive
Trichotomy (D7 T) Negative
Trichotomy (D6 F) Positive
Trichotomy (D6 T) Negative
Trichotomy (D5 F) Positive
Trichotomy (D5 T) Negative
Trichotomy (D4 F) Positive
Trichotomy (D4 T) Negative
Trichotomy (D3 F) Positive
Trichotomy (D3 T) Negative
Trichotomy (D2 F) Positive
Trichotomy (D2 T) Negative
Trichotomy (D1 F) Positive
Trichotomy (D1 T) Negative
(Trichotomy a b, Ext0 a) => Trichotomy (D1 (DF a)) b
Trichotomy (D0 T) Negative
(Trichotomy a b, ExtF a) => Trichotomy (D0 (DF a)) b

class TEven a b | a -> bSource

Instances

TEven F T
TEven T F
TEven (DF a) F
TEven (DE a) T
TEven (DD a) F
TEven (DC a) T
TEven (DB a) F
TEven (DA a) T
TEven (D9 a) F
TEven (D8 a) T
TEven (D7 a) F
TEven (D6 a) T
TEven (D5 a) F
TEven (D4 a) T
TEven (D3 a) F
TEven (D2 a) T
TEven (D1 a) F
TEven (D0 a) T

class TSucc n m | n -> m, m -> nSource

Instances

TSucc T F
TSucc F (D1 F)
TSucc (DE T) T
(TSucc n m, ExtF n, Ext0 m) => TSucc (DF n) (D0 m)
TSucc (DE F) (DF F)
TSucc (DE (DF a)) (DF (DF a))
TSucc (DE (DE a)) (DF (DE a))
TSucc (DE (DD a)) (DF (DD a))
TSucc (DE (DC a)) (DF (DC a))
TSucc (DE (DB a)) (DF (DB a))
TSucc (DE (DA a)) (DF (DA a))
TSucc (DE (D9 a)) (DF (D9 a))
TSucc (DE (D8 a)) (DF (D8 a))
TSucc (DE (D7 a)) (DF (D7 a))
TSucc (DE (D6 a)) (DF (D6 a))
TSucc (DE (D5 a)) (DF (D5 a))
TSucc (DE (D4 a)) (DF (D4 a))
TSucc (DE (D3 a)) (DF (D3 a))
TSucc (DE (D2 a)) (DF (D2 a))
TSucc (DE (D1 a)) (DF (D1 a))
TSucc (DE (D0 a)) (DF (D0 a))
TSucc (DD F) (DE F)
TSucc (DD T) (DE T)
TSucc (DD (DF a)) (DE (DF a))
TSucc (DD (DE a)) (DE (DE a))
TSucc (DD (DD a)) (DE (DD a))
TSucc (DD (DC a)) (DE (DC a))
TSucc (DD (DB a)) (DE (DB a))
TSucc (DD (DA a)) (DE (DA a))
TSucc (DD (D9 a)) (DE (D9 a))
TSucc (DD (D8 a)) (DE (D8 a))
TSucc (DD (D7 a)) (DE (D7 a))
TSucc (DD (D6 a)) (DE (D6 a))
TSucc (DD (D5 a)) (DE (D5 a))
TSucc (DD (D4 a)) (DE (D4 a))
TSucc (DD (D3 a)) (DE (D3 a))
TSucc (DD (D2 a)) (DE (D2 a))
TSucc (DD (D1 a)) (DE (D1 a))
TSucc (DD (D0 a)) (DE (D0 a))
TSucc (DC F) (DD F)
TSucc (DC T) (DD T)
TSucc (DC (DF a)) (DD (DF a))
TSucc (DC (DE a)) (DD (DE a))
TSucc (DC (DD a)) (DD (DD a))
TSucc (DC (DC a)) (DD (DC a))
TSucc (DC (DB a)) (DD (DB a))
TSucc (DC (DA a)) (DD (DA a))
TSucc (DC (D9 a)) (DD (D9 a))
TSucc (DC (D8 a)) (DD (D8 a))
TSucc (DC (D7 a)) (DD (D7 a))
TSucc (DC (D6 a)) (DD (D6 a))
TSucc (DC (D5 a)) (DD (D5 a))
TSucc (DC (D4 a)) (DD (D4 a))
TSucc (DC (D3 a)) (DD (D3 a))
TSucc (DC (D2 a)) (DD (D2 a))
TSucc (DC (D1 a)) (DD (D1 a))
TSucc (DC (D0 a)) (DD (D0 a))
TSucc (DB F) (DC F)
TSucc (DB T) (DC T)
TSucc (DB (DF a)) (DC (DF a))
TSucc (DB (DE a)) (DC (DE a))
TSucc (DB (DD a)) (DC (DD a))
TSucc (DB (DC a)) (DC (DC a))
TSucc (DB (DB a)) (DC (DB a))
TSucc (DB (DA a)) (DC (DA a))
TSucc (DB (D9 a)) (DC (D9 a))
TSucc (DB (D8 a)) (DC (D8 a))
TSucc (DB (D7 a)) (DC (D7 a))
TSucc (DB (D6 a)) (DC (D6 a))
TSucc (DB (D5 a)) (DC (D5 a))
TSucc (DB (D4 a)) (DC (D4 a))
TSucc (DB (D3 a)) (DC (D3 a))
TSucc (DB (D2 a)) (DC (D2 a))
TSucc (DB (D1 a)) (DC (D1 a))
TSucc (DB (D0 a)) (DC (D0 a))
TSucc (DA F) (DB F)
TSucc (DA T) (DB T)
TSucc (DA (DF a)) (DB (DF a))
TSucc (DA (DE a)) (DB (DE a))
TSucc (DA (DD a)) (DB (DD a))
TSucc (DA (DC a)) (DB (DC a))
TSucc (DA (DB a)) (DB (DB a))
TSucc (DA (DA a)) (DB (DA a))
TSucc (DA (D9 a)) (DB (D9 a))
TSucc (DA (D8 a)) (DB (D8 a))
TSucc (DA (D7 a)) (DB (D7 a))
TSucc (DA (D6 a)) (DB (D6 a))
TSucc (DA (D5 a)) (DB (D5 a))
TSucc (DA (D4 a)) (DB (D4 a))
TSucc (DA (D3 a)) (DB (D3 a))
TSucc (DA (D2 a)) (DB (D2 a))
TSucc (DA (D1 a)) (DB (D1 a))
TSucc (DA (D0 a)) (DB (D0 a))
TSucc (D9 F) (DA F)
TSucc (D9 T) (DA T)
TSucc (D9 (DF a)) (DA (DF a))
TSucc (D9 (DE a)) (DA (DE a))
TSucc (D9 (DD a)) (DA (DD a))
TSucc (D9 (DC a)) (DA (DC a))
TSucc (D9 (DB a)) (DA (DB a))
TSucc (D9 (DA a)) (DA (DA a))
TSucc (D9 (D9 a)) (DA (D9 a))
TSucc (D9 (D8 a)) (DA (D8 a))
TSucc (D9 (D7 a)) (DA (D7 a))
TSucc (D9 (D6 a)) (DA (D6 a))
TSucc (D9 (D5 a)) (DA (D5 a))
TSucc (D9 (D4 a)) (DA (D4 a))
TSucc (D9 (D3 a)) (DA (D3 a))
TSucc (D9 (D2 a)) (DA (D2 a))
TSucc (D9 (D1 a)) (DA (D1 a))
TSucc (D9 (D0 a)) (DA (D0 a))
TSucc (D8 F) (D9 F)
TSucc (D8 T) (D9 T)
TSucc (D8 (DF a)) (D9 (DF a))
TSucc (D8 (DE a)) (D9 (DE a))
TSucc (D8 (DD a)) (D9 (DD a))
TSucc (D8 (DC a)) (D9 (DC a))
TSucc (D8 (DB a)) (D9 (DB a))
TSucc (D8 (DA a)) (D9 (DA a))
TSucc (D8 (D9 a)) (D9 (D9 a))
TSucc (D8 (D8 a)) (D9 (D8 a))
TSucc (D8 (D7 a)) (D9 (D7 a))
TSucc (D8 (D6 a)) (D9 (D6 a))
TSucc (D8 (D5 a)) (D9 (D5 a))
TSucc (D8 (D4 a)) (D9 (D4 a))
TSucc (D8 (D3 a)) (D9 (D3 a))
TSucc (D8 (D2 a)) (D9 (D2 a))
TSucc (D8 (D1 a)) (D9 (D1 a))
TSucc (D8 (D0 a)) (D9 (D0 a))
TSucc (D7 F) (D8 F)
TSucc (D7 T) (D8 T)
TSucc (D7 (DF a)) (D8 (DF a))
TSucc (D7 (DE a)) (D8 (DE a))
TSucc (D7 (DD a)) (D8 (DD a))
TSucc (D7 (DC a)) (D8 (DC a))
TSucc (D7 (DB a)) (D8 (DB a))
TSucc (D7 (DA a)) (D8 (DA a))
TSucc (D7 (D9 a)) (D8 (D9 a))
TSucc (D7 (D8 a)) (D8 (D8 a))
TSucc (D7 (D7 a)) (D8 (D7 a))
TSucc (D7 (D6 a)) (D8 (D6 a))
TSucc (D7 (D5 a)) (D8 (D5 a))
TSucc (D7 (D4 a)) (D8 (D4 a))
TSucc (D7 (D3 a)) (D8 (D3 a))
TSucc (D7 (D2 a)) (D8 (D2 a))
TSucc (D7 (D1 a)) (D8 (D1 a))
TSucc (D7 (D0 a)) (D8 (D0 a))
TSucc (D6 F) (D7 F)
TSucc (D6 T) (D7 T)
TSucc (D6 (DF a)) (D7 (DF a))
TSucc (D6 (DE a)) (D7 (DE a))
TSucc (D6 (DD a)) (D7 (DD a))
TSucc (D6 (DC a)) (D7 (DC a))
TSucc (D6 (DB a)) (D7 (DB a))
TSucc (D6 (DA a)) (D7 (DA a))
TSucc (D6 (D9 a)) (D7 (D9 a))
TSucc (D6 (D8 a)) (D7 (D8 a))
TSucc (D6 (D7 a)) (D7 (D7 a))
TSucc (D6 (D6 a)) (D7 (D6 a))
TSucc (D6 (D5 a)) (D7 (D5 a))
TSucc (D6 (D4 a)) (D7 (D4 a))
TSucc (D6 (D3 a)) (D7 (D3 a))
TSucc (D6 (D2 a)) (D7 (D2 a))
TSucc (D6 (D1 a)) (D7 (D1 a))
TSucc (D6 (D0 a)) (D7 (D0 a))
TSucc (D5 F) (D6 F)
TSucc (D5 T) (D6 T)
TSucc (D5 (DF a)) (D6 (DF a))
TSucc (D5 (DE a)) (D6 (DE a))
TSucc (D5 (DD a)) (D6 (DD a))
TSucc (D5 (DC a)) (D6 (DC a))
TSucc (D5 (DB a)) (D6 (DB a))
TSucc (D5 (DA a)) (D6 (DA a))
TSucc (D5 (D9 a)) (D6 (D9 a))
TSucc (D5 (D8 a)) (D6 (D8 a))
TSucc (D5 (D7 a)) (D6 (D7 a))
TSucc (D5 (D6 a)) (D6 (D6 a))
TSucc (D5 (D5 a)) (D6 (D5 a))
TSucc (D5 (D4 a)) (D6 (D4 a))
TSucc (D5 (D3 a)) (D6 (D3 a))
TSucc (D5 (D2 a)) (D6 (D2 a))
TSucc (D5 (D1 a)) (D6 (D1 a))
TSucc (D5 (D0 a)) (D6 (D0 a))
TSucc (D4 F) (D5 F)
TSucc (D4 T) (D5 T)
TSucc (D4 (DF a)) (D5 (DF a))
TSucc (D4 (DE a)) (D5 (DE a))
TSucc (D4 (DD a)) (D5 (DD a))
TSucc (D4 (DC a)) (D5 (DC a))
TSucc (D4 (DB a)) (D5 (DB a))
TSucc (D4 (DA a)) (D5 (DA a))
TSucc (D4 (D9 a)) (D5 (D9 a))
TSucc (D4 (D8 a)) (D5 (D8 a))
TSucc (D4 (D7 a)) (D5 (D7 a))
TSucc (D4 (D6 a)) (D5 (D6 a))
TSucc (D4 (D5 a)) (D5 (D5 a))
TSucc (D4 (D4 a)) (D5 (D4 a))
TSucc (D4 (D3 a)) (D5 (D3 a))
TSucc (D4 (D2 a)) (D5 (D2 a))
TSucc (D4 (D1 a)) (D5 (D1 a))
TSucc (D4 (D0 a)) (D5 (D0 a))
TSucc (D3 F) (D4 F)
TSucc (D3 T) (D4 T)
TSucc (D3 (DF a)) (D4 (DF a))
TSucc (D3 (DE a)) (D4 (DE a))
TSucc (D3 (DD a)) (D4 (DD a))
TSucc (D3 (DC a)) (D4 (DC a))
TSucc (D3 (DB a)) (D4 (DB a))
TSucc (D3 (DA a)) (D4 (DA a))
TSucc (D3 (D9 a)) (D4 (D9 a))
TSucc (D3 (D8 a)) (D4 (D8 a))
TSucc (D3 (D7 a)) (D4 (D7 a))
TSucc (D3 (D6 a)) (D4 (D6 a))
TSucc (D3 (D5 a)) (D4 (D5 a))
TSucc (D3 (D4 a)) (D4 (D4 a))
TSucc (D3 (D3 a)) (D4 (D3 a))
TSucc (D3 (D2 a)) (D4 (D2 a))
TSucc (D3 (D1 a)) (D4 (D1 a))
TSucc (D3 (D0 a)) (D4 (D0 a))
TSucc (D2 F) (D3 F)
TSucc (D2 T) (D3 T)
TSucc (D2 (DF a)) (D3 (DF a))
TSucc (D2 (DE a)) (D3 (DE a))
TSucc (D2 (DD a)) (D3 (DD a))
TSucc (D2 (DC a)) (D3 (DC a))
TSucc (D2 (DB a)) (D3 (DB a))
TSucc (D2 (DA a)) (D3 (DA a))
TSucc (D2 (D9 a)) (D3 (D9 a))
TSucc (D2 (D8 a)) (D3 (D8 a))
TSucc (D2 (D7 a)) (D3 (D7 a))
TSucc (D2 (D6 a)) (D3 (D6 a))
TSucc (D2 (D5 a)) (D3 (D5 a))
TSucc (D2 (D4 a)) (D3 (D4 a))
TSucc (D2 (D3 a)) (D3 (D3 a))
TSucc (D2 (D2 a)) (D3 (D2 a))
TSucc (D2 (D1 a)) (D3 (D1 a))
TSucc (D2 (D0 a)) (D3 (D0 a))
TSucc (D1 F) (D2 F)
TSucc (D1 T) (D2 T)
TSucc (D1 (DF a)) (D2 (DF a))
TSucc (D1 (DE a)) (D2 (DE a))
TSucc (D1 (DD a)) (D2 (DD a))
TSucc (D1 (DC a)) (D2 (DC a))
TSucc (D1 (DB a)) (D2 (DB a))
TSucc (D1 (DA a)) (D2 (DA a))
TSucc (D1 (D9 a)) (D2 (D9 a))
TSucc (D1 (D8 a)) (D2 (D8 a))
TSucc (D1 (D7 a)) (D2 (D7 a))
TSucc (D1 (D6 a)) (D2 (D6 a))
TSucc (D1 (D5 a)) (D2 (D5 a))
TSucc (D1 (D4 a)) (D2 (D4 a))
TSucc (D1 (D3 a)) (D2 (D3 a))
TSucc (D1 (D2 a)) (D2 (D2 a))
TSucc (D1 (D1 a)) (D2 (D1 a))
TSucc (D1 (D0 a)) (D2 (D0 a))
TSucc (D0 T) (D1 T)
TSucc (D0 (DF a)) (D1 (DF a))
TSucc (D0 (DE a)) (D1 (DE a))
TSucc (D0 (DD a)) (D1 (DD a))
TSucc (D0 (DC a)) (D1 (DC a))
TSucc (D0 (DB a)) (D1 (DB a))
TSucc (D0 (DA a)) (D1 (DA a))
TSucc (D0 (D9 a)) (D1 (D9 a))
TSucc (D0 (D8 a)) (D1 (D8 a))
TSucc (D0 (D7 a)) (D1 (D7 a))
TSucc (D0 (D6 a)) (D1 (D6 a))
TSucc (D0 (D5 a)) (D1 (D5 a))
TSucc (D0 (D4 a)) (D1 (D4 a))
TSucc (D0 (D3 a)) (D1 (D3 a))
TSucc (D0 (D2 a)) (D1 (D2 a))
TSucc (D0 (D1 a)) (D1 (D1 a))
TSucc (D0 (D0 a)) (D1 (D0 a))

class TAddC' a b c d | a b c -> dSource

Instances

TAddC' F F F F
TAddC' F T F T
TAddC' F T T F
TAddC' T F F T
TAddC' T F T F
TAddC' T T T T
TAddC' F F T (D1 F)
TAddC' T T F (DE T)
TSucc a b => TAddC' F (DF a) T (D0 b)
TAddC' F (DF a) F (DF a)
TAddC' F (DE a) F (DE a)
TAddC' F (DE a) T (DF a)
TAddC' F (DD a) F (DD a)
TAddC' F (DD a) T (DE a)
TAddC' F (DC a) F (DC a)
TAddC' F (DC a) T (DD a)
TAddC' F (DB a) F (DB a)
TAddC' F (DB a) T (DC a)
TAddC' F (DA a) F (DA a)
TAddC' F (DA a) T (DB a)
TAddC' F (D9 a) F (D9 a)
TAddC' F (D9 a) T (DA a)
TAddC' F (D8 a) F (D8 a)
TAddC' F (D8 a) T (D9 a)
TAddC' F (D7 a) F (D7 a)
TAddC' F (D7 a) T (D8 a)
TAddC' F (D6 a) F (D6 a)
TAddC' F (D6 a) T (D7 a)
TAddC' F (D5 a) F (D5 a)
TAddC' F (D5 a) T (D6 a)
TAddC' F (D4 a) F (D4 a)
TAddC' F (D4 a) T (D5 a)
TAddC' F (D3 a) F (D3 a)
TAddC' F (D3 a) T (D4 a)
TAddC' F (D2 a) F (D2 a)
TAddC' F (D2 a) T (D3 a)
TAddC' F (D1 a) F (D1 a)
TAddC' F (D1 a) T (D2 a)
TAddC' F (D0 a) F (D0 a)
TAddC' F (D0 a) T (D1 a)
TAddC' T (DF a) T (DF a)
TAddC' T (DF a) F (DE a)
TAddC' T (DE a) T (DE a)
TAddC' T (DE a) F (DD a)
TAddC' T (DD a) T (DD a)
TAddC' T (DD a) F (DC a)
TAddC' T (DC a) T (DC a)
TAddC' T (DC a) F (DB a)
TAddC' T (DB a) T (DB a)
TAddC' T (DB a) F (DA a)
TAddC' T (DA a) T (DA a)
TAddC' T (DA a) F (D9 a)
TAddC' T (D9 a) T (D9 a)
TAddC' T (D9 a) F (D8 a)
TAddC' T (D8 a) T (D8 a)
TAddC' T (D8 a) F (D7 a)
TAddC' T (D7 a) T (D7 a)
TAddC' T (D7 a) F (D6 a)
TAddC' T (D6 a) T (D6 a)
TAddC' T (D6 a) F (D5 a)
TAddC' T (D5 a) T (D5 a)
TAddC' T (D5 a) F (D4 a)
TAddC' T (D4 a) T (D4 a)
TAddC' T (D4 a) F (D3 a)
TAddC' T (D3 a) T (D3 a)
TAddC' T (D3 a) F (D2 a)
TAddC' T (D2 a) T (D2 a)
TAddC' T (D2 a) F (D1 a)
TAddC' T (D1 a) T (D1 a)
TAddC' T (D1 a) F (D0 a)
TSucc b a => TAddC' T (D0 a) F (DF b)
TAddC' T (D0 a) T (D0 a)
TSucc a b => TAddC' (DF a) F T (D0 b)
TAddC' (DF a) F F (DF a)
TAddC' (DF a) T T (DF a)
TAddC' (DF a) T F (DE a)
TAddC' (DE a) F F (DE a)
TAddC' (DE a) T T (DE a)
TAddC' (DE a) F T (DF a)
TAddC' (DE a) T F (DD a)
TAddC' (DD a) F F (DD a)
TAddC' (DD a) T T (DD a)
TAddC' (DD a) F T (DE a)
TAddC' (DD a) T F (DC a)
TAddC' (DC a) F F (DC a)
TAddC' (DC a) T T (DC a)
TAddC' (DC a) F T (DD a)
TAddC' (DC a) T F (DB a)
TAddC' (DB a) F F (DB a)
TAddC' (DB a) T T (DB a)
TAddC' (DB a) F T (DC a)
TAddC' (DB a) T F (DA a)
TAddC' (DA a) F F (DA a)
TAddC' (DA a) T T (DA a)
TAddC' (DA a) F T (DB a)
TAddC' (DA a) T F (D9 a)
TAddC' (D9 a) F F (D9 a)
TAddC' (D9 a) T T (D9 a)
TAddC' (D9 a) F T (DA a)
TAddC' (D9 a) T F (D8 a)
TAddC' (D8 a) F F (D8 a)
TAddC' (D8 a) T T (D8 a)
TAddC' (D8 a) F T (D9 a)
TAddC' (D8 a) T F (D7 a)
TAddC' (D7 a) F F (D7 a)
TAddC' (D7 a) T T (D7 a)
TAddC' (D7 a) F T (D8 a)
TAddC' (D7 a) T F (D6 a)
TAddC' (D6 a) F F (D6 a)
TAddC' (D6 a) T T (D6 a)
TAddC' (D6 a) F T (D7 a)
TAddC' (D6 a) T F (D5 a)
TAddC' (D5 a) F F (D5 a)
TAddC' (D5 a) T T (D5 a)
TAddC' (D5 a) F T (D6 a)
TAddC' (D5 a) T F (D4 a)
TAddC' (D4 a) F F (D4 a)
TAddC' (D4 a) T T (D4 a)
TAddC' (D4 a) F T (D5 a)
TAddC' (D4 a) T F (D3 a)
TAddC' (D3 a) F F (D3 a)
TAddC' (D3 a) T T (D3 a)
TAddC' (D3 a) F T (D4 a)
TAddC' (D3 a) T F (D2 a)
TAddC' (D2 a) F F (D2 a)
TAddC' (D2 a) T T (D2 a)
TAddC' (D2 a) F T (D3 a)
TAddC' (D2 a) T F (D1 a)
TAddC' (D1 a) F F (D1 a)
TAddC' (D1 a) T T (D1 a)
TAddC' (D1 a) F T (D2 a)
TAddC' (D1 a) T F (D0 a)
TSucc b a => TAddC' (D0 a) T F (DF b)
TAddC' (D0 a) F F (D0 a)
TAddC' (D0 a) T T (D0 a)
TAddC' (D0 a) F T (D1 a)
TAddC' a b T c => TAddC' (DF a) (DF b) T (DF c)
TAddC' a b T c => TAddC' (DF a) (DF b) F (DE c)
TAddC' a b T c => TAddC' (DF a) (DE b) T (DE c)
TAddC' a b T c => TAddC' (DF a) (DE b) F (DD c)
TAddC' a b T c => TAddC' (DF a) (DD b) T (DD c)
TAddC' a b T c => TAddC' (DF a) (DD b) F (DC c)
TAddC' a b T c => TAddC' (DF a) (DC b) T (DC c)
TAddC' a b T c => TAddC' (DF a) (DC b) F (DB c)
TAddC' a b T c => TAddC' (DF a) (DB b) T (DB c)
TAddC' a b T c => TAddC' (DF a) (DB b) F (DA c)
TAddC' a b T c => TAddC' (DF a) (DA b) T (DA c)
TAddC' a b T c => TAddC' (DF a) (DA b) F (D9 c)
TAddC' a b T c => TAddC' (DF a) (D9 b) T (D9 c)
TAddC' a b T c => TAddC' (DF a) (D9 b) F (D8 c)
TAddC' a b T c => TAddC' (DF a) (D8 b) T (D8 c)
TAddC' a b T c => TAddC' (DF a) (D8 b) F (D7 c)
TAddC' a b T c => TAddC' (DF a) (D7 b) T (D7 c)
TAddC' a b T c => TAddC' (DF a) (D7 b) F (D6 c)
TAddC' a b T c => TAddC' (DF a) (D6 b) T (D6 c)
TAddC' a b T c => TAddC' (DF a) (D6 b) F (D5 c)
TAddC' a b T c => TAddC' (DF a) (D5 b) T (D5 c)
TAddC' a b T c => TAddC' (DF a) (D5 b) F (D4 c)
TAddC' a b T c => TAddC' (DF a) (D4 b) T (D4 c)
TAddC' a b T c => TAddC' (DF a) (D4 b) F (D3 c)
TAddC' a b T c => TAddC' (DF a) (D3 b) T (D3 c)
TAddC' a b T c => TAddC' (DF a) (D3 b) F (D2 c)
TAddC' a b T c => TAddC' (DF a) (D2 b) T (D2 c)
TAddC' a b T c => TAddC' (DF a) (D2 b) F (D1 c)
TAddC' a b T c => TAddC' (DF a) (D1 b) T (D1 c)
TAddC' a b T c => TAddC' (DF a) (D1 b) F (D0 c)
TAddC' a b T c => TAddC' (DF a) (D0 b) T (D0 c)
TAddC' a b F c => TAddC' (DF a) (D0 b) F (DF c)
TAddC' a b T c => TAddC' (DE a) (DF b) T (DE c)
TAddC' a b T c => TAddC' (DE a) (DF b) F (DD c)
TAddC' a b T c => TAddC' (DE a) (DE b) T (DD c)
TAddC' a b T c => TAddC' (DE a) (DE b) F (DC c)
TAddC' a b T c => TAddC' (DE a) (DD b) T (DC c)
TAddC' a b T c => TAddC' (DE a) (DD b) F (DB c)
TAddC' a b T c => TAddC' (DE a) (DC b) T (DB c)
TAddC' a b T c => TAddC' (DE a) (DC b) F (DA c)
TAddC' a b T c => TAddC' (DE a) (DB b) T (DA c)
TAddC' a b T c => TAddC' (DE a) (DB b) F (D9 c)
TAddC' a b T c => TAddC' (DE a) (DA b) T (D9 c)
TAddC' a b T c => TAddC' (DE a) (DA b) F (D8 c)
TAddC' a b T c => TAddC' (DE a) (D9 b) T (D8 c)
TAddC' a b T c => TAddC' (DE a) (D9 b) F (D7 c)
TAddC' a b T c => TAddC' (DE a) (D8 b) T (D7 c)
TAddC' a b T c => TAddC' (DE a) (D8 b) F (D6 c)
TAddC' a b T c => TAddC' (DE a) (D7 b) T (D6 c)
TAddC' a b T c => TAddC' (DE a) (D7 b) F (D5 c)
TAddC' a b T c => TAddC' (DE a) (D6 b) T (D5 c)
TAddC' a b T c => TAddC' (DE a) (D6 b) F (D4 c)
TAddC' a b T c => TAddC' (DE a) (D5 b) T (D4 c)
TAddC' a b T c => TAddC' (DE a) (D5 b) F (D3 c)
TAddC' a b T c => TAddC' (DE a) (D4 b) T (D3 c)
TAddC' a b T c => TAddC' (DE a) (D4 b) F (D2 c)
TAddC' a b T c => TAddC' (DE a) (D3 b) T (D2 c)
TAddC' a b T c => TAddC' (DE a) (D3 b) F (D1 c)
TAddC' a b T c => TAddC' (DE a) (D2 b) T (D1 c)
TAddC' a b T c => TAddC' (DE a) (D2 b) F (D0 c)
TAddC' a b T c => TAddC' (DE a) (D1 b) T (D0 c)
TAddC' a b F c => TAddC' (DE a) (D1 b) F (DF c)
TAddC' a b F c => TAddC' (DE a) (D0 b) T (DF c)
TAddC' a b F c => TAddC' (DE a) (D0 b) F (DE c)
TAddC' a b T c => TAddC' (DD a) (DF b) T (DD c)
TAddC' a b T c => TAddC' (DD a) (DF b) F (DC c)
TAddC' a b T c => TAddC' (DD a) (DE b) T (DC c)
TAddC' a b T c => TAddC' (DD a) (DE b) F (DB c)
TAddC' a b T c => TAddC' (DD a) (DD b) T (DB c)
TAddC' a b T c => TAddC' (DD a) (DD b) F (DA c)
TAddC' a b T c => TAddC' (DD a) (DC b) T (DA c)
TAddC' a b T c => TAddC' (DD a) (DC b) F (D9 c)
TAddC' a b T c => TAddC' (DD a) (DB b) T (D9 c)
TAddC' a b T c => TAddC' (DD a) (DB b) F (D8 c)
TAddC' a b T c => TAddC' (DD a) (DA b) T (D8 c)
TAddC' a b T c => TAddC' (DD a) (DA b) F (D7 c)
TAddC' a b T c => TAddC' (DD a) (D9 b) T (D7 c)
TAddC' a b T c => TAddC' (DD a) (D9 b) F (D6 c)
TAddC' a b T c => TAddC' (DD a) (D8 b) T (D6 c)
TAddC' a b T c => TAddC' (DD a) (D8 b) F (D5 c)
TAddC' a b T c => TAddC' (DD a) (D7 b) T (D5 c)
TAddC' a b T c => TAddC' (DD a) (D7 b) F (D4 c)
TAddC' a b T c => TAddC' (DD a) (D6 b) T (D4 c)
TAddC' a b T c => TAddC' (DD a) (D6 b) F (D3 c)
TAddC' a b T c => TAddC' (DD a) (D5 b) T (D3 c)
TAddC' a b T c => TAddC' (DD a) (D5 b) F (D2 c)
TAddC' a b T c => TAddC' (DD a) (D4 b) T (D2 c)
TAddC' a b T c => TAddC' (DD a) (D4 b) F (D1 c)
TAddC' a b T c => TAddC' (DD a) (D3 b) T (D1 c)
TAddC' a b T c => TAddC' (DD a) (D3 b) F (D0 c)
TAddC' a b T c => TAddC' (DD a) (D2 b) T (D0 c)
TAddC' a b F c => TAddC' (DD a) (D2 b) F (DF c)
TAddC' a b F c => TAddC' (DD a) (D1 b) T (DF c)
TAddC' a b F c => TAddC' (DD a) (D1 b) F (DE c)
TAddC' a b F c => TAddC' (DD a) (D0 b) T (DE c)
TAddC' a b F c => TAddC' (DD a) (D0 b) F (DD c)
TAddC' a b T c => TAddC' (DC a) (DF b) T (DC c)
TAddC' a b T c => TAddC' (DC a) (DF b) F (DB c)
TAddC' a b T c => TAddC' (DC a) (DE b) T (DB c)
TAddC' a b T c => TAddC' (DC a) (DE b) F (DA c)
TAddC' a b T c => TAddC' (DC a) (DD b) T (DA c)
TAddC' a b T c => TAddC' (DC a) (DD b) F (D9 c)
TAddC' a b T c => TAddC' (DC a) (DC b) T (D9 c)
TAddC' a b T c => TAddC' (DC a) (DC b) F (D8 c)
TAddC' a b T c => TAddC' (DC a) (DB b) T (D8 c)
TAddC' a b T c => TAddC' (DC a) (DB b) F (D7 c)
TAddC' a b T c => TAddC' (DC a) (DA b) T (D7 c)
TAddC' a b T c => TAddC' (DC a) (DA b) F (D6 c)
TAddC' a b T c => TAddC' (DC a) (D9 b) T (D6 c)
TAddC' a b T c => TAddC' (DC a) (D9 b) F (D5 c)
TAddC' a b T c => TAddC' (DC a) (D8 b) T (D5 c)
TAddC' a b T c => TAddC' (DC a) (D8 b) F (D4 c)
TAddC' a b T c => TAddC' (DC a) (D7 b) T (D4 c)
TAddC' a b T c => TAddC' (DC a) (D7 b) F (D3 c)
TAddC' a b T c => TAddC' (DC a) (D6 b) T (D3 c)
TAddC' a b T c => TAddC' (DC a) (D6 b) F (D2 c)
TAddC' a b T c => TAddC' (DC a) (D5 b) T (D2 c)
TAddC' a b T c => TAddC' (DC a) (D5 b) F (D1 c)
TAddC' a b T c => TAddC' (DC a) (D4 b) T (D1 c)
TAddC' a b T c => TAddC' (DC a) (D4 b) F (D0 c)
TAddC' a b T c => TAddC' (DC a) (D3 b) T (D0 c)
TAddC' a b F c => TAddC' (DC a) (D3 b) F (DF c)
TAddC' a b F c => TAddC' (DC a) (D2 b) T (DF c)
TAddC' a b F c => TAddC' (DC a) (D2 b) F (DE c)
TAddC' a b F c => TAddC' (DC a) (D1 b) T (DE c)
TAddC' a b F c => TAddC' (DC a) (D1 b) F (DD c)
TAddC' a b F c => TAddC' (DC a) (D0 b) T (DD c)
TAddC' a b F c => TAddC' (DC a) (D0 b) F (DC c)
TAddC' a b T c => TAddC' (DB a) (DF b) T (DB c)
TAddC' a b T c => TAddC' (DB a) (DF b) F (DA c)
TAddC' a b T c => TAddC' (DB a) (DE b) T (DA c)
TAddC' a b T c => TAddC' (DB a) (DE b) F (D9 c)
TAddC' a b T c => TAddC' (DB a) (DD b) T (D9 c)
TAddC' a b T c => TAddC' (DB a) (DD b) F (D8 c)
TAddC' a b T c => TAddC' (DB a) (DC b) T (D8 c)
TAddC' a b T c => TAddC' (DB a) (DC b) F (D7 c)
TAddC' a b T c => TAddC' (DB a) (DB b) T (D7 c)
TAddC' a b T c => TAddC' (DB a) (DB b) F (D6 c)
TAddC' a b T c => TAddC' (DB a) (DA b) T (D6 c)
TAddC' a b T c => TAddC' (DB a) (DA b) F (D5 c)
TAddC' a b T c => TAddC' (DB a) (D9 b) T (D5 c)
TAddC' a b T c => TAddC' (DB a) (D9 b) F (D4 c)
TAddC' a b T c => TAddC' (DB a) (D8 b) T (D4 c)
TAddC' a b T c => TAddC' (DB a) (D8 b) F (D3 c)
TAddC' a b T c => TAddC' (DB a) (D7 b) T (D3 c)
TAddC' a b T c => TAddC' (DB a) (D7 b) F (D2 c)
TAddC' a b T c => TAddC' (DB a) (D6 b) T (D2 c)
TAddC' a b T c => TAddC' (DB a) (D6 b) F (D1 c)
TAddC' a b T c => TAddC' (DB a) (D5 b) T (D1 c)
TAddC' a b T c => TAddC' (DB a) (D5 b) F (D0 c)
TAddC' a b T c => TAddC' (DB a) (D4 b) T (D0 c)
TAddC' a b F c => TAddC' (DB a) (D4 b) F (DF c)
TAddC' a b F c => TAddC' (DB a) (D3 b) T (DF c)
TAddC' a b F c => TAddC' (DB a) (D3 b) F (DE c)
TAddC' a b F c => TAddC' (DB a) (D2 b) T (DE c)
TAddC' a b F c => TAddC' (DB a) (D2 b) F (DD c)
TAddC' a b F c => TAddC' (DB a) (D1 b) T (DD c)
TAddC' a b F c => TAddC' (DB a) (D1 b) F (DC c)
TAddC' a b F c => TAddC' (DB a) (D0 b) T (DC c)
TAddC' a b F c => TAddC' (DB a) (D0 b) F (DB c)
TAddC' a b T c => TAddC' (DA a) (DF b) T (DA c)
TAddC' a b T c => TAddC' (DA a) (DF b) F (D9 c)
TAddC' a b T c => TAddC' (DA a) (DE b) T (D9 c)
TAddC' a b T c => TAddC' (DA a) (DE b) F (D8 c)
TAddC' a b T c => TAddC' (DA a) (DD b) T (D8 c)
TAddC' a b T c => TAddC' (DA a) (DD b) F (D7 c)
TAddC' a b T c => TAddC' (DA a) (DC b) T (D7 c)
TAddC' a b T c => TAddC' (DA a) (DC b) F (D6 c)
TAddC' a b T c => TAddC' (DA a) (DB b) T (D6 c)
TAddC' a b T c => TAddC' (DA a) (DB b) F (D5 c)
TAddC' a b T c => TAddC' (DA a) (DA b) T (D5 c)
TAddC' a b T c => TAddC' (DA a) (DA b) F (D4 c)
TAddC' a b T c => TAddC' (DA a) (D9 b) T (D4 c)
TAddC' a b T c => TAddC' (DA a) (D9 b) F (D3 c)
TAddC' a b T c => TAddC' (DA a) (D8 b) T (D3 c)
TAddC' a b T c => TAddC' (DA a) (D8 b) F (D2 c)
TAddC' a b T c => TAddC' (DA a) (D7 b) T (D2 c)
TAddC' a b T c => TAddC' (DA a) (D7 b) F (D1 c)
TAddC' a b T c => TAddC' (DA a) (D6 b) T (D1 c)
TAddC' a b T c => TAddC' (DA a) (D6 b) F (D0 c)
TAddC' a b T c => TAddC' (DA a) (D5 b) T (D0 c)
TAddC' a b F c => TAddC' (DA a) (D5 b) F (DF c)
TAddC' a b F c => TAddC' (DA a) (D4 b) T (DF c)
TAddC' a b F c => TAddC' (DA a) (D4 b) F (DE c)
TAddC' a b F c => TAddC' (DA a) (D3 b) T (DE c)
TAddC' a b F c => TAddC' (DA a) (D3 b) F (DD c)
TAddC' a b F c => TAddC' (DA a) (D2 b) T (DD c)
TAddC' a b F c => TAddC' (DA a) (D2 b) F (DC c)
TAddC' a b F c => TAddC' (DA a) (D1 b) T (DC c)
TAddC' a b F c => TAddC' (DA a) (D1 b) F (DB c)
TAddC' a b F c => TAddC' (DA a) (D0 b) T (DB c)
TAddC' a b F c => TAddC' (DA a) (D0 b) F (DA c)
TAddC' a b T c => TAddC' (D9 a) (DF b) T (D9 c)
TAddC' a b T c => TAddC' (D9 a) (DF b) F (D8 c)
TAddC' a b T c => TAddC' (D9 a) (DE b) T (D8 c)
TAddC' a b T c => TAddC' (D9 a) (DE b) F (D7 c)
TAddC' a b T c => TAddC' (D9 a) (DD b) T (D7 c)
TAddC' a b T c => TAddC' (D9 a) (DD b) F (D6 c)
TAddC' a b T c => TAddC' (D9 a) (DC b) T (D6 c)
TAddC' a b T c => TAddC' (D9 a) (DC b) F (D5 c)
TAddC' a b T c => TAddC' (D9 a) (DB b) T (D5 c)
TAddC' a b T c => TAddC' (D9 a) (DB b) F (D4 c)
TAddC' a b T c => TAddC' (D9 a) (DA b) T (D4 c)
TAddC' a b T c => TAddC' (D9 a) (DA b) F (D3 c)
TAddC' a b T c => TAddC' (D9 a) (D9 b) T (D3 c)
TAddC' a b T c => TAddC' (D9 a) (D9 b) F (D2 c)
TAddC' a b T c => TAddC' (D9 a) (D8 b) T (D2 c)
TAddC' a b T c => TAddC' (D9 a) (D8 b) F (D1 c)
TAddC' a b T c => TAddC' (D9 a) (D7 b) T (D1 c)
TAddC' a b T c => TAddC' (D9 a) (D7 b) F (D0 c)
TAddC' a b T c => TAddC' (D9 a) (D6 b) T (D0 c)
TAddC' a b F c => TAddC' (D9 a) (D6 b) F (DF c)
TAddC' a b F c => TAddC' (D9 a) (D5 b) T (DF c)
TAddC' a b F c => TAddC' (D9 a) (D5 b) F (DE c)
TAddC' a b F c => TAddC' (D9 a) (D4 b) T (DE c)
TAddC' a b F c => TAddC' (D9 a) (D4 b) F (DD c)
TAddC' a b F c => TAddC' (D9 a) (D3 b) T (DD c)
TAddC' a b F c => TAddC' (D9 a) (D3 b) F (DC c)
TAddC' a b F c => TAddC' (D9 a) (D2 b) T (DC c)
TAddC' a b F c => TAddC' (D9 a) (D2 b) F (DB c)
TAddC' a b F c => TAddC' (D9 a) (D1 b) T (DB c)
TAddC' a b F c => TAddC' (D9 a) (D1 b) F (DA c)
TAddC' a b F c => TAddC' (D9 a) (D0 b) T (DA c)
TAddC' a b F c => TAddC' (D9 a) (D0 b) F (D9 c)
TAddC' a b T c => TAddC' (D8 a) (DF b) T (D8 c)
TAddC' a b T c => TAddC' (D8 a) (DF b) F (D7 c)
TAddC' a b T c => TAddC' (D8 a) (DE b) T (D7 c)
TAddC' a b T c => TAddC' (D8 a) (DE b) F (D6 c)
TAddC' a b T c => TAddC' (D8 a) (DD b) T (D6 c)
TAddC' a b T c => TAddC' (D8 a) (DD b) F (D5 c)
TAddC' a b T c => TAddC' (D8 a) (DC b) T (D5 c)
TAddC' a b T c => TAddC' (D8 a) (DC b) F (D4 c)
TAddC' a b T c => TAddC' (D8 a) (DB b) T (D4 c)
TAddC' a b T c => TAddC' (D8 a) (DB b) F (D3 c)
TAddC' a b T c => TAddC' (D8 a) (DA b) T (D3 c)
TAddC' a b T c => TAddC' (D8 a) (DA b) F (D2 c)
TAddC' a b T c => TAddC' (D8 a) (D9 b) T (D2 c)
TAddC' a b T c => TAddC' (D8 a) (D9 b) F (D1 c)
TAddC' a b T c => TAddC' (D8 a) (D8 b) T (D1 c)
TAddC' a b T c => TAddC' (D8 a) (D8 b) F (D0 c)
TAddC' a b T c => TAddC' (D8 a) (D7 b) T (D0 c)
TAddC' a b F c => TAddC' (D8 a) (D7 b) F (DF c)
TAddC' a b F c => TAddC' (D8 a) (D6 b) T (DF c)
TAddC' a b F c => TAddC' (D8 a) (D6 b) F (DE c)
TAddC' a b F c => TAddC' (D8 a) (D5 b) T (DE c)
TAddC' a b F c => TAddC' (D8 a) (D5 b) F (DD c)
TAddC' a b F c => TAddC' (D8 a) (D4 b) T (DD c)
TAddC' a b F c => TAddC' (D8 a) (D4 b) F (DC c)
TAddC' a b F c => TAddC' (D8 a) (D3 b) T (DC c)
TAddC' a b F c => TAddC' (D8 a) (D3 b) F (DB c)
TAddC' a b F c => TAddC' (D8 a) (D2 b) T (DB c)
TAddC' a b F c => TAddC' (D8 a) (D2 b) F (DA c)
TAddC' a b F c => TAddC' (D8 a) (D1 b) T (DA c)
TAddC' a b F c => TAddC' (D8 a) (D1 b) F (D9 c)
TAddC' a b F c => TAddC' (D8 a) (D0 b) T (D9 c)
TAddC' a b F c => TAddC' (D8 a) (D0 b) F (D8 c)
TAddC' a b T c => TAddC' (D7 a) (DF b) T (D7 c)
TAddC' a b T c => TAddC' (D7 a) (DF b) F (D6 c)
TAddC' a b T c => TAddC' (D7 a) (DE b) T (D6 c)
TAddC' a b T c => TAddC' (D7 a) (DE b) F (D5 c)
TAddC' a b T c => TAddC' (D7 a) (DD b) T (D5 c)
TAddC' a b T c => TAddC' (D7 a) (DD b) F (D4 c)
TAddC' a b T c => TAddC' (D7 a) (DC b) T (D4 c)
TAddC' a b T c => TAddC' (D7 a) (DC b) F (D3 c)
TAddC' a b T c => TAddC' (D7 a) (DB b) T (D3 c)
TAddC' a b T c => TAddC' (D7 a) (DB b) F (D2 c)
TAddC' a b T c => TAddC' (D7 a) (DA b) T (D2 c)
TAddC' a b T c => TAddC' (D7 a) (DA b) F (D1 c)
TAddC' a b T c => TAddC' (D7 a) (D9 b) T (D1 c)
TAddC' a b T c => TAddC' (D7 a) (D9 b) F (D0 c)
TAddC' a b T c => TAddC' (D7 a) (D8 b) T (D0 c)
TAddC' a b F c => TAddC' (D7 a) (D8 b) F (DF c)
TAddC' a b F c => TAddC' (D7 a) (D7 b) T (DF c)
TAddC' a b F c => TAddC' (D7 a) (D7 b) F (DE c)
TAddC' a b F c => TAddC' (D7 a) (D6 b) T (DE c)
TAddC' a b F c => TAddC' (D7 a) (D6 b) F (DD c)
TAddC' a b F c => TAddC' (D7 a) (D5 b) T (DD c)
TAddC' a b F c => TAddC' (D7 a) (D5 b) F (DC c)
TAddC' a b F c => TAddC' (D7 a) (D4 b) T (DC c)
TAddC' a b F c => TAddC' (D7 a) (D4 b) F (DB c)
TAddC' a b F c => TAddC' (D7 a) (D3 b) T (DB c)
TAddC' a b F c => TAddC' (D7 a) (D3 b) F (DA c)
TAddC' a b F c => TAddC' (D7 a) (D2 b) T (DA c)
TAddC' a b F c => TAddC' (D7 a) (D2 b) F (D9 c)
TAddC' a b F c => TAddC' (D7 a) (D1 b) T (D9 c)
TAddC' a b F c => TAddC' (D7 a) (D1 b) F (D8 c)
TAddC' a b F c => TAddC' (D7 a) (D0 b) T (D8 c)
TAddC' a b F c => TAddC' (D7 a) (D0 b) F (D7 c)
TAddC' a b T c => TAddC' (D6 a) (DF b) T (D6 c)
TAddC' a b T c => TAddC' (D6 a) (DF b) F (D5 c)
TAddC' a b T c => TAddC' (D6 a) (DE b) T (D5 c)
TAddC' a b T c => TAddC' (D6 a) (DE b) F (D4 c)
TAddC' a b T c => TAddC' (D6 a) (DD b) T (D4 c)
TAddC' a b T c => TAddC' (D6 a) (DD b) F (D3 c)
TAddC' a b T c => TAddC' (D6 a) (DC b) T (D3 c)
TAddC' a b T c => TAddC' (D6 a) (DC b) F (D2 c)
TAddC' a b T c => TAddC' (D6 a) (DB b) T (D2 c)
TAddC' a b T c => TAddC' (D6 a) (DB b) F (D1 c)
TAddC' a b T c => TAddC' (D6 a) (DA b) T (D1 c)
TAddC' a b T c => TAddC' (D6 a) (DA b) F (D0 c)
TAddC' a b T c => TAddC' (D6 a) (D9 b) T (D0 c)
TAddC' a b F c => TAddC' (D6 a) (D9 b) F (DF c)
TAddC' a b F c => TAddC' (D6 a) (D8 b) T (DF c)
TAddC' a b F c => TAddC' (D6 a) (D8 b) F (DE c)
TAddC' a b F c => TAddC' (D6 a) (D7 b) T (DE c)
TAddC' a b F c => TAddC' (D6 a) (D7 b) F (DD c)
TAddC' a b F c => TAddC' (D6 a) (D6 b) T (DD c)
TAddC' a b F c => TAddC' (D6 a) (D6 b) F (DC c)
TAddC' a b F c => TAddC' (D6 a) (D5 b) T (DC c)
TAddC' a b F c => TAddC' (D6 a) (D5 b) F (DB c)
TAddC' a b F c => TAddC' (D6 a) (D4 b) T (DB c)
TAddC' a b F c => TAddC' (D6 a) (D4 b) F (DA c)
TAddC' a b F c => TAddC' (D6 a) (D3 b) T (DA c)
TAddC' a b F c => TAddC' (D6 a) (D3 b) F (D9 c)
TAddC' a b F c => TAddC' (D6 a) (D2 b) T (D9 c)
TAddC' a b F c => TAddC' (D6 a) (D2 b) F (D8 c)
TAddC' a b F c => TAddC' (D6 a) (D1 b) T (D8 c)
TAddC' a b F c => TAddC' (D6 a) (D1 b) F (D7 c)
TAddC' a b F c => TAddC' (D6 a) (D0 b) T (D7 c)
TAddC' a b F c => TAddC' (D6 a) (D0 b) F (D6 c)
TAddC' a b T c => TAddC' (D5 a) (DF b) T (D5 c)
TAddC' a b T c => TAddC' (D5 a) (DF b) F (D4 c)
TAddC' a b T c => TAddC' (D5 a) (DE b) T (D4 c)
TAddC' a b T c => TAddC' (D5 a) (DE b) F (D3 c)
TAddC' a b T c => TAddC' (D5 a) (DD b) T (D3 c)
TAddC' a b T c => TAddC' (D5 a) (DD b) F (D2 c)
TAddC' a b T c => TAddC' (D5 a) (DC b) T (D2 c)
TAddC' a b T c => TAddC' (D5 a) (DC b) F (D1 c)
TAddC' a b T c => TAddC' (D5 a) (DB b) T (D1 c)
TAddC' a b T c => TAddC' (D5 a) (DB b) F (D0 c)
TAddC' a b T c => TAddC' (D5 a) (DA b) T (D0 c)
TAddC' a b F c => TAddC' (D5 a) (DA b) F (DF c)
TAddC' a b F c => TAddC' (D5 a) (D9 b) T (DF c)
TAddC' a b F c => TAddC' (D5 a) (D9 b) F (DE c)
TAddC' a b F c => TAddC' (D5 a) (D8 b) T (DE c)
TAddC' a b F c => TAddC' (D5 a) (D8 b) F (DD c)
TAddC' a b F c => TAddC' (D5 a) (D7 b) T (DD c)
TAddC' a b F c => TAddC' (D5 a) (D7 b) F (DC c)
TAddC' a b F c => TAddC' (D5 a) (D6 b) T (DC c)
TAddC' a b F c => TAddC' (D5 a) (D6 b) F (DB c)
TAddC' a b F c => TAddC' (D5 a) (D5 b) T (DB c)
TAddC' a b F c => TAddC' (D5 a) (D5 b) F (DA c)
TAddC' a b F c => TAddC' (D5 a) (D4 b) T (DA c)
TAddC' a b F c => TAddC' (D5 a) (D4 b) F (D9 c)
TAddC' a b F c => TAddC' (D5 a) (D3 b) T (D9 c)
TAddC' a b F c => TAddC' (D5 a) (D3 b) F (D8 c)
TAddC' a b F c => TAddC' (D5 a) (D2 b) T (D8 c)
TAddC' a b F c => TAddC' (D5 a) (D2 b) F (D7 c)
TAddC' a b F c => TAddC' (D5 a) (D1 b) T (D7 c)
TAddC' a b F c => TAddC' (D5 a) (D1 b) F (D6 c)
TAddC' a b F c => TAddC' (D5 a) (D0 b) T (D6 c)
TAddC' a b F c => TAddC' (D5 a) (D0 b) F (D5 c)
TAddC' a b T c => TAddC' (D4 a) (DF b) T (D4 c)
TAddC' a b T c => TAddC' (D4 a) (DF b) F (D3 c)
TAddC' a b T c => TAddC' (D4 a) (DE b) T (D3 c)
TAddC' a b T c => TAddC' (D4 a) (DE b) F (D2 c)
TAddC' a b T c => TAddC' (D4 a) (DD b) T (D2 c)
TAddC' a b T c => TAddC' (D4 a) (DD b) F (D1 c)
TAddC' a b T c => TAddC' (D4 a) (DC b) T (D1 c)
TAddC' a b T c => TAddC' (D4 a) (DC b) F (D0 c)
TAddC' a b T c => TAddC' (D4 a) (DB b) T (D0 c)
TAddC' a b F c => TAddC' (D4 a) (DB b) F (DF c)
TAddC' a b F c => TAddC' (D4 a) (DA b) T (DF c)
TAddC' a b F c => TAddC' (D4 a) (DA b) F (DE c)
TAddC' a b F c => TAddC' (D4 a) (D9 b) T (DE c)
TAddC' a b F c => TAddC' (D4 a) (D9 b) F (DD c)
TAddC' a b F c => TAddC' (D4 a) (D8 b) T (DD c)
TAddC' a b F c => TAddC' (D4 a) (D8 b) F (DC c)
TAddC' a b F c => TAddC' (D4 a) (D7 b) T (DC c)
TAddC' a b F c => TAddC' (D4 a) (D7 b) F (DB c)
TAddC' a b F c => TAddC' (D4 a) (D6 b) T (DB c)
TAddC' a b F c => TAddC' (D4 a) (D6 b) F (DA c)
TAddC' a b F c => TAddC' (D4 a) (D5 b) T (DA c)
TAddC' a b F c => TAddC' (D4 a) (D5 b) F (D9 c)
TAddC' a b F c => TAddC' (D4 a) (D4 b) T (D9 c)
TAddC' a b F c => TAddC' (D4 a) (D4 b) F (D8 c)
TAddC' a b F c => TAddC' (D4 a) (D3 b) T (D8 c)
TAddC' a b F c => TAddC' (D4 a) (D3 b) F (D7 c)
TAddC' a b F c => TAddC' (D4 a) (D2 b) T (D7 c)
TAddC' a b F c => TAddC' (D4 a) (D2 b) F (D6 c)
TAddC' a b F c => TAddC' (D4 a) (D1 b) T (D6 c)
TAddC' a b F c => TAddC' (D4 a) (D1 b) F (D5 c)
TAddC' a b F c => TAddC' (D4 a) (D0 b) T (D5 c)
TAddC' a b F c => TAddC' (D4 a) (D0 b) F (D4 c)
TAddC' a b T c => TAddC' (D3 a) (DF b) T (D3 c)
TAddC' a b T c => TAddC' (D3 a) (DF b) F (D2 c)
TAddC' a b T c => TAddC' (D3 a) (DE b) T (D2 c)
TAddC' a b T c => TAddC' (D3 a) (DE b) F (D1 c)
TAddC' a b T c => TAddC' (D3 a) (DD b) T (D1 c)
TAddC' a b T c => TAddC' (D3 a) (DD b) F (D0 c)
TAddC' a b T c => TAddC' (D3 a) (DC b) T (D0 c)
TAddC' a b F c => TAddC' (D3 a) (DC b) F (DF c)
TAddC' a b F c => TAddC' (D3 a) (DB b) T (DF c)
TAddC' a b F c => TAddC' (D3 a) (DB b) F (DE c)
TAddC' a b F c => TAddC' (D3 a) (DA b) T (DE c)
TAddC' a b F c => TAddC' (D3 a) (DA b) F (DD c)
TAddC' a b F c => TAddC' (D3 a) (D9 b) T (DD c)
TAddC' a b F c => TAddC' (D3 a) (D9 b) F (DC c)
TAddC' a b F c => TAddC' (D3 a) (D8 b) T (DC c)
TAddC' a b F c => TAddC' (D3 a) (D8 b) F (DB c)
TAddC' a b F c => TAddC' (D3 a) (D7 b) T (DB c)
TAddC' a b F c => TAddC' (D3 a) (D7 b) F (DA c)
TAddC' a b F c => TAddC' (D3 a) (D6 b) T (DA c)
TAddC' a b F c => TAddC' (D3 a) (D6 b) F (D9 c)
TAddC' a b F c => TAddC' (D3 a) (D5 b) T (D9 c)
TAddC' a b F c => TAddC' (D3 a) (D5 b) F (D8 c)
TAddC' a b F c => TAddC' (D3 a) (D4 b) T (D8 c)
TAddC' a b F c => TAddC' (D3 a) (D4 b) F (D7 c)
TAddC' a b F c => TAddC' (D3 a) (D3 b) T (D7 c)
TAddC' a b F c => TAddC' (D3 a) (D3 b) F (D6 c)
TAddC' a b F c => TAddC' (D3 a) (D2 b) T (D6 c)
TAddC' a b F c => TAddC' (D3 a) (D2 b) F (D5 c)
TAddC' a b F c => TAddC' (D3 a) (D1 b) T (D5 c)
TAddC' a b F c => TAddC' (D3 a) (D1 b) F (D4 c)
TAddC' a b F c => TAddC' (D3 a) (D0 b) T (D4 c)
TAddC' a b F c => TAddC' (D3 a) (D0 b) F (D3 c)
TAddC' a b T c => TAddC' (D2 a) (DF b) T (D2 c)
TAddC' a b T c => TAddC' (D2 a) (DF b) F (D1 c)
TAddC' a b T c => TAddC' (D2 a) (DE b) T (D1 c)
TAddC' a b T c => TAddC' (D2 a) (DE b) F (D0 c)
TAddC' a b T c => TAddC' (D2 a) (DD b) T (D0 c)
TAddC' a b F c => TAddC' (D2 a) (DD b) F (DF c)
TAddC' a b F c => TAddC' (D2 a) (DC b) T (DF c)
TAddC' a b F c => TAddC' (D2 a) (DC b) F (DE c)
TAddC' a b F c => TAddC' (D2 a) (DB b) T (DE c)
TAddC' a b F c => TAddC' (D2 a) (DB b) F (DD c)
TAddC' a b F c => TAddC' (D2 a) (DA b) T (DD c)
TAddC' a b F c => TAddC' (D2 a) (DA b) F (DC c)
TAddC' a b F c => TAddC' (D2 a) (D9 b) T (DC c)
TAddC' a b F c => TAddC' (D2 a) (D9 b) F (DB c)
TAddC' a b F c => TAddC' (D2 a) (D8 b) T (DB c)
TAddC' a b F c => TAddC' (D2 a) (D8 b) F (DA c)
TAddC' a b F c => TAddC' (D2 a) (D7 b) T (DA c)
TAddC' a b F c => TAddC' (D2 a) (D7 b) F (D9 c)
TAddC' a b F c => TAddC' (D2 a) (D6 b) T (D9 c)
TAddC' a b F c => TAddC' (D2 a) (D6 b) F (D8 c)
TAddC' a b F c => TAddC' (D2 a) (D5 b) T (D8 c)
TAddC' a b F c => TAddC' (D2 a) (D5 b) F (D7 c)
TAddC' a b F c => TAddC' (D2 a) (D4 b) T (D7 c)
TAddC' a b F c => TAddC' (D2 a) (D4 b) F (D6 c)
TAddC' a b F c => TAddC' (D2 a) (D3 b) T (D6 c)
TAddC' a b F c => TAddC' (D2 a) (D3 b) F (D5 c)
TAddC' a b F c => TAddC' (D2 a) (D2 b) T (D5 c)
TAddC' a b F c => TAddC' (D2 a) (D2 b) F (D4 c)
TAddC' a b F c => TAddC' (D2 a) (D1 b) T (D4 c)
TAddC' a b F c => TAddC' (D2 a) (D1 b) F (D3 c)
TAddC' a b F c => TAddC' (D2 a) (D0 b) T (D3 c)
TAddC' a b F c => TAddC' (D2 a) (D0 b) F (D2 c)
TAddC' a b T c => TAddC' (D1 a) (DF b) T (D1 c)
TAddC' a b T c => TAddC' (D1 a) (DF b) F (D0 c)
TAddC' a b T c => TAddC' (D1 a) (DE b) T (D0 c)
TAddC' a b F c => TAddC' (D1 a) (DE b) F (DF c)
TAddC' a b F c => TAddC' (D1 a) (DD b) T (DF c)
TAddC' a b F c => TAddC' (D1 a) (DD b) F (DE c)
TAddC' a b F c => TAddC' (D1 a) (DC b) T (DE c)
TAddC' a b F c => TAddC' (D1 a) (DC b) F (DD c)
TAddC' a b F c => TAddC' (D1 a) (DB b) T (DD c)
TAddC' a b F c => TAddC' (D1 a) (DB b) F (DC c)
TAddC' a b F c => TAddC' (D1 a) (DA b) T (DC c)
TAddC' a b F c => TAddC' (D1 a) (DA b) F (DB c)
TAddC' a b F c => TAddC' (D1 a) (D9 b) T (DB c)
TAddC' a b F c => TAddC' (D1 a) (D9 b) F (DA c)
TAddC' a b F c => TAddC' (D1 a) (D8 b) T (DA c)
TAddC' a b F c => TAddC' (D1 a) (D8 b) F (D9 c)
TAddC' a b F c => TAddC' (D1 a) (D7 b) T (D9 c)
TAddC' a b F c => TAddC' (D1 a) (D7 b) F (D8 c)
TAddC' a b F c => TAddC' (D1 a) (D6 b) T (D8 c)
TAddC' a b F c => TAddC' (D1 a) (D6 b) F (D7 c)
TAddC' a b F c => TAddC' (D1 a) (D5 b) T (D7 c)
TAddC' a b F c => TAddC' (D1 a) (D5 b) F (D6 c)
TAddC' a b F c => TAddC' (D1 a) (D4 b) T (D6 c)
TAddC' a b F c => TAddC' (D1 a) (D4 b) F (D5 c)
TAddC' a b F c => TAddC' (D1 a) (D3 b) T (D5 c)
TAddC' a b F c => TAddC' (D1 a) (D3 b) F (D4 c)
TAddC' a b F c => TAddC' (D1 a) (D2 b) T (D4 c)
TAddC' a b F c => TAddC' (D1 a) (D2 b) F (D3 c)
TAddC' a b F c => TAddC' (D1 a) (D1 b) T (D3 c)
TAddC' a b F c => TAddC' (D1 a) (D1 b) F (D2 c)
TAddC' a b F c => TAddC' (D1 a) (D0 b) T (D2 c)
TAddC' a b F c => TAddC' (D1 a) (D0 b) F (D1 c)
TAddC' a b T c => TAddC' (D0 a) (DF b) T (D0 c)
TAddC' a b F c => TAddC' (D0 a) (DF b) F (DF c)
TAddC' a b F c => TAddC' (D0 a) (DE b) T (DF c)
TAddC' a b F c => TAddC' (D0 a) (DE b) F (DE c)
TAddC' a b F c => TAddC' (D0 a) (DD b) T (DE c)
TAddC' a b F c => TAddC' (D0 a) (DD b) F (DD c)
TAddC' a b F c => TAddC' (D0 a) (DC b) T (DD c)
TAddC' a b F c => TAddC' (D0 a) (DC b) F (DC c)
TAddC' a b F c => TAddC' (D0 a) (DB b) T (DC c)
TAddC' a b F c => TAddC' (D0 a) (DB b) F (DB c)
TAddC' a b F c => TAddC' (D0 a) (DA b) T (DB c)
TAddC' a b F c => TAddC' (D0 a) (DA b) F (DA c)
TAddC' a b F c => TAddC' (D0 a) (D9 b) T (DA c)
TAddC' a b F c => TAddC' (D0 a) (D9 b) F (D9 c)
TAddC' a b F c => TAddC' (D0 a) (D8 b) T (D9 c)
TAddC' a b F c => TAddC' (D0 a) (D8 b) F (D8 c)
TAddC' a b F c => TAddC' (D0 a) (D7 b) T (D8 c)
TAddC' a b F c => TAddC' (D0 a) (D7 b) F (D7 c)
TAddC' a b F c => TAddC' (D0 a) (D6 b) T (D7 c)
TAddC' a b F c => TAddC' (D0 a) (D6 b) F (D6 c)
TAddC' a b F c => TAddC' (D0 a) (D5 b) T (D6 c)
TAddC' a b F c => TAddC' (D0 a) (D5 b) F (D5 c)
TAddC' a b F c => TAddC' (D0 a) (D4 b) T (D5 c)
TAddC' a b F c => TAddC' (D0 a) (D4 b) F (D4 c)
TAddC' a b F c => TAddC' (D0 a) (D3 b) T (D4 c)
TAddC' a b F c => TAddC' (D0 a) (D3 b) F (D3 c)
TAddC' a b F c => TAddC' (D0 a) (D2 b) T (D3 c)
TAddC' a b F c => TAddC' (D0 a) (D2 b) F (D2 c)
TAddC' a b F c => TAddC' (D0 a) (D1 b) T (D2 c)
TAddC' a b F c => TAddC' (D0 a) (D1 b) F (D1 c)
TAddC' a b F c => TAddC' (D0 a) (D0 b) T (D1 c)
TAddC' a b F c => TAddC' (D0 a) (D0 b) F (D0 c)

class TNF' a b c | a -> b cSource

Instances

TNF' F F F
TNF' T T F
TNF' (DF T) T F
(TNF' (DF a) c b, TIf b (DF c) T d) => TNF' (DF (DF a)) d b
TNF' (D0 F) F F
(TNF' (D0 a) c b, TIf b (D0 c) F d) => TNF' (D0 (D0 a)) d b
TNF' (DF F) (DF F) T
TNF' (DE a) c b => TNF' (DF (DE a)) (DF c) b
TNF' (DD a) c b => TNF' (DF (DD a)) (DF c) b
TNF' (DC a) c b => TNF' (DF (DC a)) (DF c) b
TNF' (DB a) c b => TNF' (DF (DB a)) (DF c) b
TNF' (DA a) c b => TNF' (DF (DA a)) (DF c) b
TNF' (D9 a) c b => TNF' (DF (D9 a)) (DF c) b
TNF' (D8 a) c b => TNF' (DF (D8 a)) (DF c) b
TNF' (D7 a) c b => TNF' (DF (D7 a)) (DF c) b
TNF' (D6 a) c b => TNF' (DF (D6 a)) (DF c) b
TNF' (D5 a) c b => TNF' (DF (D5 a)) (DF c) b
TNF' (D4 a) c b => TNF' (DF (D4 a)) (DF c) b
TNF' (D3 a) c b => TNF' (DF (D3 a)) (DF c) b
TNF' (D2 a) c b => TNF' (DF (D2 a)) (DF c) b
TNF' (D1 a) c b => TNF' (DF (D1 a)) (DF c) b
TNF' (D0 a) c b => TNF' (DF (D0 a)) (DF c) b
TNF' (DE F) (DE F) T
TNF' (DE T) (DE T) T
TNF' (DF a) c b => TNF' (DE (DF a)) (DE c) b
TNF' (DE a) c b => TNF' (DE (DE a)) (DE c) b
TNF' (DD a) c b => TNF' (DE (DD a)) (DE c) b
TNF' (DC a) c b => TNF' (DE (DC a)) (DE c) b
TNF' (DB a) c b => TNF' (DE (DB a)) (DE c) b
TNF' (DA a) c b => TNF' (DE (DA a)) (DE c) b
TNF' (D9 a) c b => TNF' (DE (D9 a)) (DE c) b
TNF' (D8 a) c b => TNF' (DE (D8 a)) (DE c) b
TNF' (D7 a) c b => TNF' (DE (D7 a)) (DE c) b
TNF' (D6 a) c b => TNF' (DE (D6 a)) (DE c) b
TNF' (D5 a) c b => TNF' (DE (D5 a)) (DE c) b
TNF' (D4 a) c b => TNF' (DE (D4 a)) (DE c) b
TNF' (D3 a) c b => TNF' (DE (D3 a)) (DE c) b
TNF' (D2 a) c b => TNF' (DE (D2 a)) (DE c) b
TNF' (D1 a) c b => TNF' (DE (D1 a)) (DE c) b
TNF' (D0 a) c b => TNF' (DE (D0 a)) (DE c) b
TNF' (DD F) (DD F) T
TNF' (DD T) (DD T) T
TNF' (DF a) c b => TNF' (DD (DF a)) (DD c) b
TNF' (DE a) c b => TNF' (DD (DE a)) (DD c) b
TNF' (DD a) c b => TNF' (DD (DD a)) (DD c) b
TNF' (DC a) c b => TNF' (DD (DC a)) (DD c) b
TNF' (DB a) c b => TNF' (DD (DB a)) (DD c) b
TNF' (DA a) c b => TNF' (DD (DA a)) (DD c) b
TNF' (D9 a) c b => TNF' (DD (D9 a)) (DD c) b
TNF' (D8 a) c b => TNF' (DD (D8 a)) (DD c) b
TNF' (D7 a) c b => TNF' (DD (D7 a)) (DD c) b
TNF' (D6 a) c b => TNF' (DD (D6 a)) (DD c) b
TNF' (D5 a) c b => TNF' (DD (D5 a)) (DD c) b
TNF' (D4 a) c b => TNF' (DD (D4 a)) (DD c) b
TNF' (D3 a) c b => TNF' (DD (D3 a)) (DD c) b
TNF' (D2 a) c b => TNF' (DD (D2 a)) (DD c) b
TNF' (D1 a) c b => TNF' (DD (D1 a)) (DD c) b
TNF' (D0 a) c b => TNF' (DD (D0 a)) (DD c) b
TNF' (DC F) (DC F) T
TNF' (DC T) (DC T) T
TNF' (DF a) c b => TNF' (DC (DF a)) (DC c) b
TNF' (DE a) c b => TNF' (DC (DE a)) (DC c) b
TNF' (DD a) c b => TNF' (DC (DD a)) (DC c) b
TNF' (DC a) c b => TNF' (DC (DC a)) (DC c) b
TNF' (DB a) c b => TNF' (DC (DB a)) (DC c) b
TNF' (DA a) c b => TNF' (DC (DA a)) (DC c) b
TNF' (D9 a) c b => TNF' (DC (D9 a)) (DC c) b
TNF' (D8 a) c b => TNF' (DC (D8 a)) (DC c) b
TNF' (D7 a) c b => TNF' (DC (D7 a)) (DC c) b
TNF' (D6 a) c b => TNF' (DC (D6 a)) (DC c) b
TNF' (D5 a) c b => TNF' (DC (D5 a)) (DC c) b
TNF' (D4 a) c b => TNF' (DC (D4 a)) (DC c) b
TNF' (D3 a) c b => TNF' (DC (D3 a)) (DC c) b
TNF' (D2 a) c b => TNF' (DC (D2 a)) (DC c) b
TNF' (D1 a) c b => TNF' (DC (D1 a)) (DC c) b
TNF' (D0 a) c b => TNF' (DC (D0 a)) (DC c) b
TNF' (DB F) (DB F) T
TNF' (DB T) (DB T) T
TNF' (DF a) c b => TNF' (DB (DF a)) (DB c) b
TNF' (DE a) c b => TNF' (DB (DE a)) (DB c) b
TNF' (DD a) c b => TNF' (DB (DD a)) (DB c) b
TNF' (DC a) c b => TNF' (DB (DC a)) (DB c) b
TNF' (DB a) c b => TNF' (DB (DB a)) (DB c) b
TNF' (DA a) c b => TNF' (DB (DA a)) (DB c) b
TNF' (D9 a) c b => TNF' (DB (D9 a)) (DB c) b
TNF' (D8 a) c b => TNF' (DB (D8 a)) (DB c) b
TNF' (D7 a) c b => TNF' (DB (D7 a)) (DB c) b
TNF' (D6 a) c b => TNF' (DB (D6 a)) (DB c) b
TNF' (D5 a) c b => TNF' (DB (D5 a)) (DB c) b
TNF' (D4 a) c b => TNF' (DB (D4 a)) (DB c) b
TNF' (D3 a) c b => TNF' (DB (D3 a)) (DB c) b
TNF' (D2 a) c b => TNF' (DB (D2 a)) (DB c) b
TNF' (D1 a) c b => TNF' (DB (D1 a)) (DB c) b
TNF' (D0 a) c b => TNF' (DB (D0 a)) (DB c) b
TNF' (DA F) (DA F) T
TNF' (DA T) (DA T) T
TNF' (DF a) c b => TNF' (DA (DF a)) (DA c) b
TNF' (DE a) c b => TNF' (DA (DE a)) (DA c) b
TNF' (DD a) c b => TNF' (DA (DD a)) (DA c) b
TNF' (DC a) c b => TNF' (DA (DC a)) (DA c) b
TNF' (DB a) c b => TNF' (DA (DB a)) (DA c) b
TNF' (DA a) c b => TNF' (DA (DA a)) (DA c) b
TNF' (D9 a) c b => TNF' (DA (D9 a)) (DA c) b
TNF' (D8 a) c b => TNF' (DA (D8 a)) (DA c) b
TNF' (D7 a) c b => TNF' (DA (D7 a)) (DA c) b
TNF' (D6 a) c b => TNF' (DA (D6 a)) (DA c) b
TNF' (D5 a) c b => TNF' (DA (D5 a)) (DA c) b
TNF' (D4 a) c b => TNF' (DA (D4 a)) (DA c) b
TNF' (D3 a) c b => TNF' (DA (D3 a)) (DA c) b
TNF' (D2 a) c b => TNF' (DA (D2 a)) (DA c) b
TNF' (D1 a) c b => TNF' (DA (D1 a)) (DA c) b
TNF' (D0 a) c b => TNF' (DA (D0 a)) (DA c) b
TNF' (D9 F) (D9 F) T
TNF' (D9 T) (D9 T) T
TNF' (DF a) c b => TNF' (D9 (DF a)) (D9 c) b
TNF' (DE a) c b => TNF' (D9 (DE a)) (D9 c) b
TNF' (DD a) c b => TNF' (D9 (DD a)) (D9 c) b
TNF' (DC a) c b => TNF' (D9 (DC a)) (D9 c) b
TNF' (DB a) c b => TNF' (D9 (DB a)) (D9 c) b
TNF' (DA a) c b => TNF' (D9 (DA a)) (D9 c) b
TNF' (D9 a) c b => TNF' (D9 (D9 a)) (D9 c) b
TNF' (D8 a) c b => TNF' (D9 (D8 a)) (D9 c) b
TNF' (D7 a) c b => TNF' (D9 (D7 a)) (D9 c) b
TNF' (D6 a) c b => TNF' (D9 (D6 a)) (D9 c) b
TNF' (D5 a) c b => TNF' (D9 (D5 a)) (D9 c) b
TNF' (D4 a) c b => TNF' (D9 (D4 a)) (D9 c) b
TNF' (D3 a) c b => TNF' (D9 (D3 a)) (D9 c) b
TNF' (D2 a) c b => TNF' (D9 (D2 a)) (D9 c) b
TNF' (D1 a) c b => TNF' (D9 (D1 a)) (D9 c) b
TNF' (D0 a) c b => TNF' (D9 (D0 a)) (D9 c) b
TNF' (D8 F) (D8 F) T
TNF' (D8 T) (D8 T) T
TNF' (DF a) c b => TNF' (D8 (DF a)) (D8 c) b
TNF' (DE a) c b => TNF' (D8 (DE a)) (D8 c) b
TNF' (DD a) c b => TNF' (D8 (DD a)) (D8 c) b
TNF' (DC a) c b => TNF' (D8 (DC a)) (D8 c) b
TNF' (DB a) c b => TNF' (D8 (DB a)) (D8 c) b
TNF' (DA a) c b => TNF' (D8 (DA a)) (D8 c) b
TNF' (D9 a) c b => TNF' (D8 (D9 a)) (D8 c) b
TNF' (D8 a) c b => TNF' (D8 (D8 a)) (D8 c) b
TNF' (D7 a) c b => TNF' (D8 (D7 a)) (D8 c) b
TNF' (D6 a) c b => TNF' (D8 (D6 a)) (D8 c) b
TNF' (D5 a) c b => TNF' (D8 (D5 a)) (D8 c) b
TNF' (D4 a) c b => TNF' (D8 (D4 a)) (D8 c) b
TNF' (D3 a) c b => TNF' (D8 (D3 a)) (D8 c) b
TNF' (D2 a) c b => TNF' (D8 (D2 a)) (D8 c) b
TNF' (D1 a) c b => TNF' (D8 (D1 a)) (D8 c) b
TNF' (D0 a) c b => TNF' (D8 (D0 a)) (D8 c) b
TNF' (D7 F) (D7 F) T
TNF' (D7 T) (D7 T) T
TNF' (DF a) c b => TNF' (D7 (DF a)) (D7 c) b
TNF' (DE a) c b => TNF' (D7 (DE a)) (D7 c) b
TNF' (DD a) c b => TNF' (D7 (DD a)) (D7 c) b
TNF' (DC a) c b => TNF' (D7 (DC a)) (D7 c) b
TNF' (DB a) c b => TNF' (D7 (DB a)) (D7 c) b
TNF' (DA a) c b => TNF' (D7 (DA a)) (D7 c) b
TNF' (D9 a) c b => TNF' (D7 (D9 a)) (D7 c) b
TNF' (D8 a) c b => TNF' (D7 (D8 a)) (D7 c) b
TNF' (D7 a) c b => TNF' (D7 (D7 a)) (D7 c) b
TNF' (D6 a) c b => TNF' (D7 (D6 a)) (D7 c) b
TNF' (D5 a) c b => TNF' (D7 (D5 a)) (D7 c) b
TNF' (D4 a) c b => TNF' (D7 (D4 a)) (D7 c) b
TNF' (D3 a) c b => TNF' (D7 (D3 a)) (D7 c) b
TNF' (D2 a) c b => TNF' (D7 (D2 a)) (D7 c) b
TNF' (D1 a) c b => TNF' (D7 (D1 a)) (D7 c) b
TNF' (D0 a) c b => TNF' (D7 (D0 a)) (D7 c) b
TNF' (D6 F) (D6 F) T
TNF' (D6 T) (D6 T) T
TNF' (DF a) c b => TNF' (D6 (DF a)) (D6 c) b
TNF' (DE a) c b => TNF' (D6 (DE a)) (D6 c) b
TNF' (DD a) c b => TNF' (D6 (DD a)) (D6 c) b
TNF' (DC a) c b => TNF' (D6 (DC a)) (D6 c) b
TNF' (DB a) c b => TNF' (D6 (DB a)) (D6 c) b
TNF' (DA a) c b => TNF' (D6 (DA a)) (D6 c) b
TNF' (D9 a) c b => TNF' (D6 (D9 a)) (D6 c) b
TNF' (D8 a) c b => TNF' (D6 (D8 a)) (D6 c) b
TNF' (D7 a) c b => TNF' (D6 (D7 a)) (D6 c) b
TNF' (D6 a) c b => TNF' (D6 (D6 a)) (D6 c) b
TNF' (D5 a) c b => TNF' (D6 (D5 a)) (D6 c) b
TNF' (D4 a) c b => TNF' (D6 (D4 a)) (D6 c) b
TNF' (D3 a) c b => TNF' (D6 (D3 a)) (D6 c) b
TNF' (D2 a) c b => TNF' (D6 (D2 a)) (D6 c) b
TNF' (D1 a) c b => TNF' (D6 (D1 a)) (D6 c) b
TNF' (D0 a) c b => TNF' (D6 (D0 a)) (D6 c) b
TNF' (D5 F) (D5 F) T
TNF' (D5 T) (D5 T) T
TNF' (DF a) c b => TNF' (D5 (DF a)) (D5 c) b
TNF' (DE a) c b => TNF' (D5 (DE a)) (D5 c) b
TNF' (DD a) c b => TNF' (D5 (DD a)) (D5 c) b
TNF' (DC a) c b => TNF' (D5 (DC a)) (D5 c) b
TNF' (DB a) c b => TNF' (D5 (DB a)) (D5 c) b
TNF' (DA a) c b => TNF' (D5 (DA a)) (D5 c) b
TNF' (D9 a) c b => TNF' (D5 (D9 a)) (D5 c) b
TNF' (D8 a) c b => TNF' (D5 (D8 a)) (D5 c) b
TNF' (D7 a) c b => TNF' (D5 (D7 a)) (D5 c) b
TNF' (D6 a) c b => TNF' (D5 (D6 a)) (D5 c) b
TNF' (D5 a) c b => TNF' (D5 (D5 a)) (D5 c) b
TNF' (D4 a) c b => TNF' (D5 (D4 a)) (D5 c) b
TNF' (D3 a) c b => TNF' (D5 (D3 a)) (D5 c) b
TNF' (D2 a) c b => TNF' (D5 (D2 a)) (D5 c) b
TNF' (D1 a) c b => TNF' (D5 (D1 a)) (D5 c) b
TNF' (D0 a) c b => TNF' (D5 (D0 a)) (D5 c) b
TNF' (D4 F) (D4 F) T
TNF' (D4 T) (D4 T) T
TNF' (DF a) c b => TNF' (D4 (DF a)) (D4 c) b
TNF' (DE a) c b => TNF' (D4 (DE a)) (D4 c) b
TNF' (DD a) c b => TNF' (D4 (DD a)) (D4 c) b
TNF' (DC a) c b => TNF' (D4 (DC a)) (D4 c) b
TNF' (DB a) c b => TNF' (D4 (DB a)) (D4 c) b
TNF' (DA a) c b => TNF' (D4 (DA a)) (D4 c) b
TNF' (D9 a) c b => TNF' (D4 (D9 a)) (D4 c) b
TNF' (D8 a) c b => TNF' (D4 (D8 a)) (D4 c) b
TNF' (D7 a) c b => TNF' (D4 (D7 a)) (D4 c) b
TNF' (D6 a) c b => TNF' (D4 (D6 a)) (D4 c) b
TNF' (D5 a) c b => TNF' (D4 (D5 a)) (D4 c) b
TNF' (D4 a) c b => TNF' (D4 (D4 a)) (D4 c) b
TNF' (D3 a) c b => TNF' (D4 (D3 a)) (D4 c) b
TNF' (D2 a) c b => TNF' (D4 (D2 a)) (D4 c) b
TNF' (D1 a) c b => TNF' (D4 (D1 a)) (D4 c) b
TNF' (D0 a) c b => TNF' (D4 (D0 a)) (D4 c) b
TNF' (D3 F) (D3 F) T
TNF' (D3 T) (D3 T) T
TNF' (DF a) c b => TNF' (D3 (DF a)) (D3 c) b
TNF' (DE a) c b => TNF' (D3 (DE a)) (D3 c) b
TNF' (DD a) c b => TNF' (D3 (DD a)) (D3 c) b
TNF' (DC a) c b => TNF' (D3 (DC a)) (D3 c) b
TNF' (DB a) c b => TNF' (D3 (DB a)) (D3 c) b
TNF' (DA a) c b => TNF' (D3 (DA a)) (D3 c) b
TNF' (D9 a) c b => TNF' (D3 (D9 a)) (D3 c) b
TNF' (D8 a) c b => TNF' (D3 (D8 a)) (D3 c) b
TNF' (D7 a) c b => TNF' (D3 (D7 a)) (D3 c) b
TNF' (D6 a) c b => TNF' (D3 (D6 a)) (D3 c) b
TNF' (D5 a) c b => TNF' (D3 (D5 a)) (D3 c) b
TNF' (D4 a) c b => TNF' (D3 (D4 a)) (D3 c) b
TNF' (D3 a) c b => TNF' (D3 (D3 a)) (D3 c) b
TNF' (D2 a) c b => TNF' (D3 (D2 a)) (D3 c) b
TNF' (D1 a) c b => TNF' (D3 (D1 a)) (D3 c) b
TNF' (D0 a) c b => TNF' (D3 (D0 a)) (D3 c) b
TNF' (D2 F) (D2 F) T
TNF' (D2 T) (D2 T) T
TNF' (DF a) c b => TNF' (D2 (DF a)) (D2 c) b
TNF' (DE a) c b => TNF' (D2 (DE a)) (D2 c) b
TNF' (DD a) c b => TNF' (D2 (DD a)) (D2 c) b
TNF' (DC a) c b => TNF' (D2 (DC a)) (D2 c) b
TNF' (DB a) c b => TNF' (D2 (DB a)) (D2 c) b
TNF' (DA a) c b => TNF' (D2 (DA a)) (D2 c) b
TNF' (D9 a) c b => TNF' (D2 (D9 a)) (D2 c) b
TNF' (D8 a) c b => TNF' (D2 (D8 a)) (D2 c) b
TNF' (D7 a) c b => TNF' (D2 (D7 a)) (D2 c) b
TNF' (D6 a) c b => TNF' (D2 (D6 a)) (D2 c) b
TNF' (D5 a) c b => TNF' (D2 (D5 a)) (D2 c) b
TNF' (D4 a) c b => TNF' (D2 (D4 a)) (D2 c) b
TNF' (D3 a) c b => TNF' (D2 (D3 a)) (D2 c) b
TNF' (D2 a) c b => TNF' (D2 (D2 a)) (D2 c) b
TNF' (D1 a) c b => TNF' (D2 (D1 a)) (D2 c) b
TNF' (D0 a) c b => TNF' (D2 (D0 a)) (D2 c) b
TNF' (D1 F) (D1 F) T
TNF' (D1 T) (D1 T) T
TNF' (DF a) c b => TNF' (D1 (DF a)) (D1 c) b
TNF' (DE a) c b => TNF' (D1 (DE a)) (D1 c) b
TNF' (DD a) c b => TNF' (D1 (DD a)) (D1 c) b
TNF' (DC a) c b => TNF' (D1 (DC a)) (D1 c) b
TNF' (DB a) c b => TNF' (D1 (DB a)) (D1 c) b
TNF' (DA a) c b => TNF' (D1 (DA a)) (D1 c) b
TNF' (D9 a) c b => TNF' (D1 (D9 a)) (D1 c) b
TNF' (D8 a) c b => TNF' (D1 (D8 a)) (D1 c) b
TNF' (D7 a) c b => TNF' (D1 (D7 a)) (D1 c) b
TNF' (D6 a) c b => TNF' (D1 (D6 a)) (D1 c) b
TNF' (D5 a) c b => TNF' (D1 (D5 a)) (D1 c) b
TNF' (D4 a) c b => TNF' (D1 (D4 a)) (D1 c) b
TNF' (D3 a) c b => TNF' (D1 (D3 a)) (D1 c) b
TNF' (D2 a) c b => TNF' (D1 (D2 a)) (D1 c) b
TNF' (D1 a) c b => TNF' (D1 (D1 a)) (D1 c) b
TNF' (D0 a) c b => TNF' (D1 (D0 a)) (D1 c) b
TNF' (D0 T) (D0 T) T
TNF' (DF a) c b => TNF' (D0 (DF a)) (D0 c) b
TNF' (DE a) c b => TNF' (D0 (DE a)) (D0 c) b
TNF' (DD a) c b => TNF' (D0 (DD a)) (D0 c) b
TNF' (DC a) c b => TNF' (D0 (DC a)) (D0 c) b
TNF' (DB a) c b => TNF' (D0 (DB a)) (D0 c) b
TNF' (DA a) c b => TNF' (D0 (DA a)) (D0 c) b
TNF' (D9 a) c b => TNF' (D0 (D9 a)) (D0 c) b
TNF' (D8 a) c b => TNF' (D0 (D8 a)) (D0 c) b
TNF' (D7 a) c b => TNF' (D0 (D7 a)) (D0 c) b
TNF' (D6 a) c b => TNF' (D0 (D6 a)) (D0 c) b
TNF' (D5 a) c b => TNF' (D0 (D5 a)) (D0 c) b
TNF' (D4 a) c b => TNF' (D0 (D4 a)) (D0 c) b
TNF' (D3 a) c b => TNF' (D0 (D3 a)) (D0 c) b
TNF' (D2 a) c b => TNF' (D0 (D2 a)) (D0 c) b
TNF' (D1 a) c b => TNF' (D0 (D1 a)) (D0 c) b

class THex a whereSource

Methods

fromTHex :: Integral b => a -> bSource

Instances

THex F
THex T
(THex a, ExtF a) => THex (DF a)
THex a => THex (DE a)
THex a => THex (DD a)
THex a => THex (DC a)
THex a => THex (DB a)
THex a => THex (DA a)
THex a => THex (D9 a)
THex a => THex (D8 a)
THex a => THex (D7 a)
THex a => THex (D6 a)
THex a => THex (D5 a)
THex a => THex (D4 a)
THex a => THex (D3 a)
THex a => THex (D2 a)
THex a => THex (D1 a)
(THex a, Ext0 a) => THex (D0 a)

class SHR1 a b c | a b -> cSource

Instances

SHR1 H0 F F
SHR1 H1 F (D1 F)
SHR1 H1 T (DE T)
SHR1 H0 T (DE T)
SHR1 H1 (DF F) (DF (D1 F))
SHR1 H1 (DF T) (DF T)
SHR1 H1 (DF a) (DF b) => SHR1 H1 (DF (DF a)) (DF (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H1 (DF (DE a)) (DF (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H1 (DF (DD a)) (DF (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H1 (DF (DC a)) (DF (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H1 (DF (DB a)) (DF (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H1 (DF (DA a)) (DF (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H1 (DF (D9 a)) (DF (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H1 (DF (D8 a)) (DF (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (DF (D7 a)) (DF (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (DF (D6 a)) (DF (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (DF (D5 a)) (DF (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (DF (D4 a)) (DF (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DF (D3 a)) (DF (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DF (D2 a)) (DF (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (DF (D1 a)) (DF (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (DF (D0 a)) (DF (D1 b))
SHR1 H1 (DE F) (DD (D1 F))
SHR1 H1 (DE T) (DD T)
SHR1 H1 (DF a) (DF b) => SHR1 H1 (DE (DF a)) (DD (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H1 (DE (DE a)) (DD (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H1 (DE (DD a)) (DD (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H1 (DE (DC a)) (DD (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H1 (DE (DB a)) (DD (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H1 (DE (DA a)) (DD (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H1 (DE (D9 a)) (DD (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H1 (DE (D8 a)) (DD (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (DE (D7 a)) (DD (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (DE (D6 a)) (DD (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (DE (D5 a)) (DD (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (DE (D4 a)) (DD (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DE (D3 a)) (DD (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DE (D2 a)) (DD (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (DE (D1 a)) (DD (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (DE (D0 a)) (DD (D1 b))
SHR1 H1 (DD F) (DB (D1 F))
SHR1 H1 (DD T) (DB T)
SHR1 H1 (DF a) (DF b) => SHR1 H1 (DD (DF a)) (DB (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H1 (DD (DE a)) (DB (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H1 (DD (DD a)) (DB (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H1 (DD (DC a)) (DB (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H1 (DD (DB a)) (DB (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H1 (DD (DA a)) (DB (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H1 (DD (D9 a)) (DB (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H1 (DD (D8 a)) (DB (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (DD (D7 a)) (DB (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (DD (D6 a)) (DB (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (DD (D5 a)) (DB (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (DD (D4 a)) (DB (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DD (D3 a)) (DB (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DD (D2 a)) (DB (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (DD (D1 a)) (DB (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (DD (D0 a)) (DB (D1 b))
SHR1 H1 (DC F) (D9 (D1 F))
SHR1 H1 (DC T) (D9 T)
SHR1 H1 (DF a) (DF b) => SHR1 H1 (DC (DF a)) (D9 (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H1 (DC (DE a)) (D9 (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H1 (DC (DD a)) (D9 (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H1 (DC (DC a)) (D9 (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H1 (DC (DB a)) (D9 (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H1 (DC (DA a)) (D9 (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H1 (DC (D9 a)) (D9 (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H1 (DC (D8 a)) (D9 (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (DC (D7 a)) (D9 (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (DC (D6 a)) (D9 (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (DC (D5 a)) (D9 (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (DC (D4 a)) (D9 (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DC (D3 a)) (D9 (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DC (D2 a)) (D9 (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (DC (D1 a)) (D9 (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (DC (D0 a)) (D9 (D1 b))
SHR1 H1 (DB F) (D7 (D1 F))
SHR1 H1 (DB T) (D7 T)
SHR1 H1 (DF a) (DF b) => SHR1 H1 (DB (DF a)) (D7 (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H1 (DB (DE a)) (D7 (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H1 (DB (DD a)) (D7 (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H1 (DB (DC a)) (D7 (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H1 (DB (DB a)) (D7 (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H1 (DB (DA a)) (D7 (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H1 (DB (D9 a)) (D7 (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H1 (DB (D8 a)) (D7 (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (DB (D7 a)) (D7 (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (DB (D6 a)) (D7 (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (DB (D5 a)) (D7 (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (DB (D4 a)) (D7 (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DB (D3 a)) (D7 (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DB (D2 a)) (D7 (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (DB (D1 a)) (D7 (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (DB (D0 a)) (D7 (D1 b))
SHR1 H1 (DA F) (D5 (D1 F))
SHR1 H1 (DA T) (D5 T)
SHR1 H1 (DF a) (DF b) => SHR1 H1 (DA (DF a)) (D5 (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H1 (DA (DE a)) (D5 (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H1 (DA (DD a)) (D5 (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H1 (DA (DC a)) (D5 (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H1 (DA (DB a)) (D5 (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H1 (DA (DA a)) (D5 (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H1 (DA (D9 a)) (D5 (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H1 (DA (D8 a)) (D5 (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (DA (D7 a)) (D5 (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (DA (D6 a)) (D5 (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (DA (D5 a)) (D5 (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (DA (D4 a)) (D5 (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DA (D3 a)) (D5 (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DA (D2 a)) (D5 (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (DA (D1 a)) (D5 (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (DA (D0 a)) (D5 (D1 b))
SHR1 H1 (D9 F) (D3 (D1 F))
SHR1 H1 (D9 T) (D3 T)
SHR1 H1 (DF a) (DF b) => SHR1 H1 (D9 (DF a)) (D3 (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H1 (D9 (DE a)) (D3 (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H1 (D9 (DD a)) (D3 (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H1 (D9 (DC a)) (D3 (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H1 (D9 (DB a)) (D3 (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H1 (D9 (DA a)) (D3 (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H1 (D9 (D9 a)) (D3 (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H1 (D9 (D8 a)) (D3 (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (D9 (D7 a)) (D3 (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (D9 (D6 a)) (D3 (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (D9 (D5 a)) (D3 (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (D9 (D4 a)) (D3 (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (D9 (D3 a)) (D3 (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (D9 (D2 a)) (D3 (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (D9 (D1 a)) (D3 (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (D9 (D0 a)) (D3 (D1 b))
SHR1 H1 (D8 F) (D1 (D1 F))
SHR1 H1 (D8 T) (D1 T)
SHR1 H1 (DF a) (DF b) => SHR1 H1 (D8 (DF a)) (D1 (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H1 (D8 (DE a)) (D1 (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H1 (D8 (DD a)) (D1 (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H1 (D8 (DC a)) (D1 (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H1 (D8 (DB a)) (D1 (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H1 (D8 (DA a)) (D1 (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H1 (D8 (D9 a)) (D1 (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H1 (D8 (D8 a)) (D1 (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (D8 (D7 a)) (D1 (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (D8 (D6 a)) (D1 (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (D8 (D5 a)) (D1 (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (D8 (D4 a)) (D1 (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (D8 (D3 a)) (D1 (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (D8 (D2 a)) (D1 (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (D8 (D1 a)) (D1 (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (D8 (D0 a)) (D1 (D1 b))
SHR1 H1 (D7 F) (DF F)
SHR1 H1 (D7 T) (DF (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H1 (D7 (DF a)) (DF (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H1 (D7 (DE a)) (DF (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H1 (D7 (DD a)) (DF (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H1 (D7 (DC a)) (DF (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H1 (D7 (DB a)) (DF (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H1 (D7 (DA a)) (DF (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H1 (D7 (D9 a)) (DF (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D7 (D8 a)) (DF (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H1 (D7 (D7 a)) (DF (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D7 (D6 a)) (DF (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H1 (D7 (D5 a)) (DF (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D7 (D4 a)) (DF (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D7 (D3 a)) (DF (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D7 (D2 a)) (DF (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H1 (D7 (D1 a)) (DF (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H1 (D7 (D0 a)) (DF (D0 b))
SHR1 H1 (D6 F) (DD F)
SHR1 H1 (D6 T) (DD (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H1 (D6 (DF a)) (DD (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H1 (D6 (DE a)) (DD (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H1 (D6 (DD a)) (DD (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H1 (D6 (DC a)) (DD (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H1 (D6 (DB a)) (DD (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H1 (D6 (DA a)) (DD (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H1 (D6 (D9 a)) (DD (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D6 (D8 a)) (DD (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H1 (D6 (D7 a)) (DD (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D6 (D6 a)) (DD (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H1 (D6 (D5 a)) (DD (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D6 (D4 a)) (DD (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D6 (D3 a)) (DD (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D6 (D2 a)) (DD (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H1 (D6 (D1 a)) (DD (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H1 (D6 (D0 a)) (DD (D0 b))
SHR1 H1 (D5 F) (DB F)
SHR1 H1 (D5 T) (DB (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H1 (D5 (DF a)) (DB (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H1 (D5 (DE a)) (DB (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H1 (D5 (DD a)) (DB (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H1 (D5 (DC a)) (DB (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H1 (D5 (DB a)) (DB (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H1 (D5 (DA a)) (DB (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H1 (D5 (D9 a)) (DB (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D5 (D8 a)) (DB (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H1 (D5 (D7 a)) (DB (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D5 (D6 a)) (DB (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H1 (D5 (D5 a)) (DB (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D5 (D4 a)) (DB (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D5 (D3 a)) (DB (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D5 (D2 a)) (DB (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H1 (D5 (D1 a)) (DB (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H1 (D5 (D0 a)) (DB (D0 b))
SHR1 H1 (D4 F) (D9 F)
SHR1 H1 (D4 T) (D9 (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H1 (D4 (DF a)) (D9 (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H1 (D4 (DE a)) (D9 (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H1 (D4 (DD a)) (D9 (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H1 (D4 (DC a)) (D9 (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H1 (D4 (DB a)) (D9 (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H1 (D4 (DA a)) (D9 (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H1 (D4 (D9 a)) (D9 (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D4 (D8 a)) (D9 (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H1 (D4 (D7 a)) (D9 (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D4 (D6 a)) (D9 (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H1 (D4 (D5 a)) (D9 (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D4 (D4 a)) (D9 (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D4 (D3 a)) (D9 (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D4 (D2 a)) (D9 (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H1 (D4 (D1 a)) (D9 (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H1 (D4 (D0 a)) (D9 (D0 b))
SHR1 H1 (D3 F) (D7 F)
SHR1 H1 (D3 T) (D7 (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H1 (D3 (DF a)) (D7 (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H1 (D3 (DE a)) (D7 (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H1 (D3 (DD a)) (D7 (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H1 (D3 (DC a)) (D7 (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H1 (D3 (DB a)) (D7 (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H1 (D3 (DA a)) (D7 (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H1 (D3 (D9 a)) (D7 (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D3 (D8 a)) (D7 (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H1 (D3 (D7 a)) (D7 (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D3 (D6 a)) (D7 (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H1 (D3 (D5 a)) (D7 (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D3 (D4 a)) (D7 (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D3 (D3 a)) (D7 (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D3 (D2 a)) (D7 (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H1 (D3 (D1 a)) (D7 (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H1 (D3 (D0 a)) (D7 (D0 b))
SHR1 H1 (D2 F) (D5 F)
SHR1 H1 (D2 T) (D5 (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H1 (D2 (DF a)) (D5 (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H1 (D2 (DE a)) (D5 (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H1 (D2 (DD a)) (D5 (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H1 (D2 (DC a)) (D5 (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H1 (D2 (DB a)) (D5 (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H1 (D2 (DA a)) (D5 (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H1 (D2 (D9 a)) (D5 (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D2 (D8 a)) (D5 (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H1 (D2 (D7 a)) (D5 (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D2 (D6 a)) (D5 (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H1 (D2 (D5 a)) (D5 (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D2 (D4 a)) (D5 (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D2 (D3 a)) (D5 (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D2 (D2 a)) (D5 (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H1 (D2 (D1 a)) (D5 (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H1 (D2 (D0 a)) (D5 (D0 b))
SHR1 H1 (D1 F) (D3 F)
SHR1 H1 (D1 T) (D3 (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H1 (D1 (DF a)) (D3 (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H1 (D1 (DE a)) (D3 (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H1 (D1 (DD a)) (D3 (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H1 (D1 (DC a)) (D3 (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H1 (D1 (DB a)) (D3 (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H1 (D1 (DA a)) (D3 (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H1 (D1 (D9 a)) (D3 (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D1 (D8 a)) (D3 (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H1 (D1 (D7 a)) (D3 (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D1 (D6 a)) (D3 (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H1 (D1 (D5 a)) (D3 (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D1 (D4 a)) (D3 (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D1 (D3 a)) (D3 (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D1 (D2 a)) (D3 (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H1 (D1 (D1 a)) (D3 (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H1 (D1 (D0 a)) (D3 (D0 b))
SHR1 H1 (D0 F) (D1 F)
SHR1 H1 (D0 T) (D1 (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H1 (D0 (DF a)) (D1 (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H1 (D0 (DE a)) (D1 (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H1 (D0 (DD a)) (D1 (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H1 (D0 (DC a)) (D1 (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H1 (D0 (DB a)) (D1 (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H1 (D0 (DA a)) (D1 (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H1 (D0 (D9 a)) (D1 (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D0 (D8 a)) (D1 (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H1 (D0 (D7 a)) (D1 (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D0 (D6 a)) (D1 (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H1 (D0 (D5 a)) (D1 (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D0 (D4 a)) (D1 (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D0 (D3 a)) (D1 (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D0 (D2 a)) (D1 (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H1 (D0 (D1 a)) (D1 (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H1 (D0 (D0 a)) (D1 (D0 b))
SHR1 H0 (DF F) (DE (D1 F))
SHR1 H0 (DF T) (DE T)
SHR1 H1 (DF a) (DF b) => SHR1 H0 (DF (DF a)) (DE (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H0 (DF (DE a)) (DE (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H0 (DF (DD a)) (DE (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H0 (DF (DC a)) (DE (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H0 (DF (DB a)) (DE (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (DF (DA a)) (DE (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (DF (D9 a)) (DE (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H0 (DF (D8 a)) (DE (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H0 (DF (D7 a)) (DE (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H0 (DF (D6 a)) (DE (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (DF (D5 a)) (DE (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H0 (DF (D4 a)) (DE (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (DF (D3 a)) (DE (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DF (D2 a)) (DE (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (DF (D1 a)) (DE (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H0 (DF (D0 a)) (DE (D1 b))
SHR1 H0 (DE F) (DC (D1 F))
SHR1 H0 (DE T) (DC T)
SHR1 H1 (DF a) (DF b) => SHR1 H0 (DE (DF a)) (DC (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H0 (DE (DE a)) (DC (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H0 (DE (DD a)) (DC (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H0 (DE (DC a)) (DC (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H0 (DE (DB a)) (DC (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (DE (DA a)) (DC (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (DE (D9 a)) (DC (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H0 (DE (D8 a)) (DC (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H0 (DE (D7 a)) (DC (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H0 (DE (D6 a)) (DC (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (DE (D5 a)) (DC (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H0 (DE (D4 a)) (DC (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (DE (D3 a)) (DC (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DE (D2 a)) (DC (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (DE (D1 a)) (DC (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H0 (DE (D0 a)) (DC (D1 b))
SHR1 H0 (DD F) (DA (D1 F))
SHR1 H0 (DD T) (DA T)
SHR1 H1 (DF a) (DF b) => SHR1 H0 (DD (DF a)) (DA (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H0 (DD (DE a)) (DA (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H0 (DD (DD a)) (DA (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H0 (DD (DC a)) (DA (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H0 (DD (DB a)) (DA (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (DD (DA a)) (DA (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (DD (D9 a)) (DA (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H0 (DD (D8 a)) (DA (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H0 (DD (D7 a)) (DA (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H0 (DD (D6 a)) (DA (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (DD (D5 a)) (DA (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H0 (DD (D4 a)) (DA (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (DD (D3 a)) (DA (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DD (D2 a)) (DA (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (DD (D1 a)) (DA (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H0 (DD (D0 a)) (DA (D1 b))
SHR1 H0 (DC F) (D8 (D1 F))
SHR1 H0 (DC T) (D8 T)
SHR1 H1 (DF a) (DF b) => SHR1 H0 (DC (DF a)) (D8 (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H0 (DC (DE a)) (D8 (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H0 (DC (DD a)) (D8 (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H0 (DC (DC a)) (D8 (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H0 (DC (DB a)) (D8 (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (DC (DA a)) (D8 (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (DC (D9 a)) (D8 (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H0 (DC (D8 a)) (D8 (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H0 (DC (D7 a)) (D8 (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H0 (DC (D6 a)) (D8 (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (DC (D5 a)) (D8 (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H0 (DC (D4 a)) (D8 (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (DC (D3 a)) (D8 (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DC (D2 a)) (D8 (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (DC (D1 a)) (D8 (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H0 (DC (D0 a)) (D8 (D1 b))
SHR1 H0 (DB F) (D6 (D1 F))
SHR1 H0 (DB T) (D6 T)
SHR1 H1 (DF a) (DF b) => SHR1 H0 (DB (DF a)) (D6 (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H0 (DB (DE a)) (D6 (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H0 (DB (DD a)) (D6 (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H0 (DB (DC a)) (D6 (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H0 (DB (DB a)) (D6 (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (DB (DA a)) (D6 (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (DB (D9 a)) (D6 (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H0 (DB (D8 a)) (D6 (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H0 (DB (D7 a)) (D6 (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H0 (DB (D6 a)) (D6 (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (DB (D5 a)) (D6 (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H0 (DB (D4 a)) (D6 (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (DB (D3 a)) (D6 (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DB (D2 a)) (D6 (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (DB (D1 a)) (D6 (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H0 (DB (D0 a)) (D6 (D1 b))
SHR1 H0 (DA F) (D4 (D1 F))
SHR1 H0 (DA T) (D4 T)
SHR1 H1 (DF a) (DF b) => SHR1 H0 (DA (DF a)) (D4 (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H0 (DA (DE a)) (D4 (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H0 (DA (DD a)) (D4 (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H0 (DA (DC a)) (D4 (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H0 (DA (DB a)) (D4 (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (DA (DA a)) (D4 (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (DA (D9 a)) (D4 (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H0 (DA (D8 a)) (D4 (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H0 (DA (D7 a)) (D4 (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H0 (DA (D6 a)) (D4 (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (DA (D5 a)) (D4 (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H0 (DA (D4 a)) (D4 (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (DA (D3 a)) (D4 (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DA (D2 a)) (D4 (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (DA (D1 a)) (D4 (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H0 (DA (D0 a)) (D4 (D1 b))
SHR1 H0 (D9 F) (D2 (D1 F))
SHR1 H0 (D9 T) (D2 T)
SHR1 H1 (DF a) (DF b) => SHR1 H0 (D9 (DF a)) (D2 (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H0 (D9 (DE a)) (D2 (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H0 (D9 (DD a)) (D2 (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H0 (D9 (DC a)) (D2 (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H0 (D9 (DB a)) (D2 (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (D9 (DA a)) (D2 (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (D9 (D9 a)) (D2 (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H0 (D9 (D8 a)) (D2 (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H0 (D9 (D7 a)) (D2 (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H0 (D9 (D6 a)) (D2 (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (D9 (D5 a)) (D2 (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H0 (D9 (D4 a)) (D2 (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (D9 (D3 a)) (D2 (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (D9 (D2 a)) (D2 (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (D9 (D1 a)) (D2 (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H0 (D9 (D0 a)) (D2 (D1 b))
SHR1 H0 (D8 F) (D0 (D1 F))
SHR1 H0 (D8 T) (D0 T)
SHR1 H1 (DF a) (DF b) => SHR1 H0 (D8 (DF a)) (D0 (DF b))
SHR1 H1 (DE a) (DD b) => SHR1 H0 (D8 (DE a)) (D0 (DD b))
SHR1 H1 (DD a) (DB b) => SHR1 H0 (D8 (DD a)) (D0 (DB b))
SHR1 H1 (DC a) (D9 b) => SHR1 H0 (D8 (DC a)) (D0 (D9 b))
SHR1 H1 (DB a) (D7 b) => SHR1 H0 (D8 (DB a)) (D0 (D7 b))
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (D8 (DA a)) (D0 (D5 b))
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (D8 (D9 a)) (D0 (D3 b))
SHR1 H1 (D8 a) (D1 b) => SHR1 H0 (D8 (D8 a)) (D0 (D1 b))
SHR1 H1 (D7 a) (DF b) => SHR1 H0 (D8 (D7 a)) (D0 (DF b))
SHR1 H1 (D6 a) (DD b) => SHR1 H0 (D8 (D6 a)) (D0 (DD b))
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (D8 (D5 a)) (D0 (DB b))
SHR1 H1 (D4 a) (D9 b) => SHR1 H0 (D8 (D4 a)) (D0 (D9 b))
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (D8 (D3 a)) (D0 (D7 b))
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (D8 (D2 a)) (D0 (D5 b))
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (D8 (D1 a)) (D0 (D3 b))
SHR1 H1 (D0 a) (D1 b) => SHR1 H0 (D8 (D0 a)) (D0 (D1 b))
SHR1 H0 (D7 F) (DE F)
SHR1 H0 (D7 T) (DE (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H0 (D7 (DF a)) (DE (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H0 (D7 (DE a)) (DE (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H0 (D7 (DD a)) (DE (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H0 (D7 (DC a)) (DE (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H0 (D7 (DB a)) (DE (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H0 (D7 (DA a)) (DE (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H0 (D7 (D9 a)) (DE (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H0 (D7 (D8 a)) (DE (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H0 (D7 (D7 a)) (DE (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H0 (D7 (D6 a)) (DE (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H0 (D7 (D5 a)) (DE (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H0 (D7 (D4 a)) (DE (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D7 (D3 a)) (DE (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H0 (D7 (D2 a)) (DE (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H0 (D7 (D1 a)) (DE (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H0 (D7 (D0 a)) (DE (D0 b))
SHR1 H0 (D6 F) (DC F)
SHR1 H0 (D6 T) (DC (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H0 (D6 (DF a)) (DC (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H0 (D6 (DE a)) (DC (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H0 (D6 (DD a)) (DC (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H0 (D6 (DC a)) (DC (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H0 (D6 (DB a)) (DC (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H0 (D6 (DA a)) (DC (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H0 (D6 (D9 a)) (DC (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H0 (D6 (D8 a)) (DC (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H0 (D6 (D7 a)) (DC (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H0 (D6 (D6 a)) (DC (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H0 (D6 (D5 a)) (DC (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H0 (D6 (D4 a)) (DC (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D6 (D3 a)) (DC (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H0 (D6 (D2 a)) (DC (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H0 (D6 (D1 a)) (DC (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H0 (D6 (D0 a)) (DC (D0 b))
SHR1 H0 (D5 F) (DA F)
SHR1 H0 (D5 T) (DA (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H0 (D5 (DF a)) (DA (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H0 (D5 (DE a)) (DA (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H0 (D5 (DD a)) (DA (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H0 (D5 (DC a)) (DA (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H0 (D5 (DB a)) (DA (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H0 (D5 (DA a)) (DA (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H0 (D5 (D9 a)) (DA (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H0 (D5 (D8 a)) (DA (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H0 (D5 (D7 a)) (DA (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H0 (D5 (D6 a)) (DA (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H0 (D5 (D5 a)) (DA (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H0 (D5 (D4 a)) (DA (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D5 (D3 a)) (DA (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H0 (D5 (D2 a)) (DA (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H0 (D5 (D1 a)) (DA (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H0 (D5 (D0 a)) (DA (D0 b))
SHR1 H0 (D4 F) (D8 F)
SHR1 H0 (D4 T) (D8 (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H0 (D4 (DF a)) (D8 (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H0 (D4 (DE a)) (D8 (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H0 (D4 (DD a)) (D8 (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H0 (D4 (DC a)) (D8 (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H0 (D4 (DB a)) (D8 (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H0 (D4 (DA a)) (D8 (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H0 (D4 (D9 a)) (D8 (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H0 (D4 (D8 a)) (D8 (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H0 (D4 (D7 a)) (D8 (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H0 (D4 (D6 a)) (D8 (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H0 (D4 (D5 a)) (D8 (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H0 (D4 (D4 a)) (D8 (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D4 (D3 a)) (D8 (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H0 (D4 (D2 a)) (D8 (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H0 (D4 (D1 a)) (D8 (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H0 (D4 (D0 a)) (D8 (D0 b))
SHR1 H0 (D3 F) (D6 F)
SHR1 H0 (D3 T) (D6 (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H0 (D3 (DF a)) (D6 (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H0 (D3 (DE a)) (D6 (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H0 (D3 (DD a)) (D6 (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H0 (D3 (DC a)) (D6 (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H0 (D3 (DB a)) (D6 (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H0 (D3 (DA a)) (D6 (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H0 (D3 (D9 a)) (D6 (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H0 (D3 (D8 a)) (D6 (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H0 (D3 (D7 a)) (D6 (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H0 (D3 (D6 a)) (D6 (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H0 (D3 (D5 a)) (D6 (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H0 (D3 (D4 a)) (D6 (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D3 (D3 a)) (D6 (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H0 (D3 (D2 a)) (D6 (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H0 (D3 (D1 a)) (D6 (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H0 (D3 (D0 a)) (D6 (D0 b))
SHR1 H0 (D2 F) (D4 F)
SHR1 H0 (D2 T) (D4 (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H0 (D2 (DF a)) (D4 (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H0 (D2 (DE a)) (D4 (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H0 (D2 (DD a)) (D4 (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H0 (D2 (DC a)) (D4 (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H0 (D2 (DB a)) (D4 (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H0 (D2 (DA a)) (D4 (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H0 (D2 (D9 a)) (D4 (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H0 (D2 (D8 a)) (D4 (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H0 (D2 (D7 a)) (D4 (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H0 (D2 (D6 a)) (D4 (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H0 (D2 (D5 a)) (D4 (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H0 (D2 (D4 a)) (D4 (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D2 (D3 a)) (D4 (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H0 (D2 (D2 a)) (D4 (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H0 (D2 (D1 a)) (D4 (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H0 (D2 (D0 a)) (D4 (D0 b))
SHR1 H0 (D1 F) (D2 F)
SHR1 H0 (D1 T) (D2 (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H0 (D1 (DF a)) (D2 (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H0 (D1 (DE a)) (D2 (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H0 (D1 (DD a)) (D2 (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H0 (D1 (DC a)) (D2 (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H0 (D1 (DB a)) (D2 (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H0 (D1 (DA a)) (D2 (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H0 (D1 (D9 a)) (D2 (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H0 (D1 (D8 a)) (D2 (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H0 (D1 (D7 a)) (D2 (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H0 (D1 (D6 a)) (D2 (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H0 (D1 (D5 a)) (D2 (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H0 (D1 (D4 a)) (D2 (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D1 (D3 a)) (D2 (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H0 (D1 (D2 a)) (D2 (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H0 (D1 (D1 a)) (D2 (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H0 (D1 (D0 a)) (D2 (D0 b))
SHR1 H0 (D0 F) (D0 F)
SHR1 H0 (D0 T) (D0 (DE T))
SHR1 H0 (DF a) (DE b) => SHR1 H0 (D0 (DF a)) (D0 (DE b))
SHR1 H0 (DE a) (DC b) => SHR1 H0 (D0 (DE a)) (D0 (DC b))
SHR1 H0 (DD a) (DA b) => SHR1 H0 (D0 (DD a)) (D0 (DA b))
SHR1 H0 (DC a) (D8 b) => SHR1 H0 (D0 (DC a)) (D0 (D8 b))
SHR1 H0 (DB a) (D6 b) => SHR1 H0 (D0 (DB a)) (D0 (D6 b))
SHR1 H0 (DA a) (D4 b) => SHR1 H0 (D0 (DA a)) (D0 (D4 b))
SHR1 H0 (D9 a) (D2 b) => SHR1 H0 (D0 (D9 a)) (D0 (D2 b))
SHR1 H0 (D8 a) (D0 b) => SHR1 H0 (D0 (D8 a)) (D0 (D0 b))
SHR1 H0 (D7 a) (DE b) => SHR1 H0 (D0 (D7 a)) (D0 (DE b))
SHR1 H0 (D6 a) (DC b) => SHR1 H0 (D0 (D6 a)) (D0 (DC b))
SHR1 H0 (D5 a) (DA b) => SHR1 H0 (D0 (D5 a)) (D0 (DA b))
SHR1 H0 (D4 a) (D8 b) => SHR1 H0 (D0 (D4 a)) (D0 (D8 b))
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D0 (D3 a)) (D0 (D6 b))
SHR1 H0 (D2 a) (D4 b) => SHR1 H0 (D0 (D2 a)) (D0 (D4 b))
SHR1 H0 (D1 a) (D2 b) => SHR1 H0 (D0 (D1 a)) (D0 (D2 b))
SHR1 H0 (D0 a) (D0 b) => SHR1 H0 (D0 (D0 a)) (D0 (D0 b))

lsn, shr1, thex, tnf', taddc', tsucc, teven, trichotomy :: Name Source

wrapI :: [a] -> (a -> Type) -> [Dec]Source

concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]Source