Tests by plug feature LetDef2; CLI Option: -workers 1

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
08ffcaa9d0af83f5faafae8332fd3bf2c92fdd7f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	And	LetDef2	True	Passed	Model Under Test Equivalent Model
70889423d7188b852a135ec5b8ceb91331807cb0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	And	LetDef2	False	Passed	Model Under Test Equivalent Model
7e1ed117833ce2b7a7ec373adb2e57ccde431f48	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B) Plug Feature: LET definitions are reduced to global definitions	AndMultiLine	LetDef2	True	Passed	Model Under Test Equivalent Model
38cddd79dc01d496b2b2d6d3dbded0e646335bf1	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B) Plug Feature: LET definitions are reduced to global definitions	AndMultiLine	LetDef2	False	Passed	Model Under Test Equivalent Model
9e1933b969225f1836650c8d7404ecf3bed091fe	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Imply	LetDef2	True	Passed	Model Under Test Equivalent Model
49acbb54959aa555cb70532ce58811b5e2054b97	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Imply	LetDef2	False	Passed	Model Under Test Equivalent Model
6d2e6f4d91ba8afd4a5da2fc04f9c42cc34a8f64	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Not	LetDef2	True	Passed	Model Under Test Equivalent Model
51e3679f930609e16a145084707a180c9e1c834b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Not	LetDef2	False	Passed	Model Under Test Equivalent Model
44fbddede86259c31107320933328008f86b8a4c	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B) Plug Feature: LET definitions are reduced to global definitions	Or	LetDef2	True	Passed	Model Under Test Equivalent Model
9f0e57e720e4642c648fcbc653648774231a1767	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B) Plug Feature: LET definitions are reduced to global definitions	Or	LetDef2	False	Passed	Model Under Test Equivalent Model
d85978fc0ffa6d0d18e6c2a2aaeac9089d04a1c9	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B) Plug Feature: LET definitions are reduced to global definitions	OrMultiLine	LetDef2	True	Passed	Model Under Test Equivalent Model
d6d2d6ba1eb80440af30de17ca870bb3b29d8eb8	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B) Plug Feature: LET definitions are reduced to global definitions	OrMultiLine	LetDef2	False	Passed	Model Under Test Equivalent Model
3fe72060f00e3f069bed10f3daa188c02685338d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AndProp	LetDef2	True	Passed	Model Under Test Equivalent Model
568a9c26d30ec72656538b9e52d4ad5856be9743	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AndProp	LetDef2	False	Passed	Model Under Test Equivalent Model
74a930912efac3cf8bb023cee05237cac4ce01ff	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Boxed	LetDef2	True	Passed	Model Under Test Equivalent Model
ef98d4ec8b8ca4e52fa33535608a20ff123d2b05	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Boxed	LetDef2	False	Passed	Model Under Test Equivalent Model
91d17acf55d5b0b2f127d7a24ccac39c30c4e925	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDef2	True	Passed	Model Under Test Equivalent Model
e92294d46bf7b5e42fdd61f509d88ff891f65557	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDef2	False	Passed	Model Under Test Equivalent Model
770b03dbfe0ed67350aeee741d4338cb26d8c4bf	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Ne	LetDef2	True	Passed	Model Under Test Equivalent Model
fa56f796c91e6895dd8a78195717da8c5557b43f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Ne	LetDef2	False	Passed	Model Under Test Equivalent Model
40c2798d052465adbf3889ca87c468613ae98d0f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Let	LetDef2	True	Passed	Model Under Test Equivalent Model
1d91b440081b49997783ff7fbbae4394d033e127	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Let	LetDef2	False	Passed	Model Under Test Equivalent Model
53767fede3cb7026371bafbf5f8e18ce3540cab3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDef2	True	Passed	Model Under Test Equivalent Model
6e7322b33656f90b87ac6ae4349fa9589ebe2eaf	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDef2	False	Passed	Model Under Test Equivalent Model
c926a3c8dafa9a7964ac7b11dc27e5499f68417b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDef2	True	Passed	Model Under Test Equivalent Model
cefb7238e9c324a002bd1dc1c3d095bd80bb1dc0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDef2	False	Passed	Model Under Test Equivalent Model
2aece2a2df029d2e8022572522f474a8f3787bbe	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDef2	True	Passed	Model Under Test Equivalent Model
d574051a34559c809d2e9344d8b21566a9fb7ad7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDef2	False	Passed	Model Under Test Equivalent Model
31e0ca6100b4896e21f1dd58990982c27a1e2e25	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Fun	LetDef2	True	Passed	Model Under Test Equivalent Model
d3177e02f5a042a54b0503fd48694ae53fd6c477	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Fun	LetDef2	False	Passed	Model Under Test Equivalent Model
060051e051a1527f0fa11c893cd669bc03917e86	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDef2	True	Passed	Model Under Test Equivalent Model
97c2f40e6f29a2cbee1f18aaf65ca015eab58d6b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDef2	False	Passed	Model Under Test Equivalent Model
d50864e15e6c8d1b43b534e226ceb2fe1f568826	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDef2	True	Passed	Model Under Test Equivalent Model
a88ae614a21ffea03d8f0f9a35b4f427e30d46fd	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDef2	False	Passed	Model Under Test Equivalent Model
6dc24a161919e3c6367b81e8180de9e21bdf7512	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Exists	LetDef2	True	Passed	Model Under Test Equivalent Model
da26503ee0a3e3acece8234314dc2bfbc931d9cf	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Exists	LetDef2	False	Passed	Model Under Test Equivalent Model
cca1b0aa9db540d87cb5e8d9a583e8b59bcc5abc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Forall	LetDef2	True	Passed	Model Under Test Equivalent Model
0bab078b9815bc3aabe61afafdce619c9473d684	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Forall	LetDef2	False	Passed	Model Under Test Equivalent Model
793d4e2761c9b7c5fd9605911985257cf1f94424	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Choose	LetDef2	True	Passed	Model Under Test Equivalent Model
b15c3b1cc85cfd3545678577725217b514241dc4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Choose	LetDef2	False	Passed	Model Under Test Equivalent Model
ed686bb4e242b53e7aa7dbb2d3ffa66339140916	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDef2	True	Passed	Model Under Test Equivalent Model
cb95f968d4911e327a0dec44c60f36041f599287	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDef2	False	Passed	Model Under Test Equivalent Model
95dea156b252b9360aa133693936c8260a8490ea	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDef2	True	Passed	Model Under Test Equivalent Model
1336301780c718aebf8dcde71936080affe4939c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDef2	False	Passed	Model Under Test Equivalent Model
2445b0206d353fd6f4571df7dacc55c208410626	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDef2	True	Passed	Model Under Test Equivalent Model
a5ee8321b587d2ff9e9cb57d53c6f8d2bcbd6971	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDef2	False	Passed	Model Under Test Equivalent Model
088868779c87bcc01f7568560593d6a703b680f1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDef2	True	Passed	Model Under Test Equivalent Model
ac57aff7c8c53e12d1c5457338bed7f19afae921	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDef2	False	Passed	Model Under Test Equivalent Model
753db5a2d36dc4611effcb284e2975b19f8b7c07	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDef2	True	Passed	Model Under Test Equivalent Model
fe4104148a794423935fd32225f7b3eca07c1584	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDef2	False	Passed	Model Under Test Equivalent Model
5f9dd3b34b42afce31b2bdc87bc9c529122cc790	TLC with reduction strategy: Case Feature: @ is reduced to F[arg] Plug Feature: LET definitions are reduced to global definitions	Except1FunWithAt	LetDef2	True	Passed	Model Under Test Equivalent Model
212a3d5306fecb9f3a507de8ed0319e562b93135	TLC with reduction strategy: Case Feature: @ is reduced to F[arg] Plug Feature: LET definitions are reduced to global definitions	Except1FunWithAt	LetDef2	False	Passed	Model Under Test Equivalent Model
5ce587ce48856f88826a831548ab56f3885008ac	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDef2	True	Passed	Model Under Test Equivalent Model
a7f127ee8a11ebcf219a2982732795297409a777	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDef2	False	Passed	Model Under Test Equivalent Model
fc71119f443134e6e0e3ad21347971b595a9ce12	TLC with reduction strategy: Case Feature: @ is reduced to F.arg Plug Feature: LET definitions are reduced to global definitions	Except1RecWithAt	LetDef2	True	Passed	Model Under Test Equivalent Model
d8aff8b4f2bd04369b92089cae7d547d5af17314	TLC with reduction strategy: Case Feature: @ is reduced to F.arg Plug Feature: LET definitions are reduced to global definitions	Except1RecWithAt	LetDef2	False	Passed	Model Under Test Equivalent Model
d41bc6eac38934bb0b03e4fee5b373ec50fd0075	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDef2	True	Passed	Model Under Test Equivalent Model
7eacc06275342fee4b820f742b2f867a58336d95	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDef2	False	Passed	Model Under Test Equivalent Model
4bcb4b651692e55fc1299784153358d800fc74c4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2FunTuple	LetDef2	True	Passed	Model Under Test Equivalent Model
ba5a96150ec84a551e28d54029f1363a8c5014d4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2FunTuple	LetDef2	False	Passed	Model Under Test Equivalent Model
7ab3e0875d14fc6a5480f7712bc449fa9d08498f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDef2	True	Passed	Model Under Test Equivalent Model
533e007df4e2e5b65e900f0175c83276e9addaa8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDef2	False	Passed	Model Under Test Equivalent Model
502d6ae83d782008c0dad5a2b61c3f858f2b6381	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumUnaryMinus	LetDef2	True	Passed	Model Under Test Equivalent Model
30cbf778dbdf1cc2e587c9205ea1080aa88b6abc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumUnaryMinus	LetDef2	False	Passed	Model Under Test Equivalent Model
e231b615912d00ae5e5c7a1467fa5f0a3a7f86e7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumPlus	LetDef2	True	Passed	Model Under Test Equivalent Model
baff624e3bda02c67ef275b56fc8f11530fe72d2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumPlus	LetDef2	False	Passed	Model Under Test Equivalent Model
cbb162da85a2b3713fc5a0a05c204ad518833a63	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMinus	LetDef2	True	Passed	Model Under Test Equivalent Model
6c9d3cd915e631fc3dfb9013bf83fdde5232114e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMinus	LetDef2	False	Passed	Model Under Test Equivalent Model
4de3583b7b03010925cdecc91f00abb087eb6b38	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMul	LetDef2	True	Passed	Model Under Test Equivalent Model
f7f2493f0039c9186333e08fc3f4cf790b28e0fb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMul	LetDef2	False	Passed	Model Under Test Equivalent Model
d1ea25466413046cee937a2888451d2c6d297d80	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumDiv	LetDef2	True	Passed	Model Under Test Equivalent Model
69805a519321f65146abd0af07bfd76e35bac901	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumDiv	LetDef2	False	Passed	Model Under Test Equivalent Model
644f6262f60684303ebfe552c274c5572430677a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMod	LetDef2	True	Passed	Model Under Test Equivalent Model
954b060df240851bc3270f1614d544edd5798ac7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMod	LetDef2	False	Passed	Model Under Test Equivalent Model
0b98ae80ff61c7a9a9aba4193687b661c1c4c07c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumPow	LetDef2	True	Passed	Model Under Test Equivalent Model
97cf06ae42d1ac9f924a786278a900e716688877	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumPow	LetDef2	False	Passed	Model Under Test Equivalent Model
8ed214e59ffca19e46ef65b2147ad18e8fc6a3bc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumGt	LetDef2	True	Passed	Model Under Test Equivalent Model
ad52368e315fd71105fc0079e6720958a7bdeea6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumGt	LetDef2	False	Passed	Model Under Test Equivalent Model
a009bb8e2afb0e5454fd585e8b55c92a884940c0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumGe	LetDef2	True	Passed	Model Under Test Equivalent Model
725633b96eca39b3d6b2c0b62cbcc76355c809f8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumGe	LetDef2	False	Passed	Model Under Test Equivalent Model
c0fab9ccb9f80039fcd45dcfae40353a80a3f7f7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumLt	LetDef2	True	Passed	Model Under Test Equivalent Model
f102511871f3500ea596c171f0514529113ed57a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumLt	LetDef2	False	Passed	Model Under Test Equivalent Model
89dc7b9cd50c37a7f0825fd3b67adbe1e3e78b6e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumLe	LetDef2	True	Passed	Model Under Test Equivalent Model
483b660f4e749d642ef0900ddc32897bb126c4a3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumLe	LetDef2	False	Passed	Model Under Test Equivalent Model
e1ccae3728c21d81705e06c24721c49ce7947731	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDef2	True	Passed	Model Under Test Equivalent Model
6a1155c5499b87d9a6cb333cfbad67d7ca365c02	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDef2	False	Passed	Model Under Test Equivalent Model
78aa4b28974675448e708a413f0e2f25a6edf8eb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDefFun	LetDef2	True	Passed	Model Under Test Equivalent Model
143ca82637fd318d7ffaefc995f4ba425eca91e9	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDefFun	LetDef2	False	Passed	Model Under Test Equivalent Model
1ca9b149a862a7e404931310e63677f457625e8a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDef2	True	Passed	Model Under Test Equivalent Model
f55bcc34a21fa98d0e35d710ac40f85d189f3b4e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDef2	False	Passed	Model Under Test Equivalent Model
6a716e31435de57d44f1e9b9e4da095d1eaa5cea	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	LetDef2	True	Passed	Model Under Test Equivalent Model
2c95782f8d7c9983af422c833a725220784ca2bf	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	LetDef2	False	Passed	Model Under Test Equivalent Model
13faef550f2d980679692da511cf219a9eea7ca6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDef2	True	Passed	Model Under Test Equivalent Model
5ba1f90100c2f699d31c5b5ed5ffe93000f77b12	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDef2	False	Passed	Model Under Test Equivalent Model
0254854f531d7d7390bd4ec24fe7e0240c519db9	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef0	LetDef2	True	Passed	Model Under Test Equivalent Model
1bc9eb825489ea59d31b4aed1c818384d68dcc4f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef0	LetDef2	False	Passed	Model Under Test Equivalent Model
15fd8352436b24c720fd1013bb5c41c379674161	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDef2	True	Passed	Model Under Test Equivalent Model
8a77ced032342bf9d979b7f3ded84c1c827b8d93	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDef2	False	Passed	Model Under Test Equivalent Model
5e1fbb024c2acd63747fd61b872b7bc55aee2620	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef1	LetDef2	True	Passed	Model Under Test Equivalent Model
b99cb7194223154ba878784da14ffa31cbb47108	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef1	LetDef2	False	Passed	Model Under Test Equivalent Model
47596f079f48816589345499ac8d3efc5f0c799c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDef2	True	Passed	Model Under Test Equivalent Model
97433d558057bdcf1b47e19f1cfdf3b841565f0e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDef2	False	Passed	Model Under Test Equivalent Model
994663dd468b92047f0fe0a0fadc55eddae4e9b2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef2	LetDef2	True	Passed	Model Under Test Equivalent Model
4596192ec69f6f3ca65c59272e3ad0ba0f7a8d48	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef2	LetDef2	False	Passed	Model Under Test Equivalent Model
b25133af006526c055b31d7fee4a400aca7124fb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDef2	True	Passed	Model Under Test Equivalent Model
65b889ce82a4cbbcb390272447b2a67a36644a6d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDef2	False	Passed	Model Under Test Equivalent Model
328e27fb12bf28cebb73f7ad3ad58bcebccb0fc3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef1Recursive	LetDef2	True	Passed	Model Under Test Equivalent Model
d98a3514eb62b4235f1908cb23df09e9023d4735	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef1Recursive	LetDef2	False	Passed	Model Under Test Equivalent Model
d598a7de186acdc73a558307f59cb1f8bd83dd49	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Extends	LetDef2	True	Passed	Model Under Test Equivalent Model
e8c0d3151a57b62238f0970ded4fa0e597a42467	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Extends	LetDef2	False	Passed	Model Under Test Equivalent Model
7ddaeb3c4e2a4248249d36cc107367ce4500bd6d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ExtendsInDifferentFolder	LetDef2	True	Passed	Model Under Test Equivalent Model
466f79eca76f1db640ea720dda68399e352a3fd3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ExtendsInDifferentFolder	LetDef2	False	Passed	Model Under Test Equivalent Model
c423316aeaf267d09fa52b90aff16923d43e2380	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Variable	LetDef2	True	Passed	Model Under Test Equivalent Model
01206232f86997c8a903bf70c2580737bd0a9aba	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Variable	LetDef2	False	Passed	Model Under Test Equivalent Model
d83deb23d7da0691595715d31632243b82cc633c	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior Plug Feature: LET definitions are reduced to global definitions	VariableViewExclude	LetDef2	True	Passed	Model Under Test Equivalent Model
4f2920d4598b8b8c85dfa40fcf52333ac33f3cdc	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior Plug Feature: LET definitions are reduced to global definitions	VariableViewExclude	LetDef2	False	Passed	Model Under Test Equivalent Model
447a0237d99b6c9743096f231a4f484acabebc7f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDef2	True	Passed	Model Under Test Equivalent Model
c0984d44e62aaf077f9c8087f5b39256e8fa3d45	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDef2	False	Passed	Model Under Test Equivalent Model
1295b666bb9ab78219106db4a15d68ce04203bf5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDef2	True	Passed	Model Under Test Equivalent Model
c80022b142a535abb9c793c0b978b09c6489ea3a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDef2	False	Passed	Model Under Test Equivalent Model
f87d582cd829fb27856ab750ef286b4239772d53	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDef2	True	Passed	Model Under Test Equivalent Model
c800cc358e23fc4c983efe9cb5914dcb2b978943	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDef2	False	Passed	Model Under Test Equivalent Model
4d1a91cf1f89ac20fe09519ef5e61064762998a4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDef2	True	Passed	Model Under Test Equivalent Model
d974fb153dd4d56bfc9386c6c4a325954d2cd2eb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDef2	False	Passed	Model Under Test Equivalent Model
c97248b17060d798a387e79a50baafb443a8b663	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamed	LetDef2	True	Passed	Model Under Test Equivalent Model
5d777618525a82ff7feb22eb671b57074f948f7e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamed	LetDef2	False	Passed	Model Under Test Equivalent Model
462c6cd99f26166cac56445434a4c6d45851f777	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedWith	LetDef2	True	Passed	Model Under Test Equivalent Model
47e641cd0bd90f400501006bc3572f23dec9f40b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedWith	LetDef2	False	Passed	Model Under Test Equivalent Model
9841c5438ae62b2148803dc0fb189b79d13f267a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceInFolder	LetDef2	True	Passed	Model Under Test Equivalent Model
7180b45f52c0252bf4457c23cda90391f1c6f21d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceInFolder	LetDef2	False	Passed	Model Under Test Equivalent Model
5d5292144f07addc15728c1928bb73b0e79d703a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWithInFolder	LetDef2	True	Passed	Model Under Test Equivalent Model
c7309ef8cc64e5b5a488e43922b9821eb9aecc97	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWithInFolder	LetDef2	False	Passed	Model Under Test Equivalent Model
34bd67d5c37e5518663ccb9798e6e1f920138bfe	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedInFolder	LetDef2	True	Passed	Model Under Test Equivalent Model
697529d7585d6bb89509beb82402a6e66caa780b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedInFolder	LetDef2	False	Passed	Model Under Test Equivalent Model
75a971de47e45e0832f277653375b9783505cd9a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedWithInFolder	LetDef2	True	Passed	Model Under Test Equivalent Model
bd649bf6cfd78fd61c45a6a1538726a512078bf8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedWithInFolder	LetDef2	False	Passed	Model Under Test Equivalent Model
45a577578362575b8272ca7c2386c47fd2cab11b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Enabled	LetDef2	True	Passed	Model Under Test Equivalent Model
49237d5a2fe8b0b2c9e97d2748ebd30031e3e2f3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Enabled	LetDef2	False	Passed	Model Under Test Equivalent Model
1e6f972dc5f0caabdc52840860a3c9e9f29005af	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Assume	LetDef2	True	Passed	Model Under Test Equivalent Model
e66657e0e2bb8f89c0d8d4b7493f3e0f5c6227a0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Assume	LetDef2	False	Passed	Model Under Test Equivalent Model
6bcd54cfa9f93f6fe6d3921507e7dc2f612e6c44	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AssumeNamed	LetDef2	True	Passed	Model Under Test Equivalent Model
64324ee2f52b72ddbe79774cb3339a9fcfab8846	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AssumeNamed	LetDef2	False	Passed	Model Under Test Equivalent Model
67c30e614e6e1a25207d190c0eddf02b363b8a3a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDef2	True	Passed	Model Under Test Equivalent Model
5147c313e07a72bbe05488fa41aa79ff32b8b417	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDef2	False	Passed	Model Under Test Equivalent Model
f979b94c12819dc05e4fc901c92b694ccfaeab91	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross2	LetDef2	True	Passed	Model Under Test Equivalent Model
575ec76e31f9ec80b42c361567bceca62e39a903	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross2	LetDef2	False	Passed	Model Under Test Equivalent Model
3f964cce3d44fc01d51c55206754772325222704	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross3	LetDef2	True	Passed	Model Under Test Equivalent Model
10f1fda32bfc1d2796b13bb8147c1a8b3643695b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross3	LetDef2	False	Passed	Model Under Test Equivalent Model
b536e19c558d9dcac18f427c348e443d526fde09	TLC with reduction strategy: Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R)) Plug Feature: LET definitions are reduced to global definitions	FunSet	LetDef2	True	Passed	Model Under Test Equivalent Model
cf3ade119c7513eec8a5812eb867c9cad8e80d01	TLC with reduction strategy: Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R)) Plug Feature: LET definitions are reduced to global definitions	FunSet	LetDef2	False	Passed	Model Under Test Equivalent Model
111206999af1169d203b2f28a97d4b1393d55780	TLC with reduction strategy: Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R) Plug Feature: LET definitions are reduced to global definitions	RecordSet	LetDef2	True	Passed	Model Under Test Equivalent Model
378f0a86c10217527ea3e55013e22a88c85f8d8f	TLC with reduction strategy: Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R) Plug Feature: LET definitions are reduced to global definitions	RecordSet	LetDef2	False	Passed	Model Under Test Equivalent Model
310e80f84a258c4c06c0b13f9a957b63d60f1b6c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetDiff	LetDef2	True	Passed	Model Under Test Equivalent Model
1431473e17542a1b2bb0483eb8443fe125f0d983	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetDiff	LetDef2	False	Passed	Model Under Test Equivalent Model
f63e83f175379f2ce897a9a3e9525b2e787932d0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetUnion	LetDef2	True	Passed	Model Under Test Equivalent Model
6468182e79a6cf3d7478207f256193a02e648119	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetUnion	LetDef2	False	Passed	Model Under Test Equivalent Model
1a4b919e89054378398c1ac4629ed753f511f7e9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetIntersect	LetDef2	True	Passed	Model Under Test Equivalent Model
40963758f7cbfc74631b8149a096a53e63a486a4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetIntersect	LetDef2	False	Passed	Model Under Test Equivalent Model
34811ce2021d3a94f297dd5a368555e0df2d80e7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SubsetEq	LetDef2	True	Passed	Model Under Test Equivalent Model
ebd9fdb1fb7a54b6c8c8fbb54652d3966aea7603	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SubsetEq	LetDef2	False	Passed	Model Under Test Equivalent Model
d0452484b226966eacfa104ffd8aa570a77cc90f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfCond	LetDef2	True	Passed	Model Under Test Equivalent Model
3571a3460b1528763744db4b45a8034057d2979c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfCond	LetDef2	False	Passed	Model Under Test Equivalent Model
fd54da8b0f55265f27d426774ba07f07dadcefb8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDef2	True	Passed	Model Under Test Equivalent Model
2d1fedb4989a6a95031224e45e979092f2a6fa97	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDef2	False	Passed	Model Under Test Equivalent Model
ffc15c8d56850594fdf6471988247bd8f0c81719	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDef2	True	Passed	Model Under Test Equivalent Model
7bec2e9299fdabc9171f915f4b0141d5977c7df8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDef2	False	Passed	Model Under Test Equivalent Model
789d9e542b350a9aa8eb69ae98e9d2a8fdfb2bbc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Subset	LetDef2	True	Passed	Model Under Test Equivalent Model
0490453d840a7c1570a088ade921f81b0556c5b9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Subset	LetDef2	False	Passed	Model Under Test Equivalent Model
52c38468b0b326ef4fdea013067d5d6332f880a2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDef2	True	Passed	Model Under Test Equivalent Model
b617f78dd91a5c33d1d19c1f63d5254498749857	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDef2	False	Passed	Model Under Test Equivalent Model
e1cda3bd33c36765651f11388ae43384ab4a0e2c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Union	LetDef2	True	Passed	Model Under Test Equivalent Model
ee1eac4d46ad07a84ae839ea9999375ccf9d827a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Union	LetDef2	False	Passed	Model Under Test Equivalent Model
675bbbd310c6af76dbeb029c8f05addfaf08e482	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDef2	True	Passed	Model Under Test Equivalent Model
f1085eb72b0ec0f2e1d28319a20af4f73f1b9b4b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDef2	False	Passed	Model Under Test Equivalent Model
e648e56250ad67687d758f3fd8dd4241ecf8056e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Equivalence	LetDef2	True	Passed	Model Under Test Equivalent Model
43e0c30d81a9f2239f05f817acfc6cbf296eb326	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Equivalence	LetDef2	False	Passed	Model Under Test Equivalent Model
0b585364ea756851d07fd5477bc754515e7eaefb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqLen	LetDef2	True	Passed	Model Under Test Equivalent Model
e63e682a81d492f22a4dff0ccbe355b90e6da4f1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqLen	LetDef2	False	Passed	Model Under Test Equivalent Model
7d6f625a5418187cb21008eaccea44acb99f124b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqConcat	LetDef2	True	Passed	Model Under Test Equivalent Model
4c6cace94af7987d28f16f0999d0fad8b7a54574	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqConcat	LetDef2	False	Passed	Model Under Test Equivalent Model
f7484f599561ba6ecf6973522f81230e0c2a2df9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSeq	LetDef2	True	Passed	Model Under Test Equivalent Model
0305249785aeed64a2f7a90e1d386d4b8870afbe	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSeq	LetDef2	False	Passed	Model Under Test Equivalent Model
33ccba424f2b69b99067db9e65f16db02e275738	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSelectSeq	LetDef2	True	Passed	Model Under Test Equivalent Model
9392eef8dde72aeb6e8500f4f13b256d7d610bd6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSelectSeq	LetDef2	False	Passed	Model Under Test Equivalent Model
c30b86d8f9fc9e8996adf1d7beb014a9f680127a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSubSeq	LetDef2	True	Passed	Model Under Test Equivalent Model
d5362ef550cacec3dce07db10feada68855e4ccc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSubSeq	LetDef2	False	Passed	Model Under Test Equivalent Model
99ea4f8b19db45aaeb2c5998d0178d94325d06cb	TLC with reduction strategy: Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review Plug Feature: LET definitions are reduced to global definitions	NumRange	LetDef2	True	Passed	Model Under Test Equivalent Model
0900e58012ecf4ef36ffff66bcd052a3940792a8	TLC with reduction strategy: Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review Plug Feature: LET definitions are reduced to global definitions	NumRange	LetDef2	False	Passed	Model Under Test Equivalent Model
c8dab2d39e4bc3600467fa4f1b128048ae2272b0	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y] Plug Feature: LET definitions are reduced to global definitions	TlcSingletonFun	LetDef2	True	Passed	Model Under Test Equivalent Model
2e294b8dadcbf077c1548945ad09c2bbfc18a4b1	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y] Plug Feature: LET definitions are reduced to global definitions	TlcSingletonFun	LetDef2	False	Passed	Model Under Test Equivalent Model
eb82b33e9b8b93238d29fc82f2632eebf79a1095	TLC with reduction strategy: Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g \|-> IF u \in DomF THEN f[u] ELSE g[x]] Plug Feature: LET definitions are reduced to global definitions	TlcExtendFun	LetDef2	True	Passed	Model Under Test Equivalent Model
a46b0536ef4c112c4e1a75fd348cf9a752391005	TLC with reduction strategy: Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g \|-> IF u \in DomF THEN f[u] ELSE g[x]] Plug Feature: LET definitions are reduced to global definitions	TlcExtendFun	LetDef2	False	Passed	Model Under Test Equivalent Model
295bb75a8b74e3782a916701077c2e23669af378	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S } Plug Feature: LET definitions are reduced to global definitions	TlcPermuteFun	LetDef2	True	Passed	Model Under Test Equivalent Model
ead54ae998624ec096bb30948423a9ed6001e0b4	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S } Plug Feature: LET definitions are reduced to global definitions	TlcPermuteFun	LetDef2	False	Passed	Model Under Test Equivalent Model
9c26201605bc4b4fb5781c8688177f6ed90fe313	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation Plug Feature: LET definitions are reduced to global definitions	TlcSortSeq	LetDef2	True	Passed	Model Under Test Equivalent Model
643d0c96efbc72951586ea144d2b1065ed2d52b7	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation Plug Feature: LET definitions are reduced to global definitions	TlcSortSeq	LetDef2	False	Passed	Model Under Test Equivalent Model
f3925e125b803ab599e43b56c5f0ee948c71be4f	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr Plug Feature: LET definitions are reduced to global definitions	TlcEval	LetDef2	True	Passed	Model Under Test Equivalent Model
6711318cb3e95d255643d8b2a357b65630eb9b4f	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr Plug Feature: LET definitions are reduced to global definitions	TlcEval	LetDef2	False	Passed	Model Under Test Equivalent Model
ff2afe1486b9e76068576852070bca5d2dac4c55	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagToSet	LetDef2	True	Passed	Model Under Test Equivalent Model
b5fe7193105f3a62a9daa85fa9ef6e6b2b906b0b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagToSet	LetDef2	False	Passed	Model Under Test Equivalent Model
1c89c99c3b2a55bbd05a328276c07c12a0c70188	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSetToBag	LetDef2	True	Passed	Model Under Test Equivalent Model
5143d1695ee2a90eb10004a619be52aea36b7b8c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSetToBag	LetDef2	False	Passed	Model Under Test Equivalent Model
bc5f87e179bec62cf45396044cd4f5d2130afb3c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagIn	LetDef2	True	Passed	Model Under Test Equivalent Model
1b40049e93063ae59c6e2b8537b0a5dd8201108b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagIn	LetDef2	False	Passed	Model Under Test Equivalent Model
889f222b22cc70a187e96ae13a60f9c4e8717105	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagAddBag	LetDef2	True	Passed	Model Under Test Equivalent Model
ae06f9efb2b68947c46124ce60b4f14e34853320	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagAddBag	LetDef2	False	Passed	Model Under Test Equivalent Model
8db7de91bdf2148c367466e6351ce5f4e0084e38	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagSub	LetDef2	True	Passed	Model Under Test Equivalent Model
417235db93f94391971535488c341cecb2650244	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagSub	LetDef2	False	Passed	Model Under Test Equivalent Model
3e06ab9afdb162a5e7276c37cc2befb0b3b957a5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagCopiesIn	LetDef2	True	Passed	Model Under Test Equivalent Model
adb63d78295f32cd9eacbae8e6410c94ee69eee6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagCopiesIn	LetDef2	False	Passed	Model Under Test Equivalent Model
f29b7083f5f4ba143e055419e3e55e988f33b241	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSubsetEqBag	LetDef2	True	Passed	Model Under Test Equivalent Model
c0f9ad7b44d7a18f1b48b2d5d163d93e0b188e57	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSubsetEqBag	LetDef2	False	Passed	Model Under Test Equivalent Model
8bfc065a633dfd55c0d6a3e3294803ae704f5de5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagUnion	LetDef2	True	Passed	Model Under Test Equivalent Model
91452d62181df9a2175c52f59d786c61ff6b9ff7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagUnion	LetDef2	False	Passed	Model Under Test Equivalent Model
28557e033654a594a1e34a15b3d386f99ebb6b63	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagCardinality	LetDef2	True	Passed	Model Under Test Equivalent Model
4ff477d76c0a2b0589786d2f6ee46e89b65524f4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagCardinality	LetDef2	False	Passed	Model Under Test Equivalent Model
05b0c36fef65016e05c2523a032bd6d2be7634d0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagOfAll	LetDef2	True	Passed	Model Under Test Equivalent Model
66064696d335ec057224c5bcc32a747d95fc0449	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagOfAll	LetDef2	False	Passed	Model Under Test Equivalent Model
7d0e7a73a067a4807f0683a4217ce5dfeff04267	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation Plug Feature: LET definitions are reduced to global definitions	BagSubBag	LetDef2	True	Passed	Model Under Test Equivalent Model
c7b0903eab88b51cf6a241b54a79708face847ca	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation Plug Feature: LET definitions are reduced to global definitions	BagSubBag	LetDef2	False	Passed	Model Under Test Equivalent Model
d907e2b8ae4f12e89f63c96e037166b9b920afb4	TLC with reduction strategy: Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types) Plug Feature: LET definitions are reduced to global definitions	FiniteSetsIsFiniteSet	LetDef2	True	Passed	Model Under Test Equivalent Model
bf023488dcebe223d9033e453556d27a6d83d498	TLC with reduction strategy: Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types) Plug Feature: LET definitions are reduced to global definitions	FiniteSetsIsFiniteSet	LetDef2	False	Passed	Model Under Test Equivalent Model
895bf62bbdf872cc874e0984b61568695fe3e442	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FiniteSetsCardinality	LetDef2	True	Passed	Model Under Test Equivalent Model
1d5c107a7ad0260407f04ab5353a3d4ab7bbea37	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FiniteSetsCardinality	LetDef2	False	Passed	Model Under Test Equivalent Model
765b138e3e3c4916b83488dc02cf77a04b9933d7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqHead	LetDef2	True	Passed	Model Under Test Equivalent Model
b58b3731180b2b69c057df914494e6dab0fafa63	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqHead	LetDef2	False	Passed	Model Under Test Equivalent Model
4f09f31500ce5b9c7b6e6180b235638c8d3079cb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqTail	LetDef2	True	Passed	Model Under Test Equivalent Model
d5692f28b7ecc2bc290e7c0dcbd192d01362d396	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqTail	LetDef2	False	Passed	Model Under Test Equivalent Model
18050490986a9670a188ba6d98e901c134eb37aa	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDef2	True	Passed	Model Under Test Equivalent Model
550a9998932a896a1314f7ba9a68bf200debb525	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDef2	False	Passed	Model Under Test Equivalent Model

Index

Tests by plug feature LetDef2; CLI Option: -workers 1