type-int-0.5.0.2: Type Level 2s- and 16s- Complement Integers

Portabilitynon-portable (MPTC, FD, TH, undecidable instances, missing constructors)
Stabilityexperimental
MaintainerEdward Kmett <ekmett@gmail.com>
Safe HaskellNone

Data.Type.Hex.Stage2

Description

Stage2: Create the D0 and H0 data elements that will be used later. Define utility classes, some classes defined here can not be fleshed out until Stage3.

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

Documentation

data D0 a Source

Instances

TMul (D0 a1) b c => TMul a1 (D0 b) c 
TSucc a b => TAddC' F (DF a) T (D0 b) 
TAddC' F (D0 a) F (D0 a) 
TAddC' F (D0 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) 
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (DF (D0 a)) (DF (D1 b)) 
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (DE (D0 a)) (DD (D1 b)) 
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (DD (D0 a)) (DB (D1 b)) 
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (DC (D0 a)) (D9 (D1 b)) 
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (DB (D0 a)) (D7 (D1 b)) 
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (DA (D0 a)) (D5 (D1 b)) 
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (D9 (D0 a)) (D3 (D1 b)) 
SHR1 H1 (D0 a) (D1 b) => SHR1 H1 (D8 (D0 a)) (D1 (D1 b)) 
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D7 (D8 a)) (DF (D0 b)) 
SHR1 H0 (D0 a) (D0 b) => SHR1 H1 (D7 (D0 a)) (DF (D0 b)) 
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D6 (D8 a)) (DD (D0 b)) 
SHR1 H0 (D0 a) (D0 b) => SHR1 H1 (D6 (D0 a)) (DD (D0 b)) 
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D5 (D8 a)) (DB (D0 b)) 
SHR1 H0 (D0 a) (D0 b) => SHR1 H1 (D5 (D0 a)) (DB (D0 b)) 
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D4 (D8 a)) (D9 (D0 b)) 
SHR1 H0 (D0 a) (D0 b) => SHR1 H1 (D4 (D0 a)) (D9 (D0 b)) 
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D3 (D8 a)) (D7 (D0 b)) 
SHR1 H0 (D0 a) (D0 b) => SHR1 H1 (D3 (D0 a)) (D7 (D0 b)) 
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D2 (D8 a)) (D5 (D0 b)) 
SHR1 H0 (D0 a) (D0 b) => SHR1 H1 (D2 (D0 a)) (D5 (D0 b)) 
SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D1 (D8 a)) (D3 (D0 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 H1 (D0 a) (D1 b) => SHR1 H0 (DF (D0 a)) (DE (D1 b)) 
SHR1 H1 (D0 a) (D1 b) => SHR1 H0 (DE (D0 a)) (DC (D1 b)) 
SHR1 H1 (D0 a) (D1 b) => SHR1 H0 (DD (D0 a)) (DA (D1 b)) 
SHR1 H1 (D0 a) (D1 b) => SHR1 H0 (DC (D0 a)) (D8 (D1 b)) 
SHR1 H1 (D0 a) (D1 b) => SHR1 H0 (DB (D0 a)) (D6 (D1 b)) 
SHR1 H1 (D0 a) (D1 b) => SHR1 H0 (DA (D0 a)) (D4 (D1 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 (D8 a) (D0 b) => SHR1 H0 (D7 (D8 a)) (DE (D0 b)) 
SHR1 H0 (D0 a) (D0 b) => SHR1 H0 (D7 (D0 a)) (DE (D0 b)) 
SHR1 H0 (D8 a) (D0 b) => SHR1 H0 (D6 (D8 a)) (DC (D0 b)) 
SHR1 H0 (D0 a) (D0 b) => SHR1 H0 (D6 (D0 a)) (DC (D0 b)) 
SHR1 H0 (D8 a) (D0 b) => SHR1 H0 (D5 (D8 a)) (DA (D0 b)) 
SHR1 H0 (D0 a) (D0 b) => SHR1 H0 (D5 (D0 a)) (DA (D0 b)) 
SHR1 H0 (D8 a) (D0 b) => SHR1 H0 (D4 (D8 a)) (D8 (D0 b)) 
SHR1 H0 (D0 a) (D0 b) => SHR1 H0 (D4 (D0 a)) (D8 (D0 b)) 
SHR1 H0 (D8 a) (D0 b) => SHR1 H0 (D3 (D8 a)) (D6 (D0 b)) 
SHR1 H0 (D0 a) (D0 b) => SHR1 H0 (D3 (D0 a)) (D6 (D0 b)) 
SHR1 H0 (D8 a) (D0 b) => SHR1 H0 (D2 (D8 a)) (D4 (D0 b)) 
SHR1 H0 (D0 a) (D0 b) => SHR1 H0 (D2 (D0 a)) (D4 (D0 b)) 
SHR1 H0 (D8 a) (D0 b) => SHR1 H0 (D1 (D8 a)) (D2 (D0 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)) 
THex (D0 a) => Show (D0 a) 
(THex a, Ext0 a) => THex (D0 a) 
TEven (D0 a) T 
Trichotomy (D0 T) Negative 
(Trichotomy a b, ExtF a) => Trichotomy (D0 (DF a)) b 
TNF' (D0 F) F F 
(TNF' (D0 a) c b, TIf b (D0 c) F d) => TNF' (D0 (D0 a)) d b 
LSN (D0 T) H0 T 
TSucc a b => TAddC' (DF a) F T (D0 b) 
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) 
LSN (D0 (D0 a)) H0 (D0 a) 
TNot a b => TNot (DF a) (D0 b) 
TNot a b => TNot (D0 a) (DF b) 
(TSucc n m, ExtF n, Ext0 m) => TSucc (DF n) (D0 m) 
TSucc (DE (D0 a)) (DF (D0 a)) 
TSucc (DD (D0 a)) (DE (D0 a)) 
TSucc (DC (D0 a)) (DD (D0 a)) 
TSucc (DB (D0 a)) (DC (D0 a)) 
TSucc (DA (D0 a)) (DB (D0 a)) 
TSucc (D9 (D0 a)) (DA (D0 a)) 
TSucc (D8 (D0 a)) (D9 (D0 a)) 
TSucc (D7 (D0 a)) (D8 (D0 a)) 
TSucc (D6 (D0 a)) (D7 (D0 a)) 
TSucc (D5 (D0 a)) (D6 (D0 a)) 
TSucc (D4 (D0 a)) (D5 (D0 a)) 
TSucc (D3 (D0 a)) (D4 (D0 a)) 
TSucc (D2 (D0 a)) (D3 (D0 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)) 
THex2Binary' a b => THex2Binary' (D0 a) (O (O (O (O b)))) 
TNF' (D0 a) c b => TNF' (DF (D0 a)) (DF c) b 
TNF' (D0 a) c b => TNF' (DE (D0 a)) (DE c) b 
TNF' (D0 a) c b => TNF' (DD (D0 a)) (DD c) b 
TNF' (D0 a) c b => TNF' (DC (D0 a)) (DC c) b 
TNF' (D0 a) c b => TNF' (DB (D0 a)) (DB c) b 
TNF' (D0 a) c b => TNF' (DA (D0 a)) (DA c) b 
TNF' (D0 a) c b => TNF' (D9 (D0 a)) (D9 c) b 
TNF' (D0 a) c b => TNF' (D8 (D0 a)) (D8 c) b 
TNF' (D0 a) c b => TNF' (D7 (D0 a)) (D7 c) b 
TNF' (D0 a) c b => TNF' (D6 (D0 a)) (D6 c) b 
TNF' (D0 a) c b => TNF' (D5 (D0 a)) (D5 c) b 
TNF' (D0 a) c b => TNF' (D4 (D0 a)) (D4 c) b 
TNF' (D0 a) c b => TNF' (D3 (D0 a)) (D3 c) b 
TNF' (D0 a) c b => TNF' (D2 (D0 a)) (D2 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 
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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) (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) F (D0 c) 
TAddC' a b T c => TAddC' (D1 a) (DE b) T (D0 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) 

data D1 a Source

Instances

TAddC' F F T (D1 F) 
SHR1 H1 F (D1 F) 
TPow' a F (D1 F) 
TSucc F (D1 F) 
(TMul (D0 a1) b c, TAdd' a1 c d) => TMul a1 (D1 b) d 
TAddC' F (D1 a) F (D1 a) 
TAddC' F (D1 a) T (D2 a) 
TAddC' F (D0 a) T (D1 a) 
TAddC' T (D2 a) F (D1 a) 
TAddC' T (D1 a) T (D1 a) 
TAddC' T (D1 a) F (D0 a) 
SHR1 H1 (DF F) (DF (D1 F)) 
SHR1 H1 (D8 a) (D1 b) => SHR1 H1 (DF (D8 a)) (DF (D1 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 (D8 a) (D1 b) => SHR1 H1 (DE (D8 a)) (DD (D1 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 (D8 a) (D1 b) => SHR1 H1 (DD (D8 a)) (DB (D1 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 (D8 a) (D1 b) => SHR1 H1 (DC (D8 a)) (D9 (D1 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 (D8 a) (D1 b) => SHR1 H1 (DB (D8 a)) (D7 (D1 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 (D8 a) (D1 b) => SHR1 H1 (DA (D8 a)) (D5 (D1 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 (D8 a) (D1 b) => SHR1 H1 (D9 (D8 a)) (D3 (D1 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 H0 (D1 a) (D2 b) => SHR1 H1 (D7 (D1 a)) (DF (D2 b)) 
SHR1 H0 (D1 a) (D2 b) => SHR1 H1 (D6 (D1 a)) (DD (D2 b)) 
SHR1 H0 (D1 a) (D2 b) => SHR1 H1 (D5 (D1 a)) (DB (D2 b)) 
SHR1 H0 (D1 a) (D2 b) => SHR1 H1 (D4 (D1 a)) (D9 (D2 b)) 
SHR1 H0 (D1 a) (D2 b) => SHR1 H1 (D3 (D1 a)) (D7 (D2 b)) 
SHR1 H0 (D1 a) (D2 b) => SHR1 H1 (D2 (D1 a)) (D5 (D2 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 H1 (D8 a) (D1 b) => SHR1 H0 (DF (D8 a)) (DE (D1 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 H1 (D8 a) (D1 b) => SHR1 H0 (DE (D8 a)) (DC (D1 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 H1 (D8 a) (D1 b) => SHR1 H0 (DD (D8 a)) (DA (D1 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 H1 (D8 a) (D1 b) => SHR1 H0 (DC (D8 a)) (D8 (D1 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 H1 (D8 a) (D1 b) => SHR1 H0 (DB (D8 a)) (D6 (D1 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 H1 (D8 a) (D1 b) => SHR1 H0 (DA (D8 a)) (D4 (D1 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 H1 (D8 a) (D1 b) => SHR1 H0 (D9 (D8 a)) (D2 (D1 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 H1 (D8 a) (D1 b) => SHR1 H0 (D8 (D8 a)) (D0 (D1 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 (D1 a) (D2 b) => SHR1 H0 (D7 (D1 a)) (DE (D2 b)) 
SHR1 H0 (D1 a) (D2 b) => SHR1 H0 (D6 (D1 a)) (DC (D2 b)) 
SHR1 H0 (D1 a) (D2 b) => SHR1 H0 (D5 (D1 a)) (DA (D2 b)) 
SHR1 H0 (D1 a) (D2 b) => SHR1 H0 (D4 (D1 a)) (D8 (D2 b)) 
SHR1 H0 (D1 a) (D2 b) => SHR1 H0 (D3 (D1 a)) (D6 (D2 b)) 
SHR1 H0 (D1 a) (D2 b) => SHR1 H0 (D2 (D1 a)) (D4 (D2 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 (D1 a) (D2 b) => SHR1 H0 (D0 (D1 a)) (D0 (D2 b)) 
THex (D1 a) => Show (D1 a) 
THex a => THex (D1 a) 
TEven (D1 a) F 
Trichotomy (D1 F) Positive 
Trichotomy (D1 T) Negative 
(Trichotomy a b, Ext0 a) => Trichotomy (D1 (DF a)) b 
LSN (D1 F) H1 F 
LSN (D1 T) H1 T 
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) 
TAddC' (D0 a) F T (D1 a) 
LSN (D1 (D1 a)) H1 (D1 a) 
TNot a b => TNot (DE a) (D1 b) 
TNot a b => TNot (D1 a) (DE b) 
TSucc (DE (D1 a)) (DF (D1 a)) 
TSucc (DD (D1 a)) (DE (D1 a)) 
TSucc (DC (D1 a)) (DD (D1 a)) 
TSucc (DB (D1 a)) (DC (D1 a)) 
TSucc (DA (D1 a)) (DB (D1 a)) 
TSucc (D9 (D1 a)) (DA (D1 a)) 
TSucc (D8 (D1 a)) (D9 (D1 a)) 
TSucc (D7 (D1 a)) (D8 (D1 a)) 
TSucc (D6 (D1 a)) (D7 (D1 a)) 
TSucc (D5 (D1 a)) (D6 (D1 a)) 
TSucc (D4 (D1 a)) (D5 (D1 a)) 
TSucc (D3 (D1 a)) (D4 (D1 a)) 
TSucc (D2 (D1 a)) (D3 (D1 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)) 
THex2Binary' a b => THex2Binary' (D1 a) (I (O (O (O b)))) 
TNF' (D1 a) c b => TNF' (DF (D1 a)) (DF c) b 
TNF' (D1 a) c b => TNF' (DE (D1 a)) (DE c) b 
TNF' (D1 a) c b => TNF' (DD (D1 a)) (DD c) b 
TNF' (D1 a) c b => TNF' (DC (D1 a)) (DC c) b 
TNF' (D1 a) c b => TNF' (DB (D1 a)) (DB c) b 
TNF' (D1 a) c b => TNF' (DA (D1 a)) (DA c) b 
TNF' (D1 a) c b => TNF' (D9 (D1 a)) (D9 c) b 
TNF' (D1 a) c b => TNF' (D8 (D1 a)) (D8 c) b 
TNF' (D1 a) c b => TNF' (D7 (D1 a)) (D7 c) b 
TNF' (D1 a) c b => TNF' (D6 (D1 a)) (D6 c) b 
TNF' (D1 a) c b => TNF' (D5 (D1 a)) (D5 c) b 
TNF' (D1 a) c b => TNF' (D4 (D1 a)) (D4 c) b 
TNF' (D1 a) c b => TNF' (D3 (D1 a)) (D3 c) b 
TNF' (D1 a) c b => TNF' (D2 (D1 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' (D1 a) c b => TNF' (D0 (D1 a)) (D0 c) b 
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' (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) (D1 b) T (D0 c) 
TAddC' a b F c => TAddC' (DE a) (D1 b) F (DF 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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) 

data D2 a Source

Instances

(TMul (D0 a1) b c, SHR1 H0 a1 a2, TAdd' a2 c d) => TMul a1 (D2 b) d 
TAddC' F (D2 a) F (D2 a) 
TAddC' F (D2 a) T (D3 a) 
TAddC' F (D1 a) T (D2 a) 
TAddC' T (D3 a) F (D2 a) 
TAddC' T (D2 a) T (D2 a) 
TAddC' T (D2 a) F (D1 a) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DF (D2 a)) (DF (D5 b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DE (D2 a)) (DD (D5 b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DD (D2 a)) (DB (D5 b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DC (D2 a)) (D9 (D5 b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DB (D2 a)) (D7 (D5 b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DA (D2 a)) (D5 (D5 b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (D9 (D2 a)) (D3 (D5 b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (D8 (D2 a)) (D1 (D5 b)) 
SHR1 H0 (D9 a) (D2 b) => SHR1 H1 (D7 (D9 a)) (DF (D2 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 (D9 a) (D2 b) => SHR1 H1 (D6 (D9 a)) (DD (D2 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 (D9 a) (D2 b) => SHR1 H1 (D5 (D9 a)) (DB (D2 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 (D9 a) (D2 b) => SHR1 H1 (D4 (D9 a)) (D9 (D2 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 (D9 a) (D2 b) => SHR1 H1 (D3 (D9 a)) (D7 (D2 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 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 H0 (D9 a) (D2 b) => SHR1 H1 (D1 (D9 a)) (D3 (D2 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 (D9 a) (D2 b) => SHR1 H1 (D0 (D9 a)) (D1 (D2 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 H1 (D2 a) (D5 b) => SHR1 H0 (DF (D2 a)) (DE (D5 b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DE (D2 a)) (DC (D5 b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DD (D2 a)) (DA (D5 b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DC (D2 a)) (D8 (D5 b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DB (D2 a)) (D6 (D5 b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DA (D2 a)) (D4 (D5 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 H1 (D2 a) (D5 b) => SHR1 H0 (D8 (D2 a)) (D0 (D5 b)) 
SHR1 H0 (D9 a) (D2 b) => SHR1 H0 (D7 (D9 a)) (DE (D2 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 (D9 a) (D2 b) => SHR1 H0 (D6 (D9 a)) (DC (D2 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 (D9 a) (D2 b) => SHR1 H0 (D5 (D9 a)) (DA (D2 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 (D9 a) (D2 b) => SHR1 H0 (D4 (D9 a)) (D8 (D2 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 (D9 a) (D2 b) => SHR1 H0 (D3 (D9 a)) (D6 (D2 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 (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 (D9 a) (D2 b) => SHR1 H0 (D0 (D9 a)) (D0 (D2 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)) 
THex (D2 a) => Show (D2 a) 
THex a => THex (D2 a) 
TEven (D2 a) T 
Trichotomy (D2 F) Positive 
Trichotomy (D2 T) Negative 
LSN (D2 F) H2 F 
LSN (D2 T) H2 T 
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 T (D2 a) 
LSN (D2 (D2 a)) H2 (D2 a) 
TNot a b => TNot (DD a) (D2 b) 
TNot a b => TNot (D2 a) (DD b) 
TSucc (DE (D2 a)) (DF (D2 a)) 
TSucc (DD (D2 a)) (DE (D2 a)) 
TSucc (DC (D2 a)) (DD (D2 a)) 
TSucc (DB (D2 a)) (DC (D2 a)) 
TSucc (DA (D2 a)) (DB (D2 a)) 
TSucc (D9 (D2 a)) (DA (D2 a)) 
TSucc (D8 (D2 a)) (D9 (D2 a)) 
TSucc (D7 (D2 a)) (D8 (D2 a)) 
TSucc (D6 (D2 a)) (D7 (D2 a)) 
TSucc (D5 (D2 a)) (D6 (D2 a)) 
TSucc (D4 (D2 a)) (D5 (D2 a)) 
TSucc (D3 (D2 a)) (D4 (D2 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 (D2 a)) (D1 (D2 a)) 
THex2Binary' a b => THex2Binary' (D2 a) (O (I (O (O b)))) 
TNF' (D2 a) c b => TNF' (DF (D2 a)) (DF c) b 
TNF' (D2 a) c b => TNF' (DE (D2 a)) (DE c) b 
TNF' (D2 a) c b => TNF' (DD (D2 a)) (DD c) b 
TNF' (D2 a) c b => TNF' (DC (D2 a)) (DC c) b 
TNF' (D2 a) c b => TNF' (DB (D2 a)) (DB c) b 
TNF' (D2 a) c b => TNF' (DA (D2 a)) (DA c) b 
TNF' (D2 a) c b => TNF' (D9 (D2 a)) (D9 c) b 
TNF' (D2 a) c b => TNF' (D8 (D2 a)) (D8 c) b 
TNF' (D2 a) c b => TNF' (D7 (D2 a)) (D7 c) b 
TNF' (D2 a) c b => TNF' (D6 (D2 a)) (D6 c) b 
TNF' (D2 a) c b => TNF' (D5 (D2 a)) (D5 c) b 
TNF' (D2 a) c b => TNF' (D4 (D2 a)) (D4 c) b 
TNF' (D2 a) c b => TNF' (D3 (D2 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' (D2 a) c b => TNF' (D1 (D2 a)) (D1 c) b 
TNF' (D2 a) c b => TNF' (D0 (D2 a)) (D0 c) b 
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' (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) (D2 b) T (D1 c) 
TAddC' a b T c => TAddC' (DE a) (D2 b) F (D0 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) (D2 b) T (D0 c) 
TAddC' a b F c => TAddC' (DD a) (D2 b) F (DF 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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) F (D2 c) 
TAddC' a b F c => TAddC' (D1 a) (D0 b) T (D2 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) 

data D3 a Source

Instances

(TMul (D0 a1) b c, SHR1 H0 a1 a2, TAdd' a1 a2 a3, TAdd' a3 c d) => TMul a1 (D3 b) d 
TAddC' F (D3 a) F (D3 a) 
TAddC' F (D3 a) T (D4 a) 
TAddC' F (D2 a) T (D3 a) 
TAddC' T (D4 a) F (D3 a) 
TAddC' T (D3 a) T (D3 a) 
TAddC' T (D3 a) F (D2 a) 
SHR1 H1 (D9 a) (D3 b) => SHR1 H1 (DF (D9 a)) (DF (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DF (D3 a)) (DF (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (DF (D1 a)) (DF (D3 b)) 
SHR1 H1 (D9 a) (D3 b) => SHR1 H1 (DE (D9 a)) (DD (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DE (D3 a)) (DD (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (DE (D1 a)) (DD (D3 b)) 
SHR1 H1 (D9 a) (D3 b) => SHR1 H1 (DD (D9 a)) (DB (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DD (D3 a)) (DB (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (DD (D1 a)) (DB (D3 b)) 
SHR1 H1 (D9 a) (D3 b) => SHR1 H1 (DC (D9 a)) (D9 (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DC (D3 a)) (D9 (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (DC (D1 a)) (D9 (D3 b)) 
SHR1 H1 (D9 a) (D3 b) => SHR1 H1 (DB (D9 a)) (D7 (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DB (D3 a)) (D7 (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (DB (D1 a)) (D7 (D3 b)) 
SHR1 H1 (D9 a) (D3 b) => SHR1 H1 (DA (D9 a)) (D5 (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DA (D3 a)) (D5 (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (DA (D1 a)) (D5 (D3 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 (D9 a) (D3 b) => SHR1 H1 (D8 (D9 a)) (D1 (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (D8 (D3 a)) (D1 (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H1 (D8 (D1 a)) (D1 (D3 b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D7 (D3 a)) (DF (D6 b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D6 (D3 a)) (DD (D6 b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D5 (D3 a)) (DB (D6 b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D4 (D3 a)) (D9 (D6 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 H0 (D3 a) (D6 b) => SHR1 H1 (D2 (D3 a)) (D5 (D6 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 H0 (D3 a) (D6 b) => SHR1 H1 (D0 (D3 a)) (D1 (D6 b)) 
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (DF (D9 a)) (DE (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (DF (D3 a)) (DE (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (DF (D1 a)) (DE (D3 b)) 
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (DE (D9 a)) (DC (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (DE (D3 a)) (DC (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (DE (D1 a)) (DC (D3 b)) 
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (DD (D9 a)) (DA (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (DD (D3 a)) (DA (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (DD (D1 a)) (DA (D3 b)) 
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (DC (D9 a)) (D8 (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (DC (D3 a)) (D8 (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (DC (D1 a)) (D8 (D3 b)) 
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (DB (D9 a)) (D6 (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (DB (D3 a)) (D6 (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (DB (D1 a)) (D6 (D3 b)) 
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (DA (D9 a)) (D4 (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (DA (D3 a)) (D4 (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (DA (D1 a)) (D4 (D3 b)) 
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (D9 (D9 a)) (D2 (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (D9 (D3 a)) (D2 (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (D9 (D1 a)) (D2 (D3 b)) 
SHR1 H1 (D9 a) (D3 b) => SHR1 H0 (D8 (D9 a)) (D0 (D3 b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H0 (D8 (D3 a)) (D0 (D7 b)) 
SHR1 H1 (D1 a) (D3 b) => SHR1 H0 (D8 (D1 a)) (D0 (D3 b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D7 (D3 a)) (DE (D6 b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D6 (D3 a)) (DC (D6 b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D5 (D3 a)) (DA (D6 b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D4 (D3 a)) (D8 (D6 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 (D3 a) (D6 b) => SHR1 H0 (D2 (D3 a)) (D4 (D6 b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D1 (D3 a)) (D2 (D6 b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D0 (D3 a)) (D0 (D6 b)) 
THex (D3 a) => Show (D3 a) 
THex a => THex (D3 a) 
TEven (D3 a) F 
Trichotomy (D3 F) Positive 
Trichotomy (D3 T) Negative 
LSN (D3 F) H3 F 
LSN (D3 T) H3 T 
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 T (D3 a) 
LSN (D3 (D3 a)) H3 (D3 a) 
TNot a b => TNot (DC a) (D3 b) 
TNot a b => TNot (D3 a) (DC b) 
TSucc (DE (D3 a)) (DF (D3 a)) 
TSucc (DD (D3 a)) (DE (D3 a)) 
TSucc (DC (D3 a)) (DD (D3 a)) 
TSucc (DB (D3 a)) (DC (D3 a)) 
TSucc (DA (D3 a)) (DB (D3 a)) 
TSucc (D9 (D3 a)) (DA (D3 a)) 
TSucc (D8 (D3 a)) (D9 (D3 a)) 
TSucc (D7 (D3 a)) (D8 (D3 a)) 
TSucc (D6 (D3 a)) (D7 (D3 a)) 
TSucc (D5 (D3 a)) (D6 (D3 a)) 
TSucc (D4 (D3 a)) (D5 (D3 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 (D3 a)) (D2 (D3 a)) 
TSucc (D0 (D3 a)) (D1 (D3 a)) 
THex2Binary' a b => THex2Binary' (D3 a) (I (I (O (O b)))) 
TNF' (D3 a) c b => TNF' (DF (D3 a)) (DF c) b 
TNF' (D3 a) c b => TNF' (DE (D3 a)) (DE c) b 
TNF' (D3 a) c b => TNF' (DD (D3 a)) (DD c) b 
TNF' (D3 a) c b => TNF' (DC (D3 a)) (DC c) b 
TNF' (D3 a) c b => TNF' (DB (D3 a)) (DB c) b 
TNF' (D3 a) c b => TNF' (DA (D3 a)) (DA c) b 
TNF' (D3 a) c b => TNF' (D9 (D3 a)) (D9 c) b 
TNF' (D3 a) c b => TNF' (D8 (D3 a)) (D8 c) b 
TNF' (D3 a) c b => TNF' (D7 (D3 a)) (D7 c) b 
TNF' (D3 a) c b => TNF' (D6 (D3 a)) (D6 c) b 
TNF' (D3 a) c b => TNF' (D5 (D3 a)) (D5 c) b 
TNF' (D3 a) c b => TNF' (D4 (D3 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' (D3 a) c b => TNF' (D2 (D3 a)) (D2 c) b 
TNF' (D3 a) c b => TNF' (D1 (D3 a)) (D1 c) b 
TNF' (D3 a) c b => TNF' (D0 (D3 a)) (D0 c) b 
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' (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) (D3 b) T (D2 c) 
TAddC' a b T c => TAddC' (DE a) (D3 b) F (D1 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) (D3 b) T (D1 c) 
TAddC' a b T c => TAddC' (DD a) (D3 b) F (D0 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) (D3 b) T (D0 c) 
TAddC' a b F c => TAddC' (DC a) (D3 b) F (DF 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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) (D1 b) F (D3 c) 
TAddC' a b F c => TAddC' (D2 a) (D0 b) T (D3 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) F (D3 c) 
TAddC' a b F c => TAddC' (D1 a) (D1 b) T (D3 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) 

data D4 a Source

Instances

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, TAdd' a4 c d) => TMul a1 (D4 b) d 
TAddC' F (D4 a) F (D4 a) 
TAddC' F (D4 a) T (D5 a) 
TAddC' F (D3 a) T (D4 a) 
TAddC' T (D5 a) F (D4 a) 
TAddC' T (D4 a) T (D4 a) 
TAddC' T (D4 a) F (D3 a) 
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (DF (D4 a)) (DF (D9 b)) 
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (DE (D4 a)) (DD (D9 b)) 
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (DD (D4 a)) (DB (D9 b)) 
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (DC (D4 a)) (D9 (D9 b)) 
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (DB (D4 a)) (D7 (D9 b)) 
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (DA (D4 a)) (D5 (D9 b)) 
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (D9 (D4 a)) (D3 (D9 b)) 
SHR1 H1 (D4 a) (D9 b) => SHR1 H1 (D8 (D4 a)) (D1 (D9 b)) 
SHR1 H0 (DA a) (D4 b) => SHR1 H1 (D7 (DA a)) (DF (D4 b)) 
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D7 (D4 a)) (DF (D8 b)) 
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D7 (D2 a)) (DF (D4 b)) 
SHR1 H0 (DA a) (D4 b) => SHR1 H1 (D6 (DA a)) (DD (D4 b)) 
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D6 (D4 a)) (DD (D8 b)) 
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D6 (D2 a)) (DD (D4 b)) 
SHR1 H0 (DA a) (D4 b) => SHR1 H1 (D5 (DA a)) (DB (D4 b)) 
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D5 (D4 a)) (DB (D8 b)) 
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D5 (D2 a)) (DB (D4 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 H0 (DA a) (D4 b) => SHR1 H1 (D3 (DA a)) (D7 (D4 b)) 
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D3 (D4 a)) (D7 (D8 b)) 
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D3 (D2 a)) (D7 (D4 b)) 
SHR1 H0 (DA a) (D4 b) => SHR1 H1 (D2 (DA a)) (D5 (D4 b)) 
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D2 (D4 a)) (D5 (D8 b)) 
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D2 (D2 a)) (D5 (D4 b)) 
SHR1 H0 (DA a) (D4 b) => SHR1 H1 (D1 (DA a)) (D3 (D4 b)) 
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D1 (D4 a)) (D3 (D8 b)) 
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D1 (D2 a)) (D3 (D4 b)) 
SHR1 H0 (DA a) (D4 b) => SHR1 H1 (D0 (DA a)) (D1 (D4 b)) 
SHR1 H0 (D4 a) (D8 b) => SHR1 H1 (D0 (D4 a)) (D1 (D8 b)) 
SHR1 H0 (D2 a) (D4 b) => SHR1 H1 (D0 (D2 a)) (D1 (D4 b)) 
SHR1 H1 (D4 a) (D9 b) => SHR1 H0 (DF (D4 a)) (DE (D9 b)) 
SHR1 H1 (D4 a) (D9 b) => SHR1 H0 (DE (D4 a)) (DC (D9 b)) 
SHR1 H1 (D4 a) (D9 b) => SHR1 H0 (DD (D4 a)) (DA (D9 b)) 
SHR1 H1 (D4 a) (D9 b) => SHR1 H0 (DC (D4 a)) (D8 (D9 b)) 
SHR1 H1 (D4 a) (D9 b) => SHR1 H0 (DB (D4 a)) (D6 (D9 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 H1 (D4 a) (D9 b) => SHR1 H0 (D9 (D4 a)) (D2 (D9 b)) 
SHR1 H1 (D4 a) (D9 b) => SHR1 H0 (D8 (D4 a)) (D0 (D9 b)) 
SHR1 H0 (DA a) (D4 b) => SHR1 H0 (D7 (DA a)) (DE (D4 b)) 
SHR1 H0 (D4 a) (D8 b) => SHR1 H0 (D7 (D4 a)) (DE (D8 b)) 
SHR1 H0 (D2 a) (D4 b) => SHR1 H0 (D7 (D2 a)) (DE (D4 b)) 
SHR1 H0 (DA a) (D4 b) => SHR1 H0 (D6 (DA a)) (DC (D4 b)) 
SHR1 H0 (D4 a) (D8 b) => SHR1 H0 (D6 (D4 a)) (DC (D8 b)) 
SHR1 H0 (D2 a) (D4 b) => SHR1 H0 (D6 (D2 a)) (DC (D4 b)) 
SHR1 H0 (DA a) (D4 b) => SHR1 H0 (D5 (DA a)) (DA (D4 b)) 
SHR1 H0 (D4 a) (D8 b) => SHR1 H0 (D5 (D4 a)) (DA (D8 b)) 
SHR1 H0 (D2 a) (D4 b) => SHR1 H0 (D5 (D2 a)) (DA (D4 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 (DA a) (D4 b) => SHR1 H0 (D3 (DA a)) (D6 (D4 b)) 
SHR1 H0 (D4 a) (D8 b) => SHR1 H0 (D3 (D4 a)) (D6 (D8 b)) 
SHR1 H0 (D2 a) (D4 b) => SHR1 H0 (D3 (D2 a)) (D6 (D4 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 (DA a) (D4 b) => SHR1 H0 (D1 (DA a)) (D2 (D4 b)) 
SHR1 H0 (D4 a) (D8 b) => SHR1 H0 (D1 (D4 a)) (D2 (D8 b)) 
SHR1 H0 (D2 a) (D4 b) => SHR1 H0 (D1 (D2 a)) (D2 (D4 b)) 
SHR1 H0 (DA a) (D4 b) => SHR1 H0 (D0 (DA a)) (D0 (D4 b)) 
SHR1 H0 (D4 a) (D8 b) => SHR1 H0 (D0 (D4 a)) (D0 (D8 b)) 
SHR1 H0 (D2 a) (D4 b) => SHR1 H0 (D0 (D2 a)) (D0 (D4 b)) 
THex (D4 a) => Show (D4 a) 
THex a => THex (D4 a) 
TEven (D4 a) T 
Trichotomy (D4 F) Positive 
Trichotomy (D4 T) Negative 
LSN (D4 F) H4 F 
LSN (D4 T) H4 T 
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 T (D4 a) 
LSN (D4 (D4 a)) H4 (D4 a) 
TNot a b => TNot (DB a) (D4 b) 
TNot a b => TNot (D4 a) (DB b) 
TSucc (DE (D4 a)) (DF (D4 a)) 
TSucc (DD (D4 a)) (DE (D4 a)) 
TSucc (DC (D4 a)) (DD (D4 a)) 
TSucc (DB (D4 a)) (DC (D4 a)) 
TSucc (DA (D4 a)) (DB (D4 a)) 
TSucc (D9 (D4 a)) (DA (D4 a)) 
TSucc (D8 (D4 a)) (D9 (D4 a)) 
TSucc (D7 (D4 a)) (D8 (D4 a)) 
TSucc (D6 (D4 a)) (D7 (D4 a)) 
TSucc (D5 (D4 a)) (D6 (D4 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 (D4 a)) (D3 (D4 a)) 
TSucc (D1 (D4 a)) (D2 (D4 a)) 
TSucc (D0 (D4 a)) (D1 (D4 a)) 
THex2Binary' a b => THex2Binary' (D4 a) (O (O (I (O b)))) 
TNF' (D4 a) c b => TNF' (DF (D4 a)) (DF c) b 
TNF' (D4 a) c b => TNF' (DE (D4 a)) (DE c) b 
TNF' (D4 a) c b => TNF' (DD (D4 a)) (DD c) b 
TNF' (D4 a) c b => TNF' (DC (D4 a)) (DC c) b 
TNF' (D4 a) c b => TNF' (DB (D4 a)) (DB c) b 
TNF' (D4 a) c b => TNF' (DA (D4 a)) (DA c) b 
TNF' (D4 a) c b => TNF' (D9 (D4 a)) (D9 c) b 
TNF' (D4 a) c b => TNF' (D8 (D4 a)) (D8 c) b 
TNF' (D4 a) c b => TNF' (D7 (D4 a)) (D7 c) b 
TNF' (D4 a) c b => TNF' (D6 (D4 a)) (D6 c) b 
TNF' (D4 a) c b => TNF' (D5 (D4 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' (D4 a) c b => TNF' (D3 (D4 a)) (D3 c) b 
TNF' (D4 a) c b => TNF' (D2 (D4 a)) (D2 c) b 
TNF' (D4 a) c b => TNF' (D1 (D4 a)) (D1 c) b 
TNF' (D4 a) c b => TNF' (D0 (D4 a)) (D0 c) b 
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' (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) (D4 b) T (D3 c) 
TAddC' a b T c => TAddC' (DE a) (D4 b) F (D2 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) (D4 b) T (D2 c) 
TAddC' a b T c => TAddC' (DD a) (D4 b) F (D1 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) (D4 b) T (D1 c) 
TAddC' a b T c => TAddC' (DC a) (D4 b) F (D0 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) (D4 b) T (D0 c) 
TAddC' a b F c => TAddC' (DB a) (D4 b) F (DF 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 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 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 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 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 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 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 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 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 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 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 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 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 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) (D1 b) F (D4 c) 
TAddC' a b F c => TAddC' (D3 a) (D0 b) T (D4 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) (D2 b) F (D4 c) 
TAddC' a b F c => TAddC' (D2 a) (D1 b) T (D4 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) F (D4 c) 
TAddC' a b F c => TAddC' (D1 a) (D2 b) T (D4 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) 

data D5 a Source

Instances

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, TAdd' a1 a4 a5, TAdd' a5 c d) => TMul a1 (D5 b) d 
TAddC' F (D5 a) F (D5 a) 
TAddC' F (D5 a) T (D6 a) 
TAddC' F (D4 a) T (D5 a) 
TAddC' T (D6 a) F (D5 a) 
TAddC' T (D5 a) T (D5 a) 
TAddC' T (D5 a) F (D4 a) 
SHR1 H1 (DA a) (D5 b) => SHR1 H1 (DF (DA a)) (DF (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (DF (D5 a)) (DF (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DF (D2 a)) (DF (D5 b)) 
SHR1 H1 (DA a) (D5 b) => SHR1 H1 (DE (DA a)) (DD (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (DE (D5 a)) (DD (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DE (D2 a)) (DD (D5 b)) 
SHR1 H1 (DA a) (D5 b) => SHR1 H1 (DD (DA a)) (DB (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (DD (D5 a)) (DB (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DD (D2 a)) (DB (D5 b)) 
SHR1 H1 (DA a) (D5 b) => SHR1 H1 (DC (DA a)) (D9 (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (DC (D5 a)) (D9 (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DC (D2 a)) (D9 (D5 b)) 
SHR1 H1 (DA a) (D5 b) => SHR1 H1 (DB (DA a)) (D7 (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (DB (D5 a)) (D7 (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (DB (D2 a)) (D7 (D5 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 (DA a) (D5 b) => SHR1 H1 (D9 (DA a)) (D3 (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (D9 (D5 a)) (D3 (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (D9 (D2 a)) (D3 (D5 b)) 
SHR1 H1 (DA a) (D5 b) => SHR1 H1 (D8 (DA a)) (D1 (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H1 (D8 (D5 a)) (D1 (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H1 (D8 (D2 a)) (D1 (D5 b)) 
SHR1 H0 (D5 a) (DA b) => SHR1 H1 (D7 (D5 a)) (DF (DA b)) 
SHR1 H0 (D5 a) (DA b) => SHR1 H1 (D6 (D5 a)) (DD (DA 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 H0 (D5 a) (DA b) => SHR1 H1 (D4 (D5 a)) (D9 (DA b)) 
SHR1 H0 (D5 a) (DA b) => SHR1 H1 (D3 (D5 a)) (D7 (DA 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 H0 (D5 a) (DA b) => SHR1 H1 (D1 (D5 a)) (D3 (DA b)) 
SHR1 H0 (D5 a) (DA b) => SHR1 H1 (D0 (D5 a)) (D1 (DA b)) 
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (DF (DA a)) (DE (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (DF (D5 a)) (DE (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DF (D2 a)) (DE (D5 b)) 
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (DE (DA a)) (DC (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (DE (D5 a)) (DC (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DE (D2 a)) (DC (D5 b)) 
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (DD (DA a)) (DA (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (DD (D5 a)) (DA (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DD (D2 a)) (DA (D5 b)) 
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (DC (DA a)) (D8 (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (DC (D5 a)) (D8 (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DC (D2 a)) (D8 (D5 b)) 
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (DB (DA a)) (D6 (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (DB (D5 a)) (D6 (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DB (D2 a)) (D6 (D5 b)) 
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (DA (DA a)) (D4 (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (DA (D5 a)) (D4 (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (DA (D2 a)) (D4 (D5 b)) 
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (D9 (DA a)) (D2 (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (D9 (D5 a)) (D2 (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (D9 (D2 a)) (D2 (D5 b)) 
SHR1 H1 (DA a) (D5 b) => SHR1 H0 (D8 (DA a)) (D0 (D5 b)) 
SHR1 H1 (D5 a) (DB b) => SHR1 H0 (D8 (D5 a)) (D0 (DB b)) 
SHR1 H1 (D2 a) (D5 b) => SHR1 H0 (D8 (D2 a)) (D0 (D5 b)) 
SHR1 H0 (D5 a) (DA b) => SHR1 H0 (D7 (D5 a)) (DE (DA b)) 
SHR1 H0 (D5 a) (DA b) => SHR1 H0 (D6 (D5 a)) (DC (DA 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 (D5 a) (DA b) => SHR1 H0 (D4 (D5 a)) (D8 (DA b)) 
SHR1 H0 (D5 a) (DA b) => SHR1 H0 (D3 (D5 a)) (D6 (DA b)) 
SHR1 H0 (D5 a) (DA b) => SHR1 H0 (D2 (D5 a)) (D4 (DA b)) 
SHR1 H0 (D5 a) (DA b) => SHR1 H0 (D1 (D5 a)) (D2 (DA b)) 
SHR1 H0 (D5 a) (DA b) => SHR1 H0 (D0 (D5 a)) (D0 (DA b)) 
THex (D5 a) => Show (D5 a) 
THex a => THex (D5 a) 
TEven (D5 a) F 
Trichotomy (D5 F) Positive 
Trichotomy (D5 T) Negative 
LSN (D5 F) H5 F 
LSN (D5 T) H5 T 
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 T (D5 a) 
LSN (D5 (D5 a)) H5 (D5 a) 
TNot a b => TNot (DA a) (D5 b) 
TNot a b => TNot (D5 a) (DA b) 
TSucc (DE (D5 a)) (DF (D5 a)) 
TSucc (DD (D5 a)) (DE (D5 a)) 
TSucc (DC (D5 a)) (DD (D5 a)) 
TSucc (DB (D5 a)) (DC (D5 a)) 
TSucc (DA (D5 a)) (DB (D5 a)) 
TSucc (D9 (D5 a)) (DA (D5 a)) 
TSucc (D8 (D5 a)) (D9 (D5 a)) 
TSucc (D7 (D5 a)) (D8 (D5 a)) 
TSucc (D6 (D5 a)) (D7 (D5 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 (D5 a)) (D4 (D5 a)) 
TSucc (D2 (D5 a)) (D3 (D5 a)) 
TSucc (D1 (D5 a)) (D2 (D5 a)) 
TSucc (D0 (D5 a)) (D1 (D5 a)) 
THex2Binary' a b => THex2Binary' (D5 a) (I (O (I (O b)))) 
TNF' (D5 a) c b => TNF' (DF (D5 a)) (DF c) b 
TNF' (D5 a) c b => TNF' (DE (D5 a)) (DE c) b 
TNF' (D5 a) c b => TNF' (DD (D5 a)) (DD c) b 
TNF' (D5 a) c b => TNF' (DC (D5 a)) (DC c) b 
TNF' (D5 a) c b => TNF' (DB (D5 a)) (DB c) b 
TNF' (D5 a) c b => TNF' (DA (D5 a)) (DA c) b 
TNF' (D5 a) c b => TNF' (D9 (D5 a)) (D9 c) b 
TNF' (D5 a) c b => TNF' (D8 (D5 a)) (D8 c) b 
TNF' (D5 a) c b => TNF' (D7 (D5 a)) (D7 c) b 
TNF' (D5 a) c b => TNF' (D6 (D5 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' (D5 a) c b => TNF' (D4 (D5 a)) (D4 c) b 
TNF' (D5 a) c b => TNF' (D3 (D5 a)) (D3 c) b 
TNF' (D5 a) c b => TNF' (D2 (D5 a)) (D2 c) b 
TNF' (D5 a) c b => TNF' (D1 (D5 a)) (D1 c) b 
TNF' (D5 a) c b => TNF' (D0 (D5 a)) (D0 c) b 
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' (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) (D5 b) T (D4 c) 
TAddC' a b T c => TAddC' (DE a) (D5 b) F (D3 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) (D5 b) T (D3 c) 
TAddC' a b T c => TAddC' (DD a) (D5 b) F (D2 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) (D5 b) T (D2 c) 
TAddC' a b T c => TAddC' (DC a) (D5 b) F (D1 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) (D5 b) T (D1 c) 
TAddC' a b T c => TAddC' (DB a) (D5 b) F (D0 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) (D5 b) T (D0 c) 
TAddC' a b F c => TAddC' (DA a) (D5 b) F (DF 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 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 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 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 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 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 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 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 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 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) (D1 b) F (D5 c) 
TAddC' a b F c => TAddC' (D4 a) (D0 b) T (D5 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) (D2 b) F (D5 c) 
TAddC' a b F c => TAddC' (D3 a) (D1 b) T (D5 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) (D3 b) F (D5 c) 
TAddC' a b F c => TAddC' (D2 a) (D2 b) T (D5 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) F (D5 c) 
TAddC' a b F c => TAddC' (D1 a) (D3 b) T (D5 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) 

data D6 a Source

Instances

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, TAdd' a2 a4 a6, TAdd' a6 c d) => TMul a1 (D6 b) d 
TAddC' F (D6 a) F (D6 a) 
TAddC' F (D6 a) T (D7 a) 
TAddC' F (D5 a) T (D6 a) 
TAddC' T (D7 a) F (D6 a) 
TAddC' T (D6 a) T (D6 a) 
TAddC' T (D6 a) F (D5 a) 
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (DF (D6 a)) (DF (DD b)) 
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (DE (D6 a)) (DD (DD b)) 
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (DD (D6 a)) (DB (DD b)) 
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (DC (D6 a)) (D9 (DD b)) 
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (DB (D6 a)) (D7 (DD b)) 
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (DA (D6 a)) (D5 (DD b)) 
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (D9 (D6 a)) (D3 (DD b)) 
SHR1 H1 (D6 a) (DD b) => SHR1 H1 (D8 (D6 a)) (D1 (DD b)) 
SHR1 H0 (DB a) (D6 b) => SHR1 H1 (D7 (DB a)) (DF (D6 b)) 
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D7 (D6 a)) (DF (DC b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D7 (D3 a)) (DF (D6 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 H0 (DB a) (D6 b) => SHR1 H1 (D5 (DB a)) (DB (D6 b)) 
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D5 (D6 a)) (DB (DC b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D5 (D3 a)) (DB (D6 b)) 
SHR1 H0 (DB a) (D6 b) => SHR1 H1 (D4 (DB a)) (D9 (D6 b)) 
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D4 (D6 a)) (D9 (DC b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D4 (D3 a)) (D9 (D6 b)) 
SHR1 H0 (DB a) (D6 b) => SHR1 H1 (D3 (DB a)) (D7 (D6 b)) 
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D3 (D6 a)) (D7 (DC b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D3 (D3 a)) (D7 (D6 b)) 
SHR1 H0 (DB a) (D6 b) => SHR1 H1 (D2 (DB a)) (D5 (D6 b)) 
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D2 (D6 a)) (D5 (DC b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D2 (D3 a)) (D5 (D6 b)) 
SHR1 H0 (DB a) (D6 b) => SHR1 H1 (D1 (DB a)) (D3 (D6 b)) 
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D1 (D6 a)) (D3 (DC b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D1 (D3 a)) (D3 (D6 b)) 
SHR1 H0 (DB a) (D6 b) => SHR1 H1 (D0 (DB a)) (D1 (D6 b)) 
SHR1 H0 (D6 a) (DC b) => SHR1 H1 (D0 (D6 a)) (D1 (DC b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H1 (D0 (D3 a)) (D1 (D6 b)) 
SHR1 H1 (D6 a) (DD b) => SHR1 H0 (DF (D6 a)) (DE (DD b)) 
SHR1 H1 (D6 a) (DD b) => SHR1 H0 (DE (D6 a)) (DC (DD b)) 
SHR1 H1 (D6 a) (DD b) => SHR1 H0 (DD (D6 a)) (DA (DD b)) 
SHR1 H1 (D6 a) (DD b) => SHR1 H0 (DC (D6 a)) (D8 (DD 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 H1 (D6 a) (DD b) => SHR1 H0 (DA (D6 a)) (D4 (DD b)) 
SHR1 H1 (D6 a) (DD b) => SHR1 H0 (D9 (D6 a)) (D2 (DD b)) 
SHR1 H1 (D6 a) (DD b) => SHR1 H0 (D8 (D6 a)) (D0 (DD b)) 
SHR1 H0 (DB a) (D6 b) => SHR1 H0 (D7 (DB a)) (DE (D6 b)) 
SHR1 H0 (D6 a) (DC b) => SHR1 H0 (D7 (D6 a)) (DE (DC b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D7 (D3 a)) (DE (D6 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 (DB a) (D6 b) => SHR1 H0 (D5 (DB a)) (DA (D6 b)) 
SHR1 H0 (D6 a) (DC b) => SHR1 H0 (D5 (D6 a)) (DA (DC b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D5 (D3 a)) (DA (D6 b)) 
SHR1 H0 (DB a) (D6 b) => SHR1 H0 (D4 (DB a)) (D8 (D6 b)) 
SHR1 H0 (D6 a) (DC b) => SHR1 H0 (D4 (D6 a)) (D8 (DC b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D4 (D3 a)) (D8 (D6 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 (DB a) (D6 b) => SHR1 H0 (D2 (DB a)) (D4 (D6 b)) 
SHR1 H0 (D6 a) (DC b) => SHR1 H0 (D2 (D6 a)) (D4 (DC b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D2 (D3 a)) (D4 (D6 b)) 
SHR1 H0 (DB a) (D6 b) => SHR1 H0 (D1 (DB a)) (D2 (D6 b)) 
SHR1 H0 (D6 a) (DC b) => SHR1 H0 (D1 (D6 a)) (D2 (DC b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D1 (D3 a)) (D2 (D6 b)) 
SHR1 H0 (DB a) (D6 b) => SHR1 H0 (D0 (DB a)) (D0 (D6 b)) 
SHR1 H0 (D6 a) (DC b) => SHR1 H0 (D0 (D6 a)) (D0 (DC b)) 
SHR1 H0 (D3 a) (D6 b) => SHR1 H0 (D0 (D3 a)) (D0 (D6 b)) 
THex (D6 a) => Show (D6 a) 
THex a => THex (D6 a) 
TEven (D6 a) T 
Trichotomy (D6 F) Positive 
Trichotomy (D6 T) Negative 
LSN (D6 F) H6 F 
LSN (D6 T) H6 T 
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 T (D6 a) 
LSN (D6 (D6 a)) H6 (D6 a) 
TNot a b => TNot (D9 a) (D6 b) 
TNot a b => TNot (D6 a) (D9 b) 
TSucc (DE (D6 a)) (DF (D6 a)) 
TSucc (DD (D6 a)) (DE (D6 a)) 
TSucc (DC (D6 a)) (DD (D6 a)) 
TSucc (DB (D6 a)) (DC (D6 a)) 
TSucc (DA (D6 a)) (DB (D6 a)) 
TSucc (D9 (D6 a)) (DA (D6 a)) 
TSucc (D8 (D6 a)) (D9 (D6 a)) 
TSucc (D7 (D6 a)) (D8 (D6 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 (D6 a)) (D5 (D6 a)) 
TSucc (D3 (D6 a)) (D4 (D6 a)) 
TSucc (D2 (D6 a)) (D3 (D6 a)) 
TSucc (D1 (D6 a)) (D2 (D6 a)) 
TSucc (D0 (D6 a)) (D1 (D6 a)) 
THex2Binary' a b => THex2Binary' (D6 a) (O (I (I (O b)))) 
TNF' (D6 a) c b => TNF' (DF (D6 a)) (DF c) b 
TNF' (D6 a) c b => TNF' (DE (D6 a)) (DE c) b 
TNF' (D6 a) c b => TNF' (DD (D6 a)) (DD c) b 
TNF' (D6 a) c b => TNF' (DC (D6 a)) (DC c) b 
TNF' (D6 a) c b => TNF' (DB (D6 a)) (DB c) b 
TNF' (D6 a) c b => TNF' (DA (D6 a)) (DA c) b 
TNF' (D6 a) c b => TNF' (D9 (D6 a)) (D9 c) b 
TNF' (D6 a) c b => TNF' (D8 (D6 a)) (D8 c) b 
TNF' (D6 a) c b => TNF' (D7 (D6 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' (D6 a) c b => TNF' (D5 (D6 a)) (D5 c) b 
TNF' (D6 a) c b => TNF' (D4 (D6 a)) (D4 c) b 
TNF' (D6 a) c b => TNF' (D3 (D6 a)) (D3 c) b 
TNF' (D6 a) c b => TNF' (D2 (D6 a)) (D2 c) b 
TNF' (D6 a) c b => TNF' (D1 (D6 a)) (D1 c) b 
TNF' (D6 a) c b => TNF' (D0 (D6 a)) (D0 c) b 
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' (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) (D6 b) T (D5 c) 
TAddC' a b T c => TAddC' (DE a) (D6 b) F (D4 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) (D6 b) T (D4 c) 
TAddC' a b T c => TAddC' (DD a) (D6 b) F (D3 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) (D6 b) T (D3 c) 
TAddC' a b T c => TAddC' (DC a) (D6 b) F (D2 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) (D6 b) T (D2 c) 
TAddC' a b T c => TAddC' (DB a) (D6 b) F (D1 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) (D6 b) T (D1 c) 
TAddC' a b T c => TAddC' (DA a) (D6 b) F (D0 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) (D6 b) T (D0 c) 
TAddC' a b F c => TAddC' (D9 a) (D6 b) F (DF 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 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 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 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 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 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) (D1 b) F (D6 c) 
TAddC' a b F c => TAddC' (D5 a) (D0 b) T (D6 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) (D2 b) F (D6 c) 
TAddC' a b F c => TAddC' (D4 a) (D1 b) T (D6 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) (D3 b) F (D6 c) 
TAddC' a b F c => TAddC' (D3 a) (D2 b) T (D6 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) (D4 b) F (D6 c) 
TAddC' a b F c => TAddC' (D2 a) (D3 b) T (D6 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) F (D6 c) 
TAddC' a b F c => TAddC' (D1 a) (D4 b) T (D6 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) 

data D7 a Source

Instances

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, TAdd' a2 a4 a6, TAdd' a1 a6 a7, TAdd' a7 c d) => TMul a1 (D7 b) d 
TAddC' F (D7 a) F (D7 a) 
TAddC' F (D7 a) T (D8 a) 
TAddC' F (D6 a) T (D7 a) 
TAddC' T (D8 a) F (D7 a) 
TAddC' T (D7 a) T (D7 a) 
TAddC' T (D7 a) F (D6 a) 
SHR1 H1 (DB a) (D7 b) => SHR1 H1 (DF (DB a)) (DF (D7 b)) 
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (DF (D7 a)) (DF (DF b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DF (D3 a)) (DF (D7 b)) 
SHR1 H1 (DB a) (D7 b) => SHR1 H1 (DE (DB a)) (DD (D7 b)) 
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (DE (D7 a)) (DD (DF b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DE (D3 a)) (DD (D7 b)) 
SHR1 H1 (DB a) (D7 b) => SHR1 H1 (DD (DB a)) (DB (D7 b)) 
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (DD (D7 a)) (DB (DF b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DD (D3 a)) (DB (D7 b)) 
SHR1 H1 (DB a) (D7 b) => SHR1 H1 (DC (DB a)) (D9 (D7 b)) 
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (DC (D7 a)) (D9 (DF b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DC (D3 a)) (D9 (D7 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 (DB a) (D7 b) => SHR1 H1 (DA (DB a)) (D5 (D7 b)) 
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (DA (D7 a)) (D5 (DF b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (DA (D3 a)) (D5 (D7 b)) 
SHR1 H1 (DB a) (D7 b) => SHR1 H1 (D9 (DB a)) (D3 (D7 b)) 
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (D9 (D7 a)) (D3 (DF b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (D9 (D3 a)) (D3 (D7 b)) 
SHR1 H1 (DB a) (D7 b) => SHR1 H1 (D8 (DB a)) (D1 (D7 b)) 
SHR1 H1 (D7 a) (DF b) => SHR1 H1 (D8 (D7 a)) (D1 (DF b)) 
SHR1 H1 (D3 a) (D7 b) => SHR1 H1 (D8 (D3 a)) (D1 (D7 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 (