why3 projects: combinatorial and sequential logic elements (from nand2tetris), some redefined theories (set, map), seplog theories