Menu
▾
▴
Re: [CZT-Devel] Issues Building CZT in Windows
|
From: Jon L. <ja...@bu...> - 2012-07-18 19:59:59
|
-------------------------------------------------------------------------------
Test set: net.sourceforge.czt.specreader.PermuteMarkupTest
-------------------------------------------------------------------------------
Tests run: 1, Failures: 1, Errors: 0, Skipped: 0, Time elapsed: 0.094 sec <<< FAILURE!
testPermuteMarkup(net.sourceforge.czt.specreader.PermuteMarkupTest) Time elapsed: 0.031 sec <<< FAILURE!
junit.framework.ComparisonFailure: null expected:<...ile /lib/prelude.tex[
%%Zloc 18#1@470
\begin{zsection}
\SECTION prelude
\end{zsection}
%%Zloc 26#1@639
%%Zchar \{ U+007B
%%Zloc 27#1@657
%%Zchar \} U+007D
%%Zloc 28#1@675
%%Zinchar \where U+007C
%%Zloc 29#1@699
%%Zchar \Delta U+0394
%%Zloc 30#1@721
%%Zchar \Xi U+039E
%%Zloc 31#1@740
%%Zprechar \theta U+03B8
%%Zloc 32#1@765
%%Zprechar \lambda U+03BB
%%Zloc 33#1@791
%%Zprechar \mu U+03BC
%%Zloc 34#1@813
%%Zchar \ldata U+27EA
%%Zloc 35#1@835
%%Zchar \rdata U+27EB
%%Zloc 36#1@857
%%Zchar \lblot U+2989
%%Zloc 37#1@879
%%Zchar \rblot U+298A
%%Zloc 38#1@901
%%Zchar \vdash U+22A2
%%Zloc 39#1@923
%%Zinchar \land U+2227
%%Zloc 40#1@946
%%Zinchar \lor U+2228
%%Zloc 41#1@968
%%Zinchar \implies U+21D2
%%Zloc 42#1@994
%%Zinchar \iff U+21D4
%%Zloc 43#1@1016
%%Zprechar \lnot U+00AC
%%Zloc 44#1@1040
%%Zprechar \forall U+2200
%%Zloc 45#1@1066
%%Zprechar \exists U+2203
%%Zloc 46#1@1092
%%Zinchar \in U+2208
%%Zloc 47#1@1113
%%Zinchar \spot U+2981
%%Zloc 48#1@1136
%%Zinchar \hide U+29F9
%%Zloc 49#1@1159
%%Zinchar \project U+2A21
%%Zloc 50#1@1185
%%Zinchar \semi U+2A1F
%%Zloc 51#1@1208
%%Zinchar \pipe U+2A20
%%Zloc 52#1@1231
%%Zpreword \IF if
%%Zloc 53#1@1249
%%Zinword \THEN then
%%Zloc 54#1@1270
%%Zinword \ELSE else
%%Zloc 55#1@1291
%%Zpreword \LET let
%%Zloc 56#1@1311
%%Zpreword \pre pre
%%Zloc 57#1@1331
%%Zinword \function function
%%Zloc 58#1@1360
%%Zinword \generic generic
%%Zloc 59#1@1387
%%Zinword \relation relation
%%Zloc 60#1@1416
%%Zinword \leftassoc leftassoc
%%Zloc 61#1@1447
%%Zinword \rightassoc rightassoc
%%Zloc 62#1@1480
%%Zinword \listarg {,}{,}
%%Zloc 63#1@1506
%%Zinword \varg \_
%%Zloc 64#1@1525
%%Zprechar \power U+2119
%%Zloc 65#1@1550
%%Zinchar \cross U+00D7
%%Zloc 66#1@1574
%%Zchar \arithmos U-0001D538
%%Zloc 67#1@1603
%%Zchar \nat U+2115
%%Zloc 71#1@1699
%%Zchar \alpha U+03B1
%%Zloc 72#1@1721
%%Zchar \beta U+03B2
%%Zloc 73#1@1742
%%Zchar \gamma U+03B3
%%Zloc 74#1@1764
%%Zchar \delta U+03B4
%%Zloc 75#1@1786
%%Zchar \epsilon U+03B5
%%Zloc 76#1@1810
%%Zchar \zeta U+03B6
%%Zloc 77#1@1831
%%Zchar \eta U+03B7
%%Zloc 78#1@1851
%%Zchar \iota U+03B9
%%Zloc 79#1@1872
%%Zchar \kappa U+03BA
%%Zloc 80#1@1894
%%Zchar \nu U+03BD
%%Zloc 81#1@1913
%%Zchar \xi U+03BE
%%Zloc 82#1@1932
%%Zchar \pi U+03C0
%%Zloc 83#1@1951
%%Zchar \rho U+03C1
%%Zloc 84#1@1971
%%Zchar \sigma U+03C3
%%Zloc 85#1@1993
%%Zchar \tau U+03C4
%%Zloc 86#1@2013
%%Zchar \upsilon U+03C5
%%Zloc 87#1@2037
%%Zchar \phi U+03C6
%%Zloc 88#1@2057
%%Zchar \chi U+03C7
%%Zloc 89#1@2077
%%Zchar \psi U+03C8
%%Zloc 90#1@2097
%%Zchar \omega U+03C9
%%Zloc 91#1@2119
%%Zchar \Gamma U+0393
%%Zloc 92#1@2141
%%Zchar \Theta U+0398
%%Zloc 93#1@2163
%%Zchar \Lambda U+039B
%%Zloc 94#1@2186
%%Zchar \Pi U+03A0
%%Zloc 95#1@2205
%%Zchar \Sigma U+03A3
%%Zloc 96#1@2227
%%Zchar \Upsilon U+03A5
%%Zloc 97#1@2251
%%Zchar \Phi U+03A6
%%Zloc 98#1@2271
%%Zchar \Psi U+03A8
%%Zloc 99#1@2291
%%Zchar \Omega U+03A9
%%Zloc 102#1@2321
\begin{zed}
\generic (\power \_)
\end{zed}
%%Zloc 119#1@2903
\begin{zed}
[\arithmos]
\end{zed}
%%Zloc 126#1@3058
\begin{axdef}
\nat : \power \arithmos
\end{axdef}
%%Zloc 139#1@3337
\begin{axdef}
number\_literal\_0 : \nat\\
number\_literal\_1 : \nat
\end{axdef}
%%Zloc 147#1@3542
\begin{zed}
\function 30 \leftassoc (\_ + \_)
\end{zed}
%%Zloc 151#1@3599
\begin{axdef}
\_ + \_ : \power ((\arithmos \cross \arithmos) \cross \arithmos)
\where
\forall m, n: \nat @ \exists_1 p: ( \_ + \_ ) @ p.1 = (m, n)\\
\forall m, n: \nat @ m + n \in \nat\\
\forall m, n: \nat | m + 1 = n + 1 @ m = n\\
\forall n: \nat @ \lnot n + 1 = 0\\
\forall w: \power \nat | 0 \in w \land (\forall y: w @ y + 1 \in w) @ w = \nat\\
\forall m: \nat @ m + 0 = m\\
\forall m, n: \nat @ m + (n + 1) = (m + n) + 1
\end{axdef}
%%Zfile /lib/set_toolkit.tex
%%Zloc 8#1@179
\begin{zsection}
\SECTION set\_toolkit
\end{zsection}
%%Zloc 14#1@256
%%Zinchar \rel U+2194
%%Zloc 29#1@609
%%Zinchar \fun U+2192
%%Zloc 46#1@1025
%%Zinchar \neq U+2260
%%Zloc 62#1@1327
%%Zinchar \notin U+2209
%%Zloc 79#1@1697
%%Zchar \emptyset U+2205
%%Zloc 89#1@1886
%%Zinchar \subseteq U+2286
%%Zloc 106#1@2275
%%Zinchar \subset U+2282
%%Zloc 137#1@2951
%%Zinchar \cup U+222A
%%Zloc 153#1@3321
%%Zinchar \cap U+2229
%%Zloc 169#1@3696
%%Zinchar \setminus U+2216
%%Zloc 185#1@4140
%%Zinchar \symdiff U+2296
%%Zloc 202#1@4591
%%Zprechar \bigcup U+22C3
%%Zloc 214#1@4953
%%Zprechar \bigcap U+22C2
%%Zloc 229#1@5341
%%Zprechar \finset U-0001D53D
%%Zloc 15#1@278
\begin{zed}
\generic 5 \rightassoc (\_ \rel \_)
\end{zed}
%%Zloc 19#1@337
\begin{zed}
X \rel Y == \power ( X \cross Y )
\end{zed}
%%Zloc 30#1@631
\begin{zed}
\generic 5 \rightassoc (\_ \fun \_)
\end{zed}
%%Zloc 34#1@690
\begin{zed}
X \fun Y == \{~ f : X \rel Y | \forall x : X @ \exists_1 y : Y @ (x , y) \in f ~\}
\end{zed}
%%Zloc 47#1@1047
\begin{zed}
\relation (\_ \neq \_)
\end{zed}
%%Zloc 51#1@1093
\begin{gendef}[X]
\_ \neq \_ : X \rel X
\where
\forall x , y : X @ x \neq y \iff \lnot x = y
\end{gendef}
%%Zloc 63#1@1351
\begin{zed}
\relation (\_ \notin \_)
\end{zed}
%%Zloc 67#1@1399
\begin{gendef}[X]
\_ \notin \_ : X \rel \power X
\where
\forall x : X ; a : \power X @ x \notin a \iff \lnot x \in a
\end{gendef}
%%Zloc 80#1@1722
\begin{zed}
\emptyset [ X ] == \{~ x : X | false ~\}
\end{zed}
%%Zloc 90#1@1913
\begin{zed}
\relation (\_ \subseteq \_)
\end{zed}
%%Zloc 94#1@1964
\begin{gendef}[X]
\_ \subseteq \_ : \power X \rel \power X
\where
\forall a , b : \power X @ a \subseteq b \iff
( \forall x : a @ x \in b )
\end{gendef}
%%Zloc 107#1@2300
\begin{zed}
\relation (\_ \subset \_)
\end{zed}
%%Zloc 111#1@2349
\begin{gendef}[X]
\_ \subset \_ : \power X \rel \power X
\where
\forall a , b : \power X @ a \subset b \iff
a \subseteq b \land a \neq b
\end{gendef}
%%Zloc 125#1@2674
\begin{zed}
\power_1 X == \{~ a : \power X | a \neq \emptyset ~\}
\end{zed}
%%Zloc 138#1@2973
\begin{zed}
\function 30 \leftassoc (\_ \cup \_)
\end{zed}
%%Zloc 142#1@3033
\begin{gendef}[X]
\_ \cup \_ : \power X \cross \power X \fun \power X
\where
\forall a , b : \power X @ a \cup b = \{~ x : X | x \in a \lor x \in b ~\}
\end{gendef}
%%Zloc 154#1@3343
\begin{zed}
\function 40 \leftassoc (\_ \cap \_)
\end{zed}
%%Zloc 158#1@3403
\begin{gendef}[X]
\_ \cap \_ : \power X \cross \power X \fun \power X
\where
\forall a , b : \power X @ a \cap b = \{~ x : X | x \in a \land x \in b ~\}
\end{gendef}
%%Zloc 170#1@3723
\begin{zed}
\function 30 \leftassoc (\_ \setminus \_)
\end{zed}
%%Zloc 174#1@3788
\begin{gendef}[X]
\_ \setminus \_ : \power X \cross \power X \fun \power X
\where
\forall a , b : \power X @ a \setminus b = \{~ x : X | x \in a \land x \notin b ~\}
\end{gendef}
%%Zloc 186#1@4166
\begin{zed}
\function 25 \leftassoc (\_ \symdiff \_)
\end{zed}
%%Zloc 190#1@4230
\begin{gendef}[X]
\_ \symdiff \_ : \power X \cross \power X \fun \power X
\where
\forall a , b : \power X @ a \symdiff b = \{~ x : X | \lnot ( x \in a \iff x \in b) ~\}
\end{gendef}
%%Zloc 203#1@4617
\begin{gendef}[X]
\bigcup : \power \power X \fun \power X
\where
\forall A : \power \power X @ \bigcup A = \{~ x : X | \exists a : A @ x \in a ~\}
\end{gendef}
%%Zloc 215#1@4979
\begin{gendef}[X]
\bigcap : \power \power X \fun \power X
\where
\forall A : \power \power X @ \bigcap A = \{~ x : X | \forall a : A @ x \in a ~\}
\end{gendef}
%%Zloc 230#1@5371
\begin{zed}
\generic (\finset \_)
\end{zed}
%%Zloc 234#1@5416
\begin{zed}
\finset X == \bigcap \{~ A : \power \power X |
\emptyset \in A \land ( \forall a : A ; x : X @ a \cup \{ x \} \in A ) ~\}
\end{zed}
%%Zloc 246#1@5821
\begin{zed}
\finset_1 X == \finset X \setminus \{ \emptyset \}
\end{zed}
%%Zfile /lib/number_toolkit.tex
%%Zloc 7#1@135
\begin{zsection}
\SECTION number\_toolkit
\end{zsection}
%%Zloc 27#1@442
%%Zchar \num U+2124
%%Zloc 43#1@900
%%Zprechar \negate U+002D
%%Zloc 132#1@3340
%%Zinchar \leq U+2264
%%Zloc 163#1@3943
%%Zinchar \geq U+2265
%%Zloc 256#1@6127
%%Zinword \div div
%%Zloc 257#1@6146
%%Zinword \mod mod
%%Zloc 13#1@215
\begin{zed}
\function (succ~\_)
\end{zed}
%%Zloc 17#1@258
\begin{axdef}
succ~\_ : \power (\nat \cross \nat)
\where
(succ~\_) = \lambda n : \nat @ n+1
\end{axdef}
%%Zloc 28#1@462
\begin{axdef}
\num : \power \arithmos
\end{axdef}
%%Zloc 44#1@926
\begin{zed}
\function (\negate \_)
\end{zed}
%%Zloc 48#1@972
\begin{axdef}
\negate \_ : \power (\arithmos \cross \arithmos)
\where
\forall x, y : \num @ \exists_1 z : \num @ ((x,y),z) \in (\_ + \_)\\
\forall x : \num @ \exists_1 y : \num @ (x,y) \in (\negate \_)
\also
\forall i , j , k : \num @
\\ \t1 ( i + j ) + k = i + ( j + k )
\\ \t1 \land i + j = j + i
\\ \t1 \land i + \negate i = 0
\\ \t1 \land i + 0 = i
\also
\num = \{ z : \arithmos | \exists x : \nat @ z = x \lor z = \negate x \}
\end{axdef}
%%Zloc 99#1@2510
\begin{zed}
\function 30 \leftassoc (\_ - \_)
\end{zed}
%%Zloc 103#1@2567
\begin{axdef}
\_ - \_ : \power ((\arithmos \cross \arithmos) \cross \arithmos)
\where
\forall x, y : \num @ \exists_1 z : \num @ ((x,y),z) \in (\_ - \_)
\also
\forall i , j : \num @ i - j = i + \negate j
\end{axdef}
%%Zloc 133#1@3362
\begin{zed}
\relation (\_ \leq \_)
\end{zed}
%%Zloc 137#1@3408
\begin{axdef}
\_ \leq \_ : \power (\arithmos \cross \arithmos)
\where
\forall i , j : \num @ i \leq j \iff j - i \in \nat
\end{axdef}
%%Zloc 148#1@3669
\begin{zed}
\relation (\_ < \_)
\end{zed}
%%Zloc 152#1@3712
\begin{axdef}
\_ < \_ : \power (\arithmos \cross \arithmos)
\where
\forall i , j : \num @ i < j \iff i + 1 \leq j
\end{axdef}
%%Zloc 164#1@3965
\begin{zed}
\relation (\_ \geq \_)
\end{zed}
%%Zloc 168#1@4011
\begin{axdef}
\_ \geq \_ : \power (\arithmos \cross \arithmos)
\where
\forall i , j : \num @ i \geq j \iff j \leq i
\end{axdef}
%%Zloc 179#1@4234
\begin{zed}
\relation (\_ > \_)
\end{zed}
%%Zloc 183#1@4277
\begin{axdef}
\_ > \_ : \power (\arithmos \cross \arithmos)
\where
\forall i , j : \num @ i > j \iff j < i
\end{axdef}
%%Zloc 194#1@4506
\begin{zed}
\nat_1 == \{ x : \nat | \lnot x = 0 \}
\end{zed}
%%Zloc 203#1@4684
\begin{zed}
\num_1 == \{ x : \num | \lnot x = 0 \}
\end{zed}
%%Zloc 211#1@4848
\begin{zed}
\function 40 \leftassoc (\_ * \_)
\end{zed}
%%Zloc 215#1@4905
\begin{axdef}
\_ * \_ : \power ((\arithmos \cross \arithmos) \cross \arithmos)
\where
\forall x, y : \num @ \exists_1 z : \num @ ((x,y),z) \in (\_ * \_)
\also
\forall i , j , k : \num @
\\ \t1 ( i * j ) * k = i * ( j * k )
\\ \t1 \land i * j = j * i
\\ \t1 \land i * ( j + k ) = i * j + i * k
\\ \t1 \land 0 * i = 0
\\ \t1 \land 1 * i = i
\end{axdef}
%%Zloc 258#1@6165
\begin{zed}
\function 40 \leftassoc (\_ \div \_)\\
\function 40 \leftassoc (\_ \mod \_)
\end{zed}
%%Zloc 263#1@6264
\begin{axdef}
\_ \div \_~, \_ \mod \_ : \power ((\arithmos \cross \arithmos) \cross \arithmos)
\where
\forall x : \num ; y : \num_1 @ \exists_1 z : \num @ ((x,y),z) \in (\_ \div \_)
\also
\forall x : \num ; y : \num_1 @ \exists_1 z : \num @ ((x,y),z) \in (\_ \mod \_)
\also
\forall i : \num ; j : \num_1 @
\\ \t1 i = ( i \div j ) * j + i \mod j
\\ \t1 \land ( 0 \leq i \mod j < j \lor j < i \mod j \leq 0 )
\end{axdef}
%%Zfile /lib/relation_toolkit.tex
%%Zloc 7#1@156
\begin{zsection}
\SECTION relation\_toolkit \parents set\_toolkit
\end{zsection}
%%Zloc 35#1@710
%%Zinchar \mapsto U+21A6
%%Zloc 51#1@1053
%%Zpreword \dom dom
%%Zloc 63#1@1306
%%Zpreword \ran ran
%%Zloc 75#1@1571
%%Zpreword \id id
%%Zloc 89#1@1821
%%Zinchar \comp U+2A3E
%%Zloc 109#1@2460
%%Zinchar \circ U+2218
%%Zloc 125#1@2838
%%Zinchar \dres U+25C1
%%Zloc 141#1@3270
%%Zinchar \rres U+25B7
%%Zloc 157#1@3701
%%Zinchar \ndres U+2A64
%%Zloc 174#1@4144
%%Zinchar \nrres U+2A65
%%Zloc 191#1@4588
%%Zpostchar \inv U+223C
%%Zloc 207#1@4931
%%Zinchar \limg U+2987
%%Zloc 208#1@4954
%%Zpostchar \rimg U+2988
%%Zloc 224#1@5406
%%Zinchar \oplus U+2295
%%Zloc 242#1@5902
%%Zpostword \plus ^+
%%Zloc 260#1@6351
%%Zpostword \star ^*
%%Zloc 13#1@277
\begin{gendef}[X,Y]
first : X \cross Y \fun X
\where
\forall x : X; y : Y @ first~(x,y) = x
\end{gendef}
%%Zloc 24#1@503
\begin{gendef}[X,Y]
second : X \cross Y \fun Y
\where
\forall x : X; y : Y @ second~(x,y) = y
\end{gendef}
%%Zloc 36#1@735
\begin{zed}
\function 10 \leftassoc (\_ \mapsto \_)
\end{zed}
%%Zloc 40#1@798
\begin{gendef}[X,Y]
\_ \mapsto \_ : X \cross Y \fun X \cross Y
\where
\forall x : X ; y : Y @ x \mapsto y = ( x , y )
\end{gendef}
%%Zloc 52#1@1073
\begin{gendef}[X,Y]
\dom : (X \rel Y) \fun \power X
\where
\forall r : X \rel Y @ \dom r = \{~ p : r @ p.1 ~\}
\end{gendef}
%%Zloc 64#1@1326
\begin{gendef}[X,Y]
\ran : (X \rel Y) \fun \power Y
\where
\forall r : X \rel Y @ \ran r = \{~ p : r @ p.2 ~\}
\end{gendef}
%%Zloc 76#1@1589
\begin{zed}
\generic (\id \_)
\end{zed}
%%Zloc 80#1@1630
\begin{zed}
\id X == \{~ x : X @ x \mapsto x ~\}
\end{zed}
%%Zloc 90#1@1844
\begin{zed}
\function 40 \leftassoc (\_ \comp \_)
\end{zed}
%%Zloc 94#1@1905
\begin{gendef}[X,Y,Z]
\_ \comp \_ : (X \rel Y) \cross (Y \rel Z) \fun (X \rel Z)
\where
\forall r : X \rel Y ; s : Y \rel Z @
r \comp s = \{~ p : r ; q : s | p.2 = q.1 @ p.1 \mapsto q.2 ~\}
\end{gendef}
%%Zloc 110#1@2483
\begin{zed}
\function 40 \leftassoc (\_ \circ \_)
\end{zed}
%%Zloc 114#1@2544
\begin{gendef}[X,Y,Z]
\_ \circ \_ : (Y \rel Z) \cross (X \rel Y) \fun (X \rel Z)
\where
\forall r : X \rel Y ; s : Y \rel Z @ s \circ r = r \comp s
\end{gendef}
%%Zloc 126#1@2861
\begin{zed}
\function 65 \rightassoc (\_ \dres \_)
\end{zed}
%%Zloc 130#1@2923
\begin{gendef}[X,Y]
\_ \dres \_ : \power X \cross ( X \rel Y ) \fun ( X \rel Y )
\where
\forall a : \power X ; r : X \rel Y @ a \dres r = \{~ p : r | p.1 \in a ~\}
\end{gendef}
%%Zloc 142#1@3293
\begin{zed}
\function 60 \leftassoc (\_ \rres \_)
\end{zed}
%%Zloc 146#1@3354
\begin{gendef}[X,Y]
\_ \rres \_ : ( X \rel Y) \cross \power Y \fun ( X \rel Y )
\where
\forall r : X \rel Y ; b : \power Y @ r \rres b = \{~ p : r | p.2 \in b ~\}
\end{gendef}
%%Zloc 158#1@3725
\begin{zed}
\function 65 \rightassoc (\_ \ndres \_)
\end{zed}
%%Zloc 162#1@3788
\begin{gendef}[X,Y]
\_ \ndres \_ : \power X \cross ( X \rel Y ) \fun ( X \rel Y )
\where
\forall a : \power X ; r : X \rel Y @ a \ndres r = \{~ p : r | p.1 \notin a ~\}
\end{gendef}
%%Zloc 175#1@4168
\begin{zed}
\function 60 \leftassoc (\_ \nrres \_)
\end{zed}
%%Zloc 179#1@4230
\begin{gendef}[X,Y]
\_ \nrres \_ : ( X \rel Y) \cross \power Y \fun ( X \rel Y )
\where
\forall r : X \rel Y ; b : \power Y @
r \nrres b = \{~ p : r | p.2 \notin b ~\}
\end{gendef}
%%Zloc 192#1@4612
\begin{zed}
\function (\_ \inv)
\end{zed}
%%Zloc 196#1@4655
\begin{gendef}[X,Y]
\_ \inv : ( X \rel Y ) \fun ( Y \rel X )
\where
\forall r : X \rel Y @ r \inv = \{~ p : r @ p.2 \mapsto p.1 ~\}
\end{gendef}
%%Zloc 209#1@4979
\begin{zed}
\function (\_ \limg \_ \rimg)
\end{zed}
%%Zloc 213#1@5032
\begin{gendef}[X,Y]
\_ \limg \_ \rimg : ( X \rel Y ) \cross \power X \fun \power Y
\where
\forall r : X \rel Y ; a : \power X @ r \limg a \rimg = \{~ p : r | p.1 \in a @ p.2 ~\}
\end{gendef}
%%Zloc 225#1@5430
\begin{zed}
\function 50 \leftassoc (\_ \oplus \_)
\end{zed}
%%Zloc 229#1@5492
\begin{gendef}[X,Y]
\_ \oplus \_ : ( X \rel Y ) \cross ( X \rel Y ) \fun ( X \rel Y )
\where
\forall r , s : X \rel Y @ r \oplus s = ( ( \dom s ) \ndres r ) \cup s
\end{gendef}
%%Zloc 243#1@5923
\begin{zed}
\function (\_ \plus)
\end{zed}
%%Zloc 247#1@5967
\begin{gendef}[X]
\_ \plus : ( X \rel X ) \fun (X \rel X )
\where
\forall r : X \rel X @
r \plus = \bigcap \{~ s : X \rel X | r \subseteq s \land r \comp s \subseteq s ~\}
\end{gendef}
%%Zloc 261#1@6372
\begin{zed}
\function (\_ \star)
\end{zed}
%%Zloc 265#1@6416
\begin{gendef}[X]
\_ \star : ( X \rel X ) \fun (X \rel X )
\where
\forall r : X \rel X @ r \star = r \plus \cup \id X
\end{gendef}
%%Zfile /lib/function_toolkit.tex
%%Zloc 7#1@137
\begin{zsection}
\SECTION function\_toolkit \parents relation\_toolkit
\end{zsection}
%%Zloc 13#1@254
%%Zinchar \pfun U+21F8
%%Zloc 29#1@717
%%Zinchar \pinj U+2914
%%Zloc 46#1@1247
%%Zinchar \inj U+21A3
%%Zloc 61#1@1581
%%Zinchar \psurj U+2900
%%Zloc 77#1@1976
%%Zinchar \surj U+21A0
%%Zloc 92#1@2307
%%Zinchar \bij U+2916
%%Zloc 107#1@2640
%%Zinchar \ffun U+21FB
%%Zloc 121#1@2926
%%Zinchar \finj U+2915
%%Zloc 135#1@3225
%%Zpreword \disjoint disjoint
%%Zloc 152#1@3627
%%Zinword \partition partition
%%Zloc 14#1@277
\begin{zed}
\generic 5 \rightassoc (\_ \pfun \_)
\end{zed}
%%Zloc 18#1@337
\begin{zed}
X \pfun Y == \{~ f : X \rel Y | \forall p , q : f | p.1 = q.1 @ p.2 = q.2 ~\}
\end{zed}
%%Zloc 30#1@740
\begin{zed}
\generic 5 \rightassoc (\_ \pinj \_)
\end{zed}
%%Zloc 34#1@800
\begin{zed}
X \pinj Y == \{~ f : X \rel Y | \forall p, q : f @ p.1 = q.1 \iff p.2 = q.2 ~\}
\end{zed}
%%Zloc 47#1@1269
\begin{zed}
\generic 5 \rightassoc (\_ \inj \_)
\end{zed}
%%Zloc 51#1@1328
\begin{zed}
X \inj Y == ( X \pinj Y ) \cap ( X \fun Y )
\end{zed}
%%Zloc 62#1@1605
\begin{zed}
\generic 5 \rightassoc (\_ \psurj \_)
\end{zed}
%%Zloc 66#1@1666
\begin{zed}
X \psurj Y == \{~ f : X \pfun Y | \ran f = Y ~\}
\end{zed}
%%Zloc 78#1@1999
\begin{zed}
\generic 5 \rightassoc (\_ \surj \_)
\end{zed}
%%Zloc 82#1@2059
\begin{zed}
X \surj Y == ( X \psurj Y) \cap ( X \fun Y )
\end{zed}
%%Zloc 93#1@2329
\begin{zed}
\generic 5 \rightassoc (\_ \bij \_)
\end{zed}
%%Zloc 97#1@2388
\begin{zed}
X \bij Y == ( X \surj Y ) \cap ( X \inj Y )
\end{zed}
%%Zloc 108#1@2663
\begin{zed}
\generic 5 \rightassoc (\_ \ffun \_)
\end{zed}
%%Zloc 112#1@2723
\begin{zed}
X \ffun Y == (X \pfun Y) \cap \finset (X \cross Y)
\end{zed}
%%Zloc 122#1@2949
\begin{zed}
\generic 5 \rightassoc (\_ \finj \_)
\end{zed}
%%Zloc 126#1@3009
\begin{zed}
X \finj Y == ( X \ffun Y ) \cap ( X \pinj Y )
\end{zed}
%%Zloc 136#1@3255
\begin{zed}
\relation (\disjoint \_)
\end{zed}
%%Zloc 140#1@3303
\begin{gendef}[L,X]
\disjoint \_ : \power ( L \rel \power X )
\where
\forall f : L \rel \power X @
\disjoint f \iff ( \forall p , q : f | p \neq q @ p.2 \cap q.2 = \emptyset )
\end{gendef}
%%Zloc 153#1@3658
\begin{zed}
\relation (\_ \partition \_)
\end{zed}
%%Zloc 157#1@3710
\begin{gendef}[L,X]
\_ \partition \_ : ( L \rel \power X ) \rel \power X
\where
\forall f : L \rel \power X ; a : \power X @
f \partition a \iff \disjoint f \land \bigcup ( \ran f ) = a
\end{gendef}
%%Zfile /lib/sequence_toolkit.tex
%%Zloc 7#1@137
\begin{zsection}
\SECTION sequence\_toolkit \parents function\_toolkit, number\_toolkit
\end{zsection}
%%Zloc 13#1@266
%%Zinword \upto ..
%%Zloc 64#1@1692
%%Zprechar \# U+0023
%%Zloc 112#1@2845
%%Zpreword \seq seq
%%Zloc 138#1@3497
%%Zpreword \iseq iseq
%%Zloc 152#1@3791
%%Zprechar \langle U+27E8
%%Zloc 153#1@3817
%%Zpostchar \rangle U+27E9
%%Zloc 166#1@4087
%%Zinchar \cat U+2040
%%Zloc 255#1@6252
%%Zinchar \extract U+21BF
%%Zloc 274#1@6721
%%Zinchar \filter U+21BE
%%Zloc 293#1@7168
%%Zinword \prefix prefix
%%Zloc 310#1@7487
%%Zinword \suffix suffix
%%Zloc 327#1@7825
%%Zinword \infix infix
%%Zloc 344#1@8176
%%Zinword \dcat {\cat}/
%%Zloc 14#1@285
\begin{zed}
\function 20 \leftassoc (\_ \upto \_)
\end{zed}
%%Zloc 18#1@346
\begin{axdef}
\_ \upto \_ : \arithmos \cross \arithmos \pfun \power \arithmos
\where
(\num \cross \num) \dres (\_ \upto \_) \in \num \cross \num \fun \power \num
\also
\forall i , j : \num @ i \upto j = \{~ k : \num | i \leq k \leq j ~\}
\end{axdef}
%%Zloc 32#1@752
\begin{gendef}[X]
iter : \num \fun (X \rel X) \fun (X \rel X)
\where
\forall r : X \rel X @ iter ~ 0 ~ r = \id X
\also
\forall r : X \rel X; n : \nat @ iter~(n+1)~r = r \comp (iter~n~r)
\also
\forall r : X \rel X; n : \nat @ iter~(\negate n)~r = iter~n~(r \inv)
\end{gendef}
%%Zloc 50#1@1421
\begin{zed}
\function (\_~^{~\_~})
\end{zed}
%%Zloc 54#1@1467
\begin{gendef}[X]
\_~^{~\_~} : (X \rel X) \cross \num \fun (X \rel X)
\where
\forall r : X \rel X; n : \nat @ r~^{~n~} = iter~n~r
\end{gendef}
%%Zloc 65#1@1713
\begin{zed}
\function (\# \_)
\end{zed}
%%Zloc 69#1@1754
\begin{gendef}[X]
\# \_ : \finset X \fun \nat
\where
\forall a : \finset X @ \# a = (\mu n : \nat | ( \exists f : 1 \upto n \inj a @ \ran f = a ) )
\end{gendef}
%%Zloc 80#1@2075
\begin{zed}
\function (min~\_)
\end{zed}
%%Zloc 84#1@2117
\begin{axdef}
min~\_ : \power \arithmos \pfun \arithmos
\where
\power \num \dres (min~\_) = \{~ a : \power \num ; m : \num | m \in a \land ( \forall n : a @ m \leq n ) @ a \mapsto m ~\}
\end{axdef}
%%Zloc 96#1@2454
\begin{zed}
\function (max~\_)
\end{zed}
%%Zloc 100#1@2496
\begin{axdef}
max~\_ : \power \arithmos \pfun \arithmos
\where
\power \num \dres (max~\_) = \{~ a : \power \num ; m : \num | m \in a \land ( \forall n : a @ n \leq m ) @ a \mapsto m ~\}
\end{axdef}
%%Zloc 113#1@2865
\begin{zed}
\generic (\seq \_)
\end{zed}
%%Zloc 117#1@2907
\begin{zed}
\seq X == \{~ f : \nat \ffun X | \dom f = 1 \upto \# f ~\}
\end{zed}
%%Zloc 130#1@3322
\begin{zed}
\seq_1 X == \seq X \setminus \{ \emptyset \}
\end{zed}
%%Zloc 139#1@3519
\begin{zed}
\generic (\iseq \_)
\end{zed}
%%Zloc 143#1@3562
\begin{zed}
\iseq X == \seq X \cap (\nat \pinj X)
\end{zed}
%%Zloc 154#1@3844
\begin{zed}
\function (\langle \listarg \rangle)
\end{zed}
%%Zloc 158#1@3904
\begin{zed}
\langle \listarg \rangle [ X ] == \lambda s : \seq X @ s
\end{zed}
%%Zloc 167#1@4109
\begin{zed}
\function 30 \leftassoc (\_ \cat \_)
\end{zed}
%%Zloc 172#1@4170
\begin{gendef}[X]
\_ \cat \_ : \seq X \cross \seq X \fun \seq X
\where
\forall s , t : \seq X @
s \cat t = s \cup \{~ n : \dom t @ n + \# s \mapsto t~n ~\}
\end{gendef}
%%Zloc 186#1@4581
\begin{gendef}[X]
rev : \seq X \fun \seq X
\where
\forall s : \seq X @ rev~s = \lambda n : \dom s @ s ( \# s - n + 1 )
\end{gendef}
%%Zloc 197#1@4843
\begin{gendef}[X]
head : \seq_1 X \fun X
\where
\forall s : \seq_1 X @ head~s = s~1
\end{gendef}
%%Zloc 208#1@5073
\begin{gendef}[X]
last : \seq_1 X \fun X
\where
\forall s : \seq_1 X @ last~s = s ( \# s )
\end{gendef}
%%Zloc 219#1@5309
\begin{gendef}[X]
tail : \seq_1 X \fun \seq X
\where
\forall s : \seq_1 X @ tail~s = \lambda n : 1 \upto (\# s - 1) @ s ( n + 1 )
\end{gendef}
%%Zloc 231#1@5657
\begin{gendef}[X]
front : \seq_1 X \fun \seq X
\where
\forall s : \seq_1 X @ front~s = \{ \# s \} \ndres s
\end{gendef}
%%Zloc 243#1@5942
\begin{gendef}[X]
squash : ( \num \ffun X ) \fun \seq X
\where
\forall f : \num \ffun X @ squash~f =
\{~ p : f @ \# \{~ i : \dom f | i \leq p.1 ~\} \mapsto p.2 ~\}
\end{gendef}
%%Zloc 256#1@6278
\begin{zed}
\function 45 \rightassoc (\_ \extract \_)
\end{zed}
%%Zloc 260#1@6343
\begin{gendef}[X]
\_ \extract \_ : \power \num \cross \seq X \fun \seq X
\where
\forall a : \power \num ; s : \seq X @
a \extract s = squash ( a \dres s )
\end{gendef}
%%Zloc 275#1@6746
\begin{zed}
\function 40 \leftassoc (\_ \filter \_)
\end{zed}
%%Zloc 279#1@6809
\begin{gendef}[X]
\_ \filter \_ : \seq X \cross \power X \fun \seq X
\where
\forall s : \seq X ; a : \power X @
s \filter a = squash ( s \rres a )
\end{gendef}
%%Zloc 294#1@7193
\begin{zed}
\relation (\_ \prefix \_)
\end{zed}
%%Zloc 298#1@7242
\begin{gendef}[X]
\_ \prefix \_ : \seq X \rel \seq X
\where
\forall s,t: \seq X @
s \prefix t \iff s \subseteq t
\end{gendef}
%%Zloc 311#1@7512
\begin{zed}
\relation (\_ \suffix \_)
\end{zed}
%%Zloc 315#1@7561
\begin{gendef}[X]
\_ \suffix \_ : \seq X \rel \seq X
\where
\forall s,t: \seq X @
s \suffix t \iff ( \exists u: \seq X @ u \cat s = t)
\end{gendef}
%%Zloc 328#1@7848
\begin{zed}
\relation (\_ \infix \_)
\end{zed}
%%Zloc 332#1@7896
\begin{gendef}[X]
\_ \infix \_ : \seq X \rel \seq X
\where
\forall s,t: \seq X @
s \infix t \iff ( \exists u,v: \seq X @ u \cat s \cat v = t)
\end{gendef}
%%Zloc 345#1@8200
\begin{gendef}[X]
\dcat : \seq \seq X \fun \seq X
\where
\dcat \langle \rangle = \langle \rangle
\also
\forall s : \seq X @ \dcat \langle s \rangle = s
\also
\forall q , r : \seq \seq X @ \dcat ( q \cat r ) = ( \dcat q ) \cat ( \dcat r )
\end{gendef}
%%Zfile /lib/standard_toolkit.tex
%%Zloc 1#1@0
\begin{zsection}
\SECTION standard\_toolkit \parents sequence\_toolkit
\end{zsection}
%%Zfile /lib/permutemarkup.tex
%%Zloc 1#1@0
\begin{zsection}
\SECTION permuteMarkup \parents standard\_toolkit
\end{zsection}
%%Zloc 15#1@218
%%Zword \mynum 43
%%Zloc 7#1@134
\begin{axdef}
\mynum == 44
\end{axdef}
%%Zloc 11#1@174
\begin{axdef}
x == 42 + \mynum
\end{axdef}
]
> but was:<...ile /lib/prelude.tex[
%%Zloc 18#1@470
n of prelude}
\begin{zsection}
\SECTION prelu
%%Zloc 26#1@639
ols are as follows
%%Zloc 27#1@657
.
%
%%Zchar \{
%%Zloc 28#1@675
U+007B
%%Zchar \} U+007
%%Zloc 29#1@699
D
%%Zinchar \where U+
%%Zloc 30#1@721
007C
%%Zchar \Delt
%%Zloc 31#1@740
a U+0394
%%Zchar \Xi U+0
%%Zloc 32#1@765
39E
%%Zprechar \theta U+0
%%Zloc 33#1@791
3B8
%%Zprechar \lambd
%%Zloc 34#1@813
a U+03BB
%%Zprechar \
%%Zloc 35#1@835
mu U+03BC
%%Zchar \ld
%%Zloc 36#1@857
ata U+27EA
%%Zchar \r
%%Zloc 37#1@879
data U+27EB
%%Zchar \
%%Zloc 38#1@901
lblot U+2989
%%Zchar
%%Zloc 39#1@923
\rblot U+298A
%%Zchar
%%Zloc 40#1@946
\vdash U+22A2
%%Zinch
%%Zloc 41#1@968
ar \land U+2227
%%Zinchar
%%Zloc 42#1@994
\lor U+2228
%%Zincha
%%Zloc 43#1@1016
r \implies U+21D2
%%Zin
%%Zloc 44#1@1040
char \iff U+21D4
%%Zprech
%%Zloc 45#1@1066
ar \lnot U+00AC
%%Zprecha
%%Zloc 46#1@1092
r \forall U+2200
%%Z
%%Zloc 47#1@1113
prechar \exists U+2203
%%Zloc 48#1@1136
%%Zinchar \in U+2208
%%Zloc 49#1@1159
%%Zinchar \spot U+2981
%%
%%Zloc 50#1@1185
Zinchar \hide U+29F9
%
%%Zloc 51#1@1208
%Zinchar \project U+2A2
%%Zloc 52#1@1231
1
%%Zinchar \semi
%%Zloc 53#1@1249
U+2A1F
%%Zinchar \p
%%Zloc 54#1@1270
ipe U+2A20
%%Zprewor
%%Zloc 55#1@1291
d \IF if
%%Zinword
%%Zloc 56#1@1311
\THEN then
%%Zinwor
%%Zloc 57#1@1331
d \ELSE else
%%Zpreword \LET
%%Zloc 58#1@1360
let
%%Zpreword \pre pre
%%Zloc 59#1@1387
%%Zinword \function function
%%Zloc 60#1@1416
%%Zinword \generic generic
%%
%%Zloc 61#1@1447
Zinword \relation relation
%%Zin
%%Zloc 62#1@1480
word \leftassoc leftassoc
%%Zloc 63#1@1506
%%Zinword \rightas
%%Zloc 64#1@1525
soc rightassoc
%%Zinword
%%Zloc 65#1@1550
\listarg {,}{,}
%%Zinw
%%Zloc 66#1@1574
ord \varg \_
%%Zprechar \pow
%%Zloc 67#1@1603
er U+2119
%%Zinchar
%%Zloc 71#1@1699
up directives for the
%%Zloc 72#1@1721
rest of the Greek alp
%%Zloc 73#1@1742
habet are as follows.
%%Zloc 74#1@1764
%
%%Zchar \alpha U+
%%Zloc 75#1@1786
03B1
%%Zchar \beta U+03
%%Zloc 76#1@1810
B2
%%Zchar \gamma U+
%%Zloc 77#1@1831
03B3
%%Zchar \delta
%%Zloc 78#1@1851
U+03B4
%%Zchar \eps
%%Zloc 79#1@1872
ilon U+03B5
%%Zchar \
%%Zloc 80#1@1894
zeta U+03B6
%%Zcha
%%Zloc 81#1@1913
r \eta U+03B7
%%Zc
%%Zloc 82#1@1932
har \iota U+03B9
%
%%Zloc 83#1@1951
%Zchar \kappa U+03BA
%%Zloc 84#1@1971
%%Zchar \nu U+03BD
%%Zloc 85#1@1993
%%Zchar \xi U+03BE
%%Zloc 86#1@2013
%%Zchar \pi U+03C0
%%Zc
%%Zloc 87#1@2037
har \rho U+03C1
%%Z
%%Zloc 88#1@2057
char \sigma U+03C3
%%Zloc 89#1@2077
%%Zchar \tau U+03C4
%%Zloc 90#1@2097
%%Zchar \upsilon U+03
%%Zloc 91#1@2119
C5
%%Zchar \phi U+03C
%%Zloc 92#1@2141
6
%%Zchar \chi U+03C7
%%Zloc 93#1@2163
%%Zchar \psi U+03C8
%%Zloc 94#1@2186
%%Zchar \omega U+03
%%Zloc 95#1@2205
C9
%%Zchar \Gamma U+0
%%Zloc 96#1@2227
393
%%Zchar \Theta U+03
%%Zloc 97#1@2251
98
%%Zchar \Lambda
%%Zloc 98#1@2271
U+039B
%%Zchar \Pi
%%Zloc 99#1@2291
U+03A0
%%Zchar \Sigma
%%Zloc 102#1@2321
%%Zchar \Upsilon U+03A5
%%Zchar \Phi U+03
%%Zloc 119#1@2903
lies amongst those of user-defined
%%Zloc 126#1@3058
The given type $\arithmos$, pronounced ``arithmos
%%Zloc 139#1@3337
seem right... should be an axdef?
%Changed by Tim Miller
%\begin{zed}
%number_lit
%%Zloc 147#1@3542
: \nat
\end{axdef}
$0$ and $1$ are natural numbers, a
%%Zloc 151#1@3599
ll uses of which are transformed
to references to these declarations (see 12.2.6.9).
\begin{zed}
\function 30 \leftassoc (\_ + \_)
\end{zed}
\begin{axdef}
\_ + \_ : \power ((\arithmos \cross \arithmos) \cross \arithmos)
\where
\forall m, n: \nat @ \exists_1 p: ( \_ + \_ ) @ p.1 = (m, n)\\
\forall m, n: \nat @ m + n \in \nat\\
\forall m, n: \nat | m + 1 = n + 1 @ m = n\\
\forall n: \nat @ \lnot n + 1 = 0\\
\forall w: \po
%%Zfile /lib/set_toolkit.tex
%%Zloc 8#1@179
ns}
\begin{zsection}
\SECTION set\_toolkit
\end{z
%%Zloc 14#1@256
elations}
%%Zinchar
%%Zloc 29#1@609
sclause{Total function
%%Zloc 46#1@1025
e{Sets}
\ssclause{I
%%Zloc 62#1@1327
are not equal to each ot
%%Zloc 79#1@1697
type, $a$,
for which $x
%%Zloc 89#1@1886
any type is the set of that
%%Zloc 106#1@2275
$a$ and $b$,
such that
%%Zloc 137#1@2951
f $X$.
\begin{note}
%%Zloc 153#1@3321
n b ~\}
\end{gendef}
%%Zloc 169#1@3696
a \land x \in b ~\}
\end{g
%%Zloc 185#1@4140
ef}
The difference of t
%%Zloc 202#1@4591
\end{gendef}
The symme
%%Zloc 214#1@4953
A @ x \in a ~\}
\end{gen
%%Zloc 229#1@5341
}
\end{gendef}
The general
%%Zloc 15#1@278
\rel U+2194
\begin{zed}
\generic 5 \rightassoc (\_ \rel
%%Zloc 19#1@337
\_)
\end{zed}
\begin{zed}
X \rel Y == \power ( X \cr
%%Zloc 30#1@631
s}
%%Zinchar \fun U+2192
\begin{zed}
\generic 5 \right
%%Zloc 34#1@690
assoc (\_ \fun \_)
\end{zed}
\begin{zed}
X \fun Y == \{~ f : X \rel Y | \forall x : X @ \exists_1 y :
%%Zloc 47#1@1047
nequality relation}
%%Zinchar \neq U+2260
%%Zloc 51#1@1093
\begin{zed}
\relation (\_ \neq \_)
\end{zed}
\begin{gendef}[X]
\_ \neq \_ : X \rel X
\where
\forall
%%Zloc 63#1@1351
her.
\ssclause{Non-membership}
%%Zinchar \
%%Zloc 67#1@1399
notin U+2209
\begin{zed}
\relation (\_ \notin \_)
\end{zed}
\begin{gendef}[X]
\_ \notin \_ : X \rel \power X
\where
\foral
%%Zloc 80#1@1722
$ is not a member of $a$.
\ssclause{Empty set}
%%Zchar \em
%%Zloc 90#1@1913
type that has no members.
\ssclause{Subset rel
%%Zloc 94#1@1964
ation}
%%Zinchar \subseteq U+2286
\begin{zed}
\relation (\_ \subseteq \_)
\end{zed}
\begin{gendef}[X]
\_ \subseteq \_ : \power X \rel \power X
%%Zloc 107#1@2300
every member of $a$ is a member of $b$.
\sscla
%%Zloc 111#1@2349
use{Proper subset relation}
%%Zinchar \subset U+2282
\begin{zed}
\relation (\_ \subset \_)
\end{zed}
\begin{gendef}[X]
\_ \subset \_ : \power
%%Zloc 125#1@2674
me type, $a$ and $b$,
such that $a$ is a subset of $b$,
and $a$ and $b$ are
%%Zloc 138#1@2973
The $\power$ symbol is established as a generic operator b
%%Zloc 142#1@3033
y the prelude.
\end{note}
\ssclause{Set union}
%%Zinchar \cup U+222A
\begin{zed}
\function 30 \leftassoc (\_ \cup \_)
\end{zed}
\begin{gendef}[X]
\_ \cu
%%Zloc 154#1@3343
The union of two sets of the same type is the set of valu
%%Zloc 158#1@3403
es
that are members of either set.
\ssclause{Set intersection}
%%Zinchar \cap U+2229
\begin{zed}
\function 40 \leftassoc (\_ \cap \_)
\end{zed}
\begin{gen
%%Zloc 170#1@3723
endef}
The intersection of two sets of the same type is the se
%%Zloc 174#1@3788
t of
values that are members of both sets.
\ssclause{Set difference}
%%Zinchar \setminus U+2216
\begin{zed}
\function 30 \leftassoc (\_ \setminus \_)
\end{zed}
\begin{
%%Zloc 186#1@4166
wo sets of the same type is the set of
values that are members
%%Zloc 190#1@4230
of the first set but not members of the second set.
\ssclause{Set symmetric difference}
%%Zinchar \symdiff U+2296
\begin{zed}
\function 25 \leftassoc (\_ \symdiff \_)
\end{ze
%%Zloc 203#1@4617
tric set difference of two sets of the same type is
the set of values that are members of one set, or the other,
but not members of both.
\ssclause{Generaliz
%%Zloc 215#1@4979
def}
The generalized union of a set of sets of the same type is
the set of values of that type that are members of at least one of the sets.
\ssclause{Gen
%%Zloc 230#1@5371
ized intersection of a set of sets of values
%%Zloc 234#1@5416
of the same
type is the set of values of that type that are members of
every one of the sets.
\sclause{Finite sets}
\ssclause{Finite subse
%%Zloc 246#1@5821
n $\finset X$ is the set of all finite subsets of $X$.
The set of finite
%%Zfile /lib/number_toolkit.tex
%%Zloc 7#1@135
s}
\begin{zsection}
\SECTION number\_toolkit
\end{zs
%%Zloc 27#1@442
\ssclause{Integer
%%Zloc 43#1@900
tion of integers, arithmet
%%Zloc 132#1@3340
forall i , j : \num @
%%Zloc 163#1@3943
, j : \num @ i < j \if
%%Zloc 256#1@6127
%\\ \t1 ( i * j
%%Zloc 257#1@6146
) * k = i * ( j * k
%%Zloc 13#1@215
ccessor}
\begin{zed}
\function (succ~\_
%%Zloc 17#1@258
)
\end{zed}
\begin{axdef}
succ~\_ : \power (\nat \cross \nat)
\where
(succ~\_) = \lambda n : \nat
%%Zloc 28#1@462
s}
%%Zchar \num U+2124
\begin{axdef}
\num : \p
%%Zloc 44#1@926
ic negation}
%%Zprechar \negate U+002D
\be
%%Zloc 48#1@972
gin{zed}
\function (\negate \_)
\end{zed}
\begin{axdef}
\negate \_ : \power (\arithmos \cross \arithmos)
\where
\forall x, y : \num @ \exists_1 z : \num @ ((x,y),z) \in (\_ + \_)\\
\forall x : \num @ \exists_1 y : \num @ (x,y) \in (\negate \_)
\also
\forall i , j , k : \num @
\\ \t1 ( i + j ) + k = i + ( j + k )
\\ \t1 \land i + j = j + i
\\ \t1 \land i + \negate i = 0
\\ \t1 \land i + 0 = i
\also
\num = \{ z : \arithmos | \
%%Zloc 99#1@2510
\implies h = \num
%\end{axdef}
\end{note}
%%reckless 0
%%Zloc 103#1@2567
%%quiet 0
\ssclause{Subtraction}
\begin{zed}
\function 30 \leftassoc (\_ - \_)
\end{zed}
\begin{axdef}
\_ - \_ : \power ((\arithmos \cross \arithmos) \cross \arithmos)
\where
\forall x, y : \num @ \exi
%%Zloc 133#1@3362
i - j = i + \negate j
%\end{axdef}
\end{note
%%Zloc 137#1@3408
}
%%reckless 0
%%quiet 0
\ssclause{Less-than-or-equal}
%%Zinchar \leq U+2264
\begin{zed}
\relation (\_ \leq \_)
\end{zed}
%%Zloc 148#1@3669
\end{axdef}
For all integers $i$ and $j
%%Zloc 152#1@3712
$, $i \leq j$ if and only if
their difference $j - i$ is a natural number.
\ssclause{Less-than}
\begin{zed}
\relation
%%Zloc 164#1@3965
f i + 1 \leq j
\end{axdef}
For all integer
%%Zloc 168#1@4011
s $i$ and $j$,
$i < j$ if and only if $i + 1 \leq j$.
\ssclause{Greater-than-or-equal}
%%Zinchar \geq U+2265
\begin{zed}
%%Zloc 179#1@4234
ithmos)
\where
\forall i , j : \num @ i \
%%Zloc 183#1@4277
geq j \iff j \leq i
\end{axdef}
For all integers $i$ and $j$,
$i \geq j$ if and only if $j \leq i$.
\ssclause{Gr
%%Zloc 194#1@4506
ss \arithmos)
\where
\forall i , j : \num @ i > j \iff j < i
%%Zloc 203#1@4684
al numbers}
\begin{zed}
\nat_1 == \{ x : \nat | \lnot x =
%%Zloc 211#1@4848
.
\ssclause{Non-zero integers}
\begin{zed}
\num_1
%%Zloc 215#1@4905
== \{ x : \num | \lnot x = 0 \}
\end{zed}
The non-zero integers $\num_1$ are the integers except zero.
\ssclause{Multiplication of integers}
\begin{zed}
\function 40 \leftassoc (\_ * \_)
\end{zed}
\begin{axdef}
\_ * \_ : \power ((\arithmos \cross \arithmos) \cross \arithmos)
\where
\forall x, y : \num @ \exists_1 z : \num @ ((x,y)
%%Zloc 258#1@6165
)
%\\ \t1 \land i * j = j * i
%\\ \t1 \land i * ( j + k ) = i * j + i * k
%\\ \t1 \land 0 *
%%Zloc 263#1@6264
i = 0
%\\ \t1 \land 1 * i = i
%\end{axdef}
\end{note}
%%reckless 0
%%quiet 0
\ssclause{Division, modulus}
%%Zinword \div div
%%Zinword \mod mod
\begin{zed}
\function 40 \leftassoc (\_ \div \_)\\
\function 40 \leftassoc (\_ \mod \_)
\end{zed}
\begin{axdef}
\_ \div \_~, \_ \mod \_ : \power ((\arithmos \cross \arithmos) \cross \arithmos)
\where
\forall x : \num ; y : \num_1 @ \exists_1 z : \num @ ((
%%Zfile /lib/relation_toolkit.tex
%%Zloc 7#1@156
s}
\begin{zsection}
\SECTION relation\_toolkit \parents set\_toolkit
\end{zs
%%Zloc 35#1@710
the pair.
\ssclause{Ma
%%Zloc 51#1@1053
er notation for $(x,
%%Zloc 63#1@1306
mponents of the orde
%%Zloc 75#1@1571
mponents of the or
%%Zloc 89#1@1821
on that relates every
%%Zloc 109#1@2460
lating the first compon
%%Zloc 125#1@2838
l composition of $s$ an
%%Zloc 141#1@3270
on $r : X \rel Y$ by a
%%Zloc 157#1@3701
on of a relation $r : X
%%Zloc 174#1@4144
main subtraction of a re
%%Zloc 191#1@4588
ndef}
The range subtr
%%Zloc 207#1@4931
: X \rel Y @ r \inv = \
%%Zloc 208#1@4954
{~ p : r @ p.2 \mapsto p.
%%Zloc 224#1@5406
.1 \in a @ p.2 ~\}
\end
%%Zloc 242#1@5902
If $r$ and $s$ are
%%Zloc 260#1@6351
teq s \land r \comp s
%%Zloc 13#1@277
jection}
\begin{gendef}[X,Y]
first : X \cross Y \fun X
\where
\forall x : X; y : Y @ first~(x,y) = x
%%Zloc 24#1@503
mponent projection}
\begin{gendef}[X,Y]
second : X \cross Y \fun Y
\where
\forall x : X; y : Y @ secon
%%Zloc 36#1@735
plet}
%%Zinchar \mapsto U+21A6
\begin{zed}
\function 10 \l
%%Zloc 40#1@798
eftassoc (\_ \mapsto \_)
\end{zed}
\begin{gendef}[X,Y]
\_ \mapsto \_ : X \cross Y \fun X \cross Y
\where
\forall x : X ; y :
%%Zloc 52#1@1073
y)$.
\ssclause{Domain}
%%Zpreword \dom dom
\begin{gendef}[X,Y]
\dom : (X \rel Y) \fun \power X
\where
\forall r :
%%Zloc 64#1@1326
red
pairs in $r$.
\ssclause{Range}
%%Zpreword \ran ran
\begin{gendef}[X,Y]
\ran : (X \rel Y) \fun \power Y
\where
%%Zloc 76#1@1589
dered
pairs in $r$.
\ssclause{Identit
%%Zloc 80#1@1630
y relation}
%%Zpreword \id id
\begin{zed}
\generic (\id
%%Zloc 90#1@1844
member of $X$ to itself.
\ssclause{Relational composition}
%%Zloc 94#1@1905
%%Zinchar \comp U+2A3E
\begin{zed}
\function 40 \leftassoc (\_ \comp \_)
\end{zed}
\begin{gendef}[X,Y,Z]
\_ \comp \_ : (X \rel Y) \cross (Y \rel Z) \fun (X \rel Z)
\where
\forall r : X \rel Y
%%Zloc 110#1@2483
ent of $p$ with the second component of $q$.
\ssclause{Fun
%%Zloc 114#1@2544
ctional composition}
%%Zinchar \circ U+2218
\begin{zed}
\function 40 \leftassoc (\_ \circ \_)
\end{zed}
\begin{gendef}[X,Y,Z]
\_ \circ \_ : (Y \rel Z) \
%%Zloc 126#1@2861
d $r$ is the same as
the relational composition of $r$ and $s
%%Zloc 130#1@2923
$.
\ssclause{Domain restriction}
%%Zinchar \dres U+25C1
\begin{zed}
\function 65 \rightassoc (\_ \dres \_)
\end{zed}
\begin{gendef}[X,Y]
\_ \dres \_ : \power X \cros
%%Zloc 142#1@3293
set $a : \power X$ is
the set of pairs in $r$ whose first co
%%Zloc 146#1@3354
mponents are in $a$.
\ssclause{Range restriction}
%%Zinchar \rres U+25B7
\begin{zed}
\function 60 \leftassoc (\_ \rres \_)
\end{zed}
\begin{gendef}[X,Y]
\_ \rres \_
%%Zloc 158#1@3725
\rel Y$ by a set $b : \power Y$ is
the set of pairs in $r$ who
%%Zloc 162#1@3788
se second components are in $b$.
\ssclause{Domain subtraction}
%%Zinchar \ndres U+2A64
\begin{zed}
\function 65 \rightassoc (\_ \ndres \_)
\end{zed}
\begin{gendef}[X,Y]
\
%%Zloc 175#1@4168
lation $r : X \rel Y$ by
a set $a : \power X$
is the set of
%%Zloc 179#1@4230
pairs in $r$ whose first components are not in $a$.
\ssclause{Range subtraction}
%%Zinchar \nrres U+2A65
\begin{zed}
\function 60 \leftassoc (\_ \nrres \_)
\end{zed}
\beg
%%Zloc 192#1@4612
action of a relation $r : X \rel Y$ by a se
%%Zloc 196#1@4655
t $b : \power Y$
is the set of pairs in $r$ whose second components are not in $b$.
\ssclause{Relational inversion}
%%Zpostchar \inv U+223C
%%Zloc 209#1@4979
1 ~\}
\end{gendef}
The inverse of a relation is t
%%Zloc 213#1@5032
he relation obtained by reversing every
ordered pair in the relation.
\ssclause{Relational image}
%%Zinchar \limg U+2987
%%Zpostchar \rimg U+2988
\begin{zed}
\function (\_ \limg \_ \
%%Zloc 225#1@5430
{gendef}
The relational image of a set $a : \power X$ throu
%%Zloc 229#1@5492
gh a relation $r : X \rel Y$
is the set of values of type $Y$ that are related under $r$ to a value in $a$.
\ssclause{Overriding}
%%Zinchar \oplus U+2295
\begin{zed}
\fu
%%Zloc 243#1@5923
both relations between $X$ and $Y$,
the ove
%%Zloc 247#1@5967
rriding of $r$ by $s$
is the whole of $s$ together with those members of $r$
that have no first components that are in the domain of $s$.
\ssclause{Transitive closure}
%%Zpostwor
%%Zloc 261#1@6372
\subseteq s ~\}
\end{gendef}
The transi
%%Zloc 265#1@6416
tive closure of a relation $r : X \rel X$ is
the smallest set that contains $r$ and
is closed under the action of composing $r$ wi
%%Zfile /lib/function_toolkit.tex
%%Zloc 7#1@137
s}
\begin{zsection}
\SECTION function\_toolkit \parents relation\_toolkit
\end{zs
%%Zloc 13#1@254
nctions}
%%Zinchar \
%%Zloc 29#1@717
ause{Partial injections
%%Zloc 46#1@1247
ynonymous.
\ssclaus
%%Zloc 61#1@1581
tions from $X$ to $Y$.
%%Zloc 77#1@1976
d ``partial surjection'
%%Zloc 92#1@2307
rom $X$ to $Y$
that a
%%Zloc 107#1@2640
ctions from $X$ to $Y$
%%Zloc 121#1@2926
ctions from $X$ to $Y$
%%Zloc 135#1@3225
ons from $X$ to $Y$ are the in
%%Zloc 152#1@3627
{gendef}
A labelled family o
%%Zloc 14#1@277
pfun U+21F8
\begin{zed}
\generic 5 \rightassoc (\_ \pfun \
%%Zloc 18#1@337
_)
\end{zed}
\begin{zed}
X \pfun Y == \{~ f : X \rel Y | \forall p , q : f | p.1 = q.1 @ p.2 = q
%%Zloc 30#1@740
}
%%Zinchar \pinj U+2914
\begin{zed}
\generic 5 \righta
%%Zloc 34#1@800
ssoc (\_ \pinj \_)
\end{zed}
\begin{zed}
X \pinj Y == \{~ f : X \rel Y | \forall p, q : f @ p.1 =
%%Zloc 47#1@1269
e{Total injections}
%%Zinchar \inj U+21A3
\begin{zed}
%%Zloc 51#1@1328
\generic 5 \rightassoc (\_ \inj \_)
\end{zed}
\begin{zed}
X \i
%%Zloc 62#1@1605
\ssclause{Partial surjections}
%%Zinchar \psurj U+2900
%%Zloc 66#1@1666
\begin{zed}
\generic 5 \rightassoc (\_ \psurj \_)
\end{zed}
\begin{
%%Zloc 78#1@1999
' are synonymous.
\ssclause{Total surjections}
%%Zinch
%%Zloc 82#1@2059
ar \surj U+21A0
\begin{zed}
\generic 5 \rightassoc (\_ \surj \_)
%%Zloc 93#1@2329
re also total functions from $X$ to $Y$.
\ssclause{Bijec
%%Zloc 97#1@2388
tions}
%%Zinchar \bij U+2916
\begin{zed}
\generic 5 \rightasso
%%Zloc 108#1@2663
that are also total injections from $X$ to $Y$.
\ssclaus
%%Zloc 112#1@2723
e{Finite functions}
%%Zinchar \ffun U+21FB
\begin{zed}
\generic 5 \ri
%%Zloc 122#1@2949
are the functions from $X$ to $Y$
that are also finite sets
%%Zloc 126#1@3009
.
\ssclause{Finite injections}
%%Zinchar \finj U+2915
\begin{z
%%Zloc 136#1@3255
jections from $X$ to $Y$
that are also finite f
%%Zloc 140#1@3303
unctions from $X$ to $Y$.
\ssclause{Disjointness}
%%Zpreword \disjoint disjoint
\begin{zed}
\relation (\disjoint \_)
\end{zed}
\begin{gendef}[L,X]
\disjoint \_ : \power ( L \rel
%%Zloc 153#1@3658
f sets is disjoint precisely when any
distinct pair
%%Zloc 157#1@3710
yields sets with no members in common.
\ssclause{Partitions}
%%Zinword \partition partition
\begin{zed}
\relation (\_ \partition \_)
\end{zed}
\begin{gendef}[L,X]
\_ \partition \_ : ( L
%%Zfile /lib/sequence_toolkit.tex
%%Zloc 7#1@137
s}
\begin{zsection}
\SECTION sequence\_toolkit \parents function\_toolkit, number\_toolkit
\end{zs
%%Zloc 13#1@266
r range}
%%Zinwo
%%Zloc 64#1@1692
ten as $r ^{ n }$.
%%Zloc 112#1@2845
ater than or equal
%%Zloc 138#1@3497
emptyset \}
\end{zed}
%%Zloc 152#1@3791
f all injective finite seq
%%Zloc 153#1@3817
uences of values of $X$,
t
%%Zloc 166#1@4087
arg \rangle [ X ] ==
%%Zloc 255#1@6252
orall f : \num \ffun X @ s
%%Zloc 274#1@6721
@
a \extract s = squas
%%Zloc 293#1@7168
orall s : \seq X ; a : \p
%%Zloc 310#1@7487
begin{zed}
\relation (\_
%%Zloc 327#1@7825
gin{zed}
\relation (\_
%%Zloc 344#1@8176
begin{zed}
\relation (\
%%Zloc 14#1@285
rd \upto ..
\begin{zed}
\function 20 \leftassoc (\_ \upto \
%%Zloc 18#1@346
_)
\end{zed}
\begin{axdef}
\_ \upto \_ : \arithmos \cross \arithmos \pfun \power \arithmos
\where
(\num \cross \num) \dres (\_ \upto \_) \in \num \cross \num \fun \power \num
\also
\forall i , j : \num @ i \upto j = \{~ k : \num | i \leq k \l
%%Zloc 32#1@752
j$.
\ssclause{Iteration}
\begin{gendef}[X]
iter : \num \fun (X \rel X) \fun (X \rel X)
\where
\forall r : X \rel X @ iter ~ 0 ~ r = \id X
\also
\forall r : X \rel X; n : \nat @ iter~(n+1)~r = r \comp (iter~n~r)
\also
\forall r : X \rel X; n : \nat @ iter~(\negate
%%Zloc 50#1@1421
for $n$ times of the inverse of the relation.
%%Zloc 54#1@1467
\begin{zed}
\function (\_~^{~\_~})
\end{zed}
\begin{gendef}[X]
\_~^{~\_~} : (X \rel X) \cross \num \fun (X \rel X)
\where
\forall r :
%%Zloc 65#1@1713
\ssclause{Number of members of a set}
%%Zloc 69#1@1754
%%Zprechar \# U+0023
\begin{zed}
\function (\# \_)
\end{zed}
\begin{gendef}[X]
\# \_ : \finset X \fun \nat
\where
\forall a : \finset X @ \# a = (\mu n
%%Zloc 80#1@2075
g at $1$ that can be put into bijection wi
%%Zloc 84#1@2117
th the set.
\ssclause{Minimum}
\begin{zed}
\function (min~\_)
\end{zed}
\begin{axdef}
min~\_ : \power \arithmos \pfun \arithmos
\where
\power \num \dres (min~\_) = \{~ a : \power \num ;
%%Zloc 96#1@2454
an or equal
to all members of that set,
%%Zloc 100#1@2496
that member is its minimum.
\ssclause{Maximum}
\begin{zed}
\function (max~\_)
\end{zed}
\begin{axdef}
max~\_ : \power \arithmos \pfun \arithmos
\where
\power \num \dres (max~\_) = \{~ a
%%Zloc 113#1@2865
to all members of that set,
that member i
%%Zloc 117#1@2907
s its maximum.
\ssclause{Finite sequences}
%%Zpreword \seq seq
\begin{zed}
%%Zloc 130#1@3322
is, of finite functions from the set $1 \upto n$,
for some $n$, to
%%Zloc 139#1@3519
$\seq_1 X$ is the set of all non-empty
%%Zloc 143#1@3562
finite sequences of values of $X$.
\ssclause{Injective seq
%%Zloc 154#1@3844
hat is, of finite sequences over $X$ that are also injection
%%Zloc 158#1@3904
s.
\ssclause{Sequence brackets}
%%Zprechar \langle U+27E8
%%Zpostchar \ran
%%Zloc 167#1@4109
\lambda s : \seq X @ s
\end{zed}
The brackets $\langle$ a
%%Zloc 172#1@4170
nd $\rangle$ can be used for enumerated sequences.
\ssclause{Concatenation}
%%Zinchar \cat U+2040
\begin{zed}
\function 30 \leftassoc (\_ \cat \_)
\end{zed}
%%Zloc 186#1@4581
alues of the same type whose result is a sequence that
begins with all elements of the first sequence and
continues with all elemen
%%Zloc 197#1@4843
~s = \lambda n : \dom s @ s ( \# s - n + 1 )
\end{gendef}
The reverse of a sequence is the seq
%%Zloc 208#1@5073
\fun X
\where
\forall s : \seq_1 X @ head~s = s~1
\end{gendef}
If $s$ is a non-empty sequence of v
%%Zloc 219#1@5309
q_1 X \fun X
\where
\forall s : \seq_1 X @ last~s = s ( \# s )
\end{gendef}
If $s$ is a non-empty sequence of values,
then $last~s$ is th
%%Zloc 231#1@5657
)
\end{gendef}
If $s$ is a non-empty sequence of values,
then $tail~s$ is the sequence of values that is obtained f
%%Zloc 243#1@5942
\forall s : \seq_1 X @ front~s = \{ \# s \} \ndres s
\end{gendef}
If $s$ is a non-empty sequence of values,
then $front~s$ is the sequence of values that is obtained from $
%%Zloc 256#1@6278
quash~f =
\{~ p : f @ \# \{~ i : \dom f | i \leq p.1 ~\} \mapst
%%Zloc 260#1@6343
o p.2 ~\}
\end{gendef}
$squash$ takes a finite function $f : \num \ffun X$
and renumbers its domain to produce a finite sequence.
\ssclause{Extraction}
%%Zinch
%%Zloc 275#1@6746
h ( a \dres s )
\end{gendef}
The extraction of a set $a$ of
%%Zloc 279#1@6809
indices from a sequence
is the sequence obtained from the original by discarding any indices
that are not in the set $a$,
then renumbering the remainder.
\
%%Zloc 294#1@7193
ower X @
s \filter a = squash ( s \rres a )
\e
%%Zloc 298#1@7242
nd{gendef}
The filter of a sequence by a set $a$
is the sequence obtained from the original by discarding any members
that
%%Zloc 311#1@7512
\prefix \_)
\end{zed}
\begin{gendef}[X]
\_
%%Zloc 315#1@7561
\prefix \_ : \seq X \rel \seq X
\where
\forall s,t: \seq X @
s \prefix t \iff s \subseteq t
\end{gendef}
A sequence $s$ is a prefix of another
%%Zloc 328#1@7848
\suffix \_)
\end{zed}
\begin{gendef}[X]
\_
%%Zloc 332#1@7896
\suffix \_ : \seq X \rel \seq X
\where
\forall s,t: \seq X @
s \suffix t \iff ( \exists u: \seq X @ u \cat s = t)
\end{gendef}
A sequence $s$ is a s
%%Zloc 345#1@8200
_ \infix \_)
\end{zed}
\begin{gendef}[X]
\_ \infix \_ : \seq X \rel \seq X
\where
\forall s,t: \seq X @
s \infix t \iff ( \exists u,v: \seq X @ u \cat s \cat v = t)
\end{gendef}
A sequence $s$ is an infix of another sequence $t$
if it form
%%Zfile /lib/standard_toolkit.tex
%%Zloc 1#1@0
\begin{zsection}
\SECTION standard\_toolkit \parents sequence\_toolkit
\end{zsection
%%Zfile /lib/permutemarkup.tex
%%Zloc 1#1@0
\begin{zsection}
\SECTION permuteMarkup \parents standard\_toolkit
\end{zsection
%%Zloc 15#1@218
end{axdef}
%%Zw
%%Zloc 7#1@134
n.
\begin{axdef}
\mynum == 44
\end{
%%Zloc 11#1@174
axdef}
\begin{axdef}
x == 42 + \mynum
\]
>
at junit.framework.Assert.assertEquals(Assert.java:81)
at junit.framework.Assert.assertEquals(Assert.java:87)
at net.sourceforge.czt.specreader.SpecReaderTester.specReaderTester(SpecReaderTester.java:50)
at net.sourceforge.czt.specreader.PermuteMarkupTest.testPermuteMarkup(PermuteMarkupTest.java:31)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:597)
at junit.framework.TestCase.runTest(TestCase.java:168)
at junit.framework.TestCase.runBare(TestCase.java:134)
at junit.framework.TestResult$1.protect(TestResult.java:110)
at junit.framework.TestResult.runProtected(TestResult.java:128)
at junit.framework.TestResult.run(TestResult.java:113)
at junit.framework.TestCase.run(TestCase.java:124)
at junit.framework.TestSuite.runTest(TestSuite.java:232)
at junit.framework.TestSuite.run(TestSuite.java:227)
at org.junit.internal.runners.JUnit38ClassRunner.run(JUnit38ClassRunner.java:79)
at org.apache.maven.surefire.junit4.JUnit4TestSet.execute(JUnit4TestSet.java:59)
at org.apache.maven.surefire.suite.AbstractDirectoryTestSuite.executeTestSet(AbstractDirectoryTestSuite.java:120)
at org.apache.maven.surefire.suite.AbstractDirectoryTestSuite.execute(AbstractDirectoryTestSuite.java:103)
at org.apache.maven.surefire.Surefire.run(Surefire.java:169)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:597)
at org.apache.maven.surefire.booter.SurefireBooter.runSuitesInProcess(SurefireBooter.java:350)
at org.apache.maven.surefire.booter.SurefireBooter.main(SurefireBooter.java:1021)
|
