fact: Fixpoint double d := match d with | Nil => Nil | D0 d => D0 (double d) | D1 d => D2 (double d) | D2 d => D4 (double d) | D3 d => D6 (double d) | D4 d => D8 (double d) | D5 d => D0 (succ_double d) | D6 d => D2 (succ_double d) | D7 d => D4 (succ_double d) | D8 d => D6 (succ_double d) | D9 d => D8 (succ_double d) end with succ_double d := match d with | Nil => D1 Nil | D0 d => D1 (double d) | D1 d => D3 (double d) | D2 d => D5 (double d) | D3 d => D7 (double d) | D4 d => D9 (double d) | D5 d => D1 (succ_double d) | D6 d => D3 (succ_double d) | D7 d => D5 (succ_double d) | D8 d => D7 (succ_double d) | D9 d => D9 (succ_double d) end.
imports: Datatypes Specif