1\DOC 2 3\TYPE {FCP_ss : ssfrag} 4 5\SYNOPSIS 6 7A simpset fragment for simplifying finite Cartesian product expressions. 8 9\KEYWORDS 10 11simplification, finite Cartesian products. 12 13\EXAMPLE 14 15{ 16 simpLib.SSFRAG{ac = [], congs = [], convs = [], dprocs = [], filter = NONE, 17 rewrs = 18 [|- !i. i < dimindex (:'b) ==> ($FCP g ' i = g i), 19 |- !g. (FCP i. g ' i) = g, 20 |- !x y. (x = y) = !i. i < dimindex (:'b) ==> (x ' i = y ' i)]} 21 : ssfrag 22} 23 24\SEEALSO 25 26wordsLib.WORD_BIT_EQ_ss 27 28\ENDDOC 29