| Portability | non-portable (MPTC, FD, TH, undecidable instances, missing constructors) |
|---|---|
| Stability | experimental |
| Maintainer | Edward Kmett <ekmett@gmail.com> |
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
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) |
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) |
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) |
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) |
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) |
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) |
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) |
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 (D7 (D9 a)) (DF (D2 b)) | |
| SHR1 H0 (D8 a) (D0 b) => SHR1 H1 (D7 (D8 a)) (DF (D0 |