16 inductive |
16 inductive |
17 domains "domino" <= "Pow(nat*nat)" |
17 domains "domino" <= "Pow(nat*nat)" |
18 intrs |
18 intrs |
19 horiz "[| i: nat; j: nat |] ==> {<i,j>, <i,succ(j)>} : domino" |
19 horiz "[| i: nat; j: nat |] ==> {<i,j>, <i,succ(j)>} : domino" |
20 vertl "[| i: nat; j: nat |] ==> {<i,j>, <succ(i),j>} : domino" |
20 vertl "[| i: nat; j: nat |] ==> {<i,j>, <succ(i),j>} : domino" |
21 type_intrs "[empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI]" |
21 type_intrs empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI |
22 |
22 |
23 |
23 |
24 inductive |
24 inductive |
25 domains "tiling(A)" <= "Pow(Union(A))" |
25 domains "tiling(A)" <= "Pow(Union(A))" |
26 intrs |
26 intrs |
27 empty "0 : tiling(A)" |
27 empty "0 : tiling(A)" |
28 Un "[| a: A; t: tiling(A); a Int t = 0 |] ==> a Un t : tiling(A)" |
28 Un "[| a: A; t: tiling(A); a Int t = 0 |] ==> a Un t : tiling(A)" |
29 type_intrs "[empty_subsetI, Union_upper, Un_least, PowI]" |
29 type_intrs empty_subsetI, Union_upper, Un_least, PowI |
30 type_elims "[make_elim PowD]" |
30 type_elims "[make_elim PowD]" |
31 |
31 |
32 constdefs |
32 constdefs |
33 evnodd :: [i,i]=>i |
33 evnodd :: [i,i]=>i |
34 "evnodd(A,b) == {z:A. EX i j. z=<i,j> & (i#+j) mod 2 = b}" |
34 "evnodd(A,b) == {z:A. EX i j. z=<i,j> & (i#+j) mod 2 = b}" |