equal
deleted
inserted
replaced
21 vertl "{(i, j), (Suc i, j)} : domino" |
21 vertl "{(i, j), (Suc i, j)} : domino" |
22 |
22 |
23 inductive "tiling A" |
23 inductive "tiling A" |
24 intrs |
24 intrs |
25 empty "{} : tiling A" |
25 empty "{} : tiling A" |
26 Un "[| a: A; t: tiling A; a Int t = {} |] ==> a Un t : tiling A" |
26 Un "[| a: A; t: tiling A; a <= Compl t |] ==> a Un t : tiling A" |
27 |
27 |
28 defs |
28 defs |
29 below_def "below n == nat_rec {} insert n" |
29 below_def "below n == nat_rec {} insert n" |
30 evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}" |
30 evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}" |
31 |
31 |