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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
319359e440920ffed360072356c758cbfb9f98f1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	And	LetDef1	True	Passed	Model Under Test Equivalent Model
b966d05c3bda35df438fc1b108621d4e36e5343d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	And	LetDef1	False	Passed	Model Under Test Equivalent Model
633fed5d29b3be919b3d46bb8605feb431adeeb2	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B) Plug Feature: LET definitions are reduced to global definitions	AndMultiLine	LetDef1	True	Passed	Model Under Test Equivalent Model
00716a25446ff30a78f4d168ffe1611163e31301	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B) Plug Feature: LET definitions are reduced to global definitions	AndMultiLine	LetDef1	False	Passed	Model Under Test Equivalent Model
3ddd944ba1ee738a481e115c73f7b72fabfc25f0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Imply	LetDef1	True	Passed	Model Under Test Equivalent Model
c6208e68d13ee715f2d9dde91f71862739a85542	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Imply	LetDef1	False	Passed	Model Under Test Equivalent Model
e36a830f4a480765c17bd1622b0193613a026e25	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Not	LetDef1	True	Passed	Model Under Test Equivalent Model
0ad72c74d4d91457766cce4b7ac7904dc13095b2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Not	LetDef1	False	Passed	Model Under Test Equivalent Model
f11c43e7d6eb9f93e35552d61aeaef137caf0cfc	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B) Plug Feature: LET definitions are reduced to global definitions	Or	LetDef1	True	Passed	Model Under Test Equivalent Model
41b817083dceb03cb77137659b085cc9070d0a32	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B) Plug Feature: LET definitions are reduced to global definitions	Or	LetDef1	False	Passed	Model Under Test Equivalent Model
1e33f0809ea7290bf7fda4f32c1bedc83f804bc0	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B) Plug Feature: LET definitions are reduced to global definitions	OrMultiLine	LetDef1	True	Passed	Model Under Test Equivalent Model
a6847a70fc5926d94b2e8d2c0914cac11abf246b	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B) Plug Feature: LET definitions are reduced to global definitions	OrMultiLine	LetDef1	False	Passed	Model Under Test Equivalent Model
45a2300b40f4774b742e40c685700bb0d2fea8a4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AndProp	LetDef1	True	Passed	Model Under Test Equivalent Model
317d0044ca8e181f8e1b6061779196b6925f36a1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AndProp	LetDef1	False	Passed	Model Under Test Equivalent Model
2ca77bd09110b995bca94957efa186b967580e2d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Boxed	LetDef1	True	Passed	Model Under Test Equivalent Model
b6fc1b610ec47a76ea2e4bbb396861382b5e9e58	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Boxed	LetDef1	False	Passed	Model Under Test Equivalent Model
1205d99ab8b8a541f0a224ac417d5cb15e66cbd1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDef1	True	Passed	Model Under Test Equivalent Model
e6e66626c0531dadbc2e225ee56ecdbfaca3e4bc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDef1	False	Passed	Model Under Test Equivalent Model
335490b55fb82f65ab888185140b6850ca420f26	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Ne	LetDef1	True	Passed	Model Under Test Equivalent Model
e8d3c816c2b64ee2f9b24de4c9847c46af0646d9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Ne	LetDef1	False	Passed	Model Under Test Equivalent Model
a1b4ea3f6997feffa65d5d11640a232f2e35cad3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Let	LetDef1	True	Passed	Model Under Test Equivalent Model
d4ce37d06c93cf88545692e9c613c88eec6b39b1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Let	LetDef1	False	Passed	Model Under Test Equivalent Model
31ec59b8f4c906c4058b6919f8fd23d21051e355	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDef1	True	Passed	Model Under Test Equivalent Model
08290c5068ef2902a68ac2a526386c558c329c04	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDef1	False	Passed	Model Under Test Equivalent Model
2eeba1c82ad649c11d51a31d561fcd831bda1bd6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDef1	True	Passed	Model Under Test Equivalent Model
a39c0edf9f6103e82548fd57ce4e61eda76ea6f3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDef1	False	Passed	Model Under Test Equivalent Model
7bed4d5db4ba24a4063f1bbb38bb2ea8463149a6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDef1	True	Passed	Model Under Test Equivalent Model
621e82f887dfca3f83a928c1105a53a4a33f8154	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDef1	False	Passed	Model Under Test Equivalent Model
d719bc8eb2431665127911ccc5d6f4814e480c19	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Fun	LetDef1	True	Passed	Model Under Test Equivalent Model
0a681a1a84151720ee5a3edc1dd0340c2baed198	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Fun	LetDef1	False	Passed	Model Under Test Equivalent Model
294ede688d022ffdabae95ab1413fe109f0d8e6f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDef1	True	Passed	Model Under Test Equivalent Model
2207fc879c727f673475d61da421bf2c522937c1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDef1	False	Passed	Model Under Test Equivalent Model
aaa2a2cb7db9d240effcc3761589c51c9f09f28d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDef1	True	Passed	Model Under Test Equivalent Model
e62aa61bc3971d4b82708bf2a49c2fb67ffd30f5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDef1	False	Passed	Model Under Test Equivalent Model
871331f1b4c05021ee31002982cb99034f20c1bf	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Exists	LetDef1	True	Passed	Model Under Test Equivalent Model
d04818f8a5dbb1d64b8b2db37ce11748dca4140a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Exists	LetDef1	False	Passed	Model Under Test Equivalent Model
0b524cd314a78b4cd9db72286ba6f25da4395b4e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Forall	LetDef1	True	Passed	Model Under Test Equivalent Model
02f995efa8406ee88bc8c50f1d03b633838e253d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Forall	LetDef1	False	Passed	Model Under Test Equivalent Model
35afb9f36506c3d3b580dcdafedc2ed4814db53d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Choose	LetDef1	True	Passed	Model Under Test Equivalent Model
da7e5163e3786b8d332a995cd4d2fcb0c94a051d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Choose	LetDef1	False	Passed	Model Under Test Equivalent Model
13b55413fb4513b027260db0b8624a18909a00d3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDef1	True	Passed	Model Under Test Equivalent Model
28e3fa34bdbdad2adf2b12ea96eda17fb46db2cd	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDef1	False	Passed	Model Under Test Equivalent Model
c8f59f222c310b299ad44b3c0a13b3134079e3c7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDef1	True	Passed	Model Under Test Equivalent Model
3687a099728547cad5d0cceb6f67fda76d67f3fe	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDef1	False	Passed	Model Under Test Equivalent Model
d74f5d067babee1d51ae438f72498b63cab42045	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDef1	True	Passed	Model Under Test Equivalent Model
ff26aa35219e2ed6d88c99efa49216d9a6f62018	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDef1	False	Passed	Model Under Test Equivalent Model
e0292360d4963cb696f053973d547bf59a07faae	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDef1	True	Passed	Model Under Test Equivalent Model
7adf5a99dcad19d01465ff3e55ecf9d4386d2d7d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDef1	False	Passed	Model Under Test Equivalent Model
c78af8afda30555fac2ce3b4e04c0b79e291af10	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDef1	True	Passed	Model Under Test Equivalent Model
a6a7769a534255e59a6c9b646115e7b64e2e5884	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDef1	False	Passed	Model Under Test Equivalent Model
bbd6b4d7d67b4ceb39c99de8012e4878d203a17b	TLC with reduction strategy: Case Feature: @ is reduced to F[arg] Plug Feature: LET definitions are reduced to global definitions	Except1FunWithAt	LetDef1	True	Passed	Model Under Test Equivalent Model
8a084669d7d580f080f6ed2af68d52b689a3c33a	TLC with reduction strategy: Case Feature: @ is reduced to F[arg] Plug Feature: LET definitions are reduced to global definitions	Except1FunWithAt	LetDef1	False	Passed	Model Under Test Equivalent Model
d38998780fe932cbf655427c41dfdd9aff21435c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDef1	True	Passed	Model Under Test Equivalent Model
3d0c4d9b6b80a14b1401d03cd4ea41d2e8a7aa74	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDef1	False	Passed	Model Under Test Equivalent Model
8cd91c092ba84bb004279c1dd41f946d3048d6b6	TLC with reduction strategy: Case Feature: @ is reduced to F.arg Plug Feature: LET definitions are reduced to global definitions	Except1RecWithAt	LetDef1	True	Passed	Model Under Test Equivalent Model
c490a32b6dd4eae042700c262f20a89ff4d128b0	TLC with reduction strategy: Case Feature: @ is reduced to F.arg Plug Feature: LET definitions are reduced to global definitions	Except1RecWithAt	LetDef1	False	Passed	Model Under Test Equivalent Model
c0f06be3fead67e4acdb14b37a518bc472a4cc06	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDef1	True	Passed	Model Under Test Equivalent Model
3c0dc8f885b0986fa4cfe2d62ba11e04af2ea948	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDef1	False	Passed	Model Under Test Equivalent Model
80299100a49d5c076782ef9f1666e46dfb705859	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2FunTuple	LetDef1	True	Passed	Model Under Test Equivalent Model
bc1d8a27001f47a14267d661341ba9b6f1f6244c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2FunTuple	LetDef1	False	Passed	Model Under Test Equivalent Model
5e162855345db9dc87842fbf70c6f89604513b3b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDef1	True	Passed	Model Under Test Equivalent Model
bd2efdfdb94a9239d81eab833b02df9cfab5e5b5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDef1	False	Passed	Model Under Test Equivalent Model
845c4ed1aeefee5c85abd8a95e770958934284c2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumUnaryMinus	LetDef1	True	Passed	Model Under Test Equivalent Model
c2a9fc4e2eaea706621e44e9970247fe28bd6a9e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumUnaryMinus	LetDef1	False	Passed	Model Under Test Equivalent Model
99b65f67aa2a23cc33c50d1f99327c97fe6b4dba	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumPlus	LetDef1	True	Passed	Model Under Test Equivalent Model
21a983a10a0b4ba3a720ca2a790e20001fc74baa	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumPlus	LetDef1	False	Passed	Model Under Test Equivalent Model
9b61cf2650b27dc2d314e81143ff890d03850bc1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMinus	LetDef1	True	Passed	Model Under Test Equivalent Model
edfe00cf6d5e32aff5eac576c7834cb6f7370816	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMinus	LetDef1	False	Passed	Model Under Test Equivalent Model
9118cd3825a29839686732c3f695b55c8a47ea28	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMul	LetDef1	True	Passed	Model Under Test Equivalent Model
cc09134c7d3207e32af75a02990aab08872db81d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMul	LetDef1	False	Passed	Model Under Test Equivalent Model
388e1596d1ab58b56f2cc3627c3ec661bb524db2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumDiv	LetDef1	True	Passed	Model Under Test Equivalent Model
4260fdd33dfb7a8e726d71fbfb6a3c57cdd641f7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumDiv	LetDef1	False	Passed	Model Under Test Equivalent Model
b34603ec4ef441addb25414363e2c53aed3fcc89	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMod	LetDef1	True	Passed	Model Under Test Equivalent Model
3e657d662b79655ac5f154edf63e72c7ec0d1517	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMod	LetDef1	False	Passed	Model Under Test Equivalent Model
fc555082c8d881edab4dc3105792df16c4dc2ed2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumPow	LetDef1	True	Passed	Model Under Test Equivalent Model
6f2290d0a446dc700e43fd9e6193c907d4832c2c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumPow	LetDef1	False	Passed	Model Under Test Equivalent Model
d09dce59924ba0393e3284dd641681f68daa68a4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumGt	LetDef1	True	Passed	Model Under Test Equivalent Model
ea89762a359510d72277603e026759ff4f9c353b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumGt	LetDef1	False	Passed	Model Under Test Equivalent Model
3eb6b1b7299aa6057482ab7ae4d8575f016c0b39	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumGe	LetDef1	True	Passed	Model Under Test Equivalent Model
b35bc25563af335776a415bbfb52e704fbb777b9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumGe	LetDef1	False	Passed	Model Under Test Equivalent Model
6f1433a3cfec4e6f9cef13aedac7b00b2aec49b4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumLt	LetDef1	True	Passed	Model Under Test Equivalent Model
57cdcff123a4d158828ff7db1d9503bc93f0ecc7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumLt	LetDef1	False	Passed	Model Under Test Equivalent Model
da28fdb00daac33292b890ff3c30f17fdb4f3ced	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumLe	LetDef1	True	Passed	Model Under Test Equivalent Model
1f5ebd37c8f1a62a919e06ce1c64f8058a284e76	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumLe	LetDef1	False	Passed	Model Under Test Equivalent Model
0274b30d711546e1ae445a396b5b401b32a810b4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDef1	True	Passed	Model Under Test Equivalent Model
99b034adf88bc44b0d77fe2e07c8d08f316ec779	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDef1	False	Passed	Model Under Test Equivalent Model
a54f1f4054b48366ecf41dceebc2cb844bfd6deb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDefFun	LetDef1	True	Passed	Model Under Test Equivalent Model
03eaf14a78384e6232bca6a5630cdceb059a66ac	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDefFun	LetDef1	False	Passed	Model Under Test Equivalent Model
90e03f1911c09c4b313f0efa9e4a7d7ee268a649	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDef1	True	Passed	Model Under Test Equivalent Model
de34ed620899af17222ccdff8958b9f615be8157	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDef1	False	Passed	Model Under Test Equivalent Model
a37c7b18849cbab802e58467f94f9c2a038c8630	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	LetDef1	True	Passed	Model Under Test Equivalent Model
9b19e03b9f880ba8129a93df21c640328a3375ff	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	LetDef1	False	Passed	Model Under Test Equivalent Model
9425a1b467aed7d4ae5c61bf5b208c8d84979ed0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDef1	True	Passed	Model Under Test Equivalent Model
4bba91890052d351429ba7de3ff74b34c66945d9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDef1	False	Passed	Model Under Test Equivalent Model
f28afb5c96845b022353df8aab4a6bf03b7aa720	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef0	LetDef1	True	Passed	Model Under Test Equivalent Model
5abf08f900b8840a42b8959c4ebe982df5c36571	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef0	LetDef1	False	Passed	Model Under Test Equivalent Model
39faccbae2b8b2f4c2ab966692deb1f835debcea	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDef1	True	Passed	Model Under Test Equivalent Model
6a9fe1337266e778d84903a4c7d43b8280de39f0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDef1	False	Passed	Model Under Test Equivalent Model
8d9dda7f61a8c2f80172ca08ad32617796abf4c4	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef1	LetDef1	True	Passed	Model Under Test Equivalent Model
bff47f74743bfbacb29da3890306e7214fa38ee0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef1	LetDef1	False	Passed	Model Under Test Equivalent Model
e2bd1b9761a99988f83db9a2e754a85cecf02b3a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDef1	True	Passed	Model Under Test Equivalent Model
2fd546bd9fbe1b9d5694946fb81b3b22eb16d778	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDef1	False	Passed	Model Under Test Equivalent Model
bfe7fabedd4cc290fa0748d0383757ef606aaf9f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef2	LetDef1	True	Passed	Model Under Test Equivalent Model
66e1ad43d716f9347594580764bc50d14e6e2e20	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef2	LetDef1	False	Passed	Model Under Test Equivalent Model
7ffa067b3f84c65ff7fddeebea936a265b717ac0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDef1	True	Passed	Model Under Test Equivalent Model
0c551240c23e8d14ba3ec9b19451db8be1d9e408	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDef1	False	Passed	Model Under Test Equivalent Model
9a64b5a921b9e44ca397d9d16719e19f8b5644f6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef1Recursive	LetDef1	True	Passed	Model Under Test Equivalent Model
8a609081ff574032d1ce1a3fa18784e4ff6bcb64	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef1Recursive	LetDef1	False	Passed	Model Under Test Equivalent Model
d8e0518f4570a7224c2f7ee3861423bb420b812b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Extends	LetDef1	True	Passed	Model Under Test Equivalent Model
6907d45a54563f248102ca20067a0c7b3ed4d2a4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Extends	LetDef1	False	Passed	Model Under Test Equivalent Model
0173113d7f007321c9f252e6deb1b90dfab8c536	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ExtendsInDifferentFolder	LetDef1	True	Passed	Model Under Test Equivalent Model
a7f4c160df59ec20fc43e1847e417c665c3259ba	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ExtendsInDifferentFolder	LetDef1	False	Passed	Model Under Test Equivalent Model
10ab602137f588864c9f8dc9ecbb657d63188029	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Variable	LetDef1	True	Passed	Model Under Test Equivalent Model
134184522745cb707cb29b3c2f078bf38e6a2a11	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Variable	LetDef1	False	Passed	Model Under Test Equivalent Model
94dc84af24e11426f330efcbfad901b85991af69	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	LetDef1	True	Passed	Model Under Test Equivalent Model
9ea350b8fcac291dc37963830f04989584edc946	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	LetDef1	False	Passed	Model Under Test Equivalent Model
e7fc62a85989456228632b620f80d2c12337a276	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDef1	True	Passed	Model Under Test Equivalent Model
08617236af09bdd829bddbd7b90fe9d806a89429	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDef1	False	Passed	Model Under Test Equivalent Model
412f369bed01a73e25eaf07ea26e77e8cc72ecf2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDef1	True	Passed	Model Under Test Equivalent Model
ab90fcb285b8d3cd351626fc3d2a12b8e44092e7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDef1	False	Passed	Model Under Test Equivalent Model
baf93e275fdcd9444fa6aefd2901ce312f9c0c9a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDef1	True	Passed	Model Under Test Equivalent Model
7b66a14838b1cc3d7572ed1bc4a274d3cbbd00a1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDef1	False	Passed	Model Under Test Equivalent Model
35c42eab027bc245b46c39701f42b9fd97c83798	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDef1	True	Passed	Model Under Test Equivalent Model
d018bf7a217dc481c0d3e2e3756e8e8f75e14fd4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDef1	False	Passed	Model Under Test Equivalent Model
f8d55722e728792421b426c9423354a522935305	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamed	LetDef1	True	Passed	Model Under Test Equivalent Model
162ab1b53a75c45b58c27c6c04ea93fea26af807	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamed	LetDef1	False	Passed	Model Under Test Equivalent Model
49711bc59bdefde897a514cfa538c3e479dfe185	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedWith	LetDef1	True	Passed	Model Under Test Equivalent Model
e86910417c3f5ac35e6683fea753c4aa04ea5e37	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedWith	LetDef1	False	Passed	Model Under Test Equivalent Model
7ff454255f046682e32dd17a0a61d95822a38a98	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceInFolder	LetDef1	True	Passed	Model Under Test Equivalent Model
6dfcc12fcc08fd59b882e74addd726a5c19e3375	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceInFolder	LetDef1	False	Passed	Model Under Test Equivalent Model
c74f5989a7d408cca9f4f85d119387791ace0cb5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWithInFolder	LetDef1	True	Passed	Model Under Test Equivalent Model
5d784d379ff7f239315f1e22d9d2250b989e5b1c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWithInFolder	LetDef1	False	Passed	Model Under Test Equivalent Model
255893671801c43580367dddca6771b7b424e873	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedInFolder	LetDef1	True	Passed	Model Under Test Equivalent Model
c7685e15900ddc2692c5ce5f26910c5f7562db71	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedInFolder	LetDef1	False	Passed	Model Under Test Equivalent Model
556d3e7c3d97df1766511fef5e718e2913727bd9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedWithInFolder	LetDef1	True	Passed	Model Under Test Equivalent Model
886d1c8a321eaaf918ff03f8fb342448567093d9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedWithInFolder	LetDef1	False	Passed	Model Under Test Equivalent Model
58081d0c306fc8dddf8ac3a1da0969b150bb58d1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Enabled	LetDef1	True	Passed	Model Under Test Equivalent Model
5c0b89971c0c5103d3df36695808168175d9b1c0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Enabled	LetDef1	False	Passed	Model Under Test Equivalent Model
9d6969fc073ffb0c68159847d4d390acd38ae5b7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Assume	LetDef1	True	Passed	Model Under Test Equivalent Model
5934eb707225d137375ea4259f3e0cd5d14fa896	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Assume	LetDef1	False	Passed	Model Under Test Equivalent Model
ac3af5f287ee3fc4547c0f6b9138d5b801a1b6a2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AssumeNamed	LetDef1	True	Passed	Model Under Test Equivalent Model
369f9709837936bed2a33b728c3320add847659d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AssumeNamed	LetDef1	False	Passed	Model Under Test Equivalent Model
30d02dc13d60f833ff4787c14c692e2346a9016d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDef1	True	Passed	Model Under Test Equivalent Model
fd1705e06244008c69077eb943a6b7e19464c71b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDef1	False	Passed	Model Under Test Equivalent Model
a83e230f49ed943588f0f606d6cbb1258a1c04bc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross2	LetDef1	True	Passed	Model Under Test Equivalent Model
d750e9bb675c702a405c97c1bb58e63edf027f13	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross2	LetDef1	False	Passed	Model Under Test Equivalent Model
b0e8e795aa23c5712260c22f7faba2ad91a89383	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross3	LetDef1	True	Passed	Model Under Test Equivalent Model
a9fa4ed9fa5e89e6548963028581bfa153272258	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross3	LetDef1	False	Passed	Model Under Test Equivalent Model
87ac5c59635a35a3b3cfd6bf637687e6a36c329f	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	LetDef1	True	Passed	Model Under Test Equivalent Model
25efbd94ff3a84ee5df32ee1e7054346554e0a6f	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	LetDef1	False	Passed	Model Under Test Equivalent Model
7dbff8fe8b9af7a307ea36d3fd24952127df3057	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	LetDef1	True	Passed	Model Under Test Equivalent Model
2a862c5725b035919fb03f48b206081989690ef8	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	LetDef1	False	Passed	Model Under Test Equivalent Model
e39cd9d712c0fad295c6fd6dacf15a8fc03fc669	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetDiff	LetDef1	True	Passed	Model Under Test Equivalent Model
5688d2458465e2431865ed267daac686ea20dcd9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetDiff	LetDef1	False	Passed	Model Under Test Equivalent Model
f12cc3dcc5d6677f783404c24cde411fd7dca71a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetUnion	LetDef1	True	Passed	Model Under Test Equivalent Model
cfa39744ac2266c752152e69a3fa37353c72465b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetUnion	LetDef1	False	Passed	Model Under Test Equivalent Model
c1a166f95d668c7bb2d368a7b322080b8f24d467	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetIntersect	LetDef1	True	Passed	Model Under Test Equivalent Model
7ffd55b89a39cddee168804980c17b97a48c4ec5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetIntersect	LetDef1	False	Passed	Model Under Test Equivalent Model
550c63bd7ae157229ba9346f954d013cf7895e0c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SubsetEq	LetDef1	True	Passed	Model Under Test Equivalent Model
98d32d5cc77d718e96aa04fcb5fe31931d6f0037	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SubsetEq	LetDef1	False	Passed	Model Under Test Equivalent Model
57361f7898b45560a542c126f986692d4ff3c521	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfCond	LetDef1	True	Passed	Model Under Test Equivalent Model
c1b01c24dec250fe4b57601f9e913ca758942327	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfCond	LetDef1	False	Passed	Model Under Test Equivalent Model
97c86da4afb118b03f244500832ebc276dcd20a3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDef1	True	Passed	Model Under Test Equivalent Model
1213239916f5db3d5fdd41ede4ad3a767fcbd2fe	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDef1	False	Passed	Model Under Test Equivalent Model
de9b718d282463b12ed14acb094d6fe0ddb94284	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDef1	True	Passed	Model Under Test Equivalent Model
97fa22bc8a0208e86c75a9eed03f9bcdb55cf6b0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDef1	False	Passed	Model Under Test Equivalent Model
0cf167e66d8be8704ecf077272d3184887bac661	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Subset	LetDef1	True	Passed	Model Under Test Equivalent Model
e6924791e52a6b323c95e9bd4d5f612d02032dc3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Subset	LetDef1	False	Passed	Model Under Test Equivalent Model
0fdafb56605289dafa4a68475c4a50593bd7756a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDef1	True	Passed	Model Under Test Equivalent Model
c083126530f268ea9079e9e754c38ab17c3cc935	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDef1	False	Passed	Model Under Test Equivalent Model
171376d307adb169f65436927dbdaf852f6671a1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Union	LetDef1	True	Passed	Model Under Test Equivalent Model
b4e790a52ce66e9c611177b6dc8ba4577cef4a02	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Union	LetDef1	False	Passed	Model Under Test Equivalent Model
6c3a098f026584f6efd43a44bf8a10cd76b26ae5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDef1	True	Passed	Model Under Test Equivalent Model
e778a12b440b57fe5e928e3a3cfbdad5e248a0cb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDef1	False	Passed	Model Under Test Equivalent Model
844b3f1c04f90f13d0174362c8a81dda50ec355c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Equivalence	LetDef1	True	Passed	Model Under Test Equivalent Model
98fb1c6788265a3810beff21260f2560f95d8282	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Equivalence	LetDef1	False	Passed	Model Under Test Equivalent Model
7a69be9a14d8c5495a3affac6319a5364d429136	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqLen	LetDef1	True	Passed	Model Under Test Equivalent Model
0cecefb77189b59c5fb1f74b95e5e725e8b2fd54	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqLen	LetDef1	False	Passed	Model Under Test Equivalent Model
044082a2ef91a5b06266f68ba17a28a47a94c4bc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqConcat	LetDef1	True	Passed	Model Under Test Equivalent Model
5c04a9b7c3296f72892f27828ea553c50f9c7b1f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqConcat	LetDef1	False	Passed	Model Under Test Equivalent Model
8f09fcd914fc1756c9585448476727987e62ca39	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSeq	LetDef1	True	Passed	Model Under Test Equivalent Model
e324d54e8c09146eebf15365032fab62c2b14214	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSeq	LetDef1	False	Passed	Model Under Test Equivalent Model
1c94fa36350c820bfb4efcc02862722fb0dc17a1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSelectSeq	LetDef1	True	Passed	Model Under Test Equivalent Model
865d4fc1708550ac379522e0337c18149cb390c7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSelectSeq	LetDef1	False	Passed	Model Under Test Equivalent Model
8fc67867d0120d3fa4fc5a60b062e23675bf3cdf	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSubSeq	LetDef1	True	Passed	Model Under Test Equivalent Model
59daa828ff800d116a5320d7690b62a915081ac0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSubSeq	LetDef1	False	Passed	Model Under Test Equivalent Model
fabdc1d5a2689cb52aaa7b8c35cd91fc7b732784	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	LetDef1	True	Passed	Model Under Test Equivalent Model
b6f5e078c3c23be70c2a33232eeede9ecd12a627	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	LetDef1	False	Passed	Model Under Test Equivalent Model
82be8a05672c277f36d728649703f47c434cc52b	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	LetDef1	True	Passed	Model Under Test Equivalent Model
8a41d1aa643a11cf2437abc9d470970c5c08d4ac	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	LetDef1	False	Passed	Model Under Test Equivalent Model
4348606bbc05ae5ed7ac1f85f74f35411cd247c7	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	LetDef1	True	Passed	Model Under Test Equivalent Model
17508a00b5e49f0784ae405198d063a5f3227b18	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	LetDef1	False	Passed	Model Under Test Equivalent Model
99f960e99c625a84d50a09210f40736b3e3fab35	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	LetDef1	True	Passed	Model Under Test Equivalent Model
919746ab78b100984ca5caebb6337ecc0591454f	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	LetDef1	False	Passed	Model Under Test Equivalent Model
20417412f9219d2c175d5ead31be47f30d34bcd0	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation Plug Feature: LET definitions are reduced to global definitions	TlcSortSeq	LetDef1	True	Passed	Model Under Test Equivalent Model
348d33d410fd1575d3712d440fa388426ccab1ae	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation Plug Feature: LET definitions are reduced to global definitions	TlcSortSeq	LetDef1	False	Passed	Model Under Test Equivalent Model
5a47b9df83e80e00b26453d3bc2e20698d7daf5a	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr Plug Feature: LET definitions are reduced to global definitions	TlcEval	LetDef1	True	Passed	Model Under Test Equivalent Model
f23bb62df2b1dbe284eebe91f2217e4a8b198db6	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr Plug Feature: LET definitions are reduced to global definitions	TlcEval	LetDef1	False	Passed	Model Under Test Equivalent Model
38f3b9043f1ffc7e7035e099670f8a68d870816b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagToSet	LetDef1	True	Passed	Model Under Test Equivalent Model
2a58454db8593a776f460c6ab4393e3ec154d649	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagToSet	LetDef1	False	Passed	Model Under Test Equivalent Model
296c2708619c16dba6db5d5cd8ea27bbc88af2c5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSetToBag	LetDef1	True	Passed	Model Under Test Equivalent Model
c78fb4c3290beb8b0f420297a447ed38a1a5d2e1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSetToBag	LetDef1	False	Passed	Model Under Test Equivalent Model
cdf344bcef999f7707abb199725963d67b9ee6fb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagIn	LetDef1	True	Passed	Model Under Test Equivalent Model
21521cc26d2a93d0b5d8c0438cfd1976d3c9dd82	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagIn	LetDef1	False	Passed	Model Under Test Equivalent Model
4fa6efb1656fa84c1a6cdab3f394b4baeacd8dfb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagAddBag	LetDef1	True	Passed	Model Under Test Equivalent Model
e8d8cf7e1b0eea7b8f3fb54fd699a1ddcfacdd2e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagAddBag	LetDef1	False	Passed	Model Under Test Equivalent Model
bb94a2017bb8b25a693550552f08e956dd60b6d6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagSub	LetDef1	True	Passed	Model Under Test Equivalent Model
e25a1cba8467f0e66c704655b2d57b2e4be6c5df	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagSub	LetDef1	False	Passed	Model Under Test Equivalent Model
82282a7e91569de6f9805d4d5ed41b85fbed37cd	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagCopiesIn	LetDef1	True	Passed	Model Under Test Equivalent Model
46f637d1d6c14d2493985f13a54d0e0850eafadb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagCopiesIn	LetDef1	False	Passed	Model Under Test Equivalent Model
4c2430aa63bb3bdd1842ed32ac7a2e607237c5de	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSubsetEqBag	LetDef1	True	Passed	Model Under Test Equivalent Model
1a16fba4d2ffd9b09264c9c08e4a898fa8248fed	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSubsetEqBag	LetDef1	False	Passed	Model Under Test Equivalent Model
418acd6091ac8b59bbb9ced38a0bc71b8da9ce90	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagUnion	LetDef1	True	Passed	Model Under Test Equivalent Model
783118e1fc70bdf1fa1ed31b0bb8c8995368a4f4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagUnion	LetDef1	False	Passed	Model Under Test Equivalent Model
d11c1f15d48f939f12cb1c0410ac41ebe9bdefd7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagCardinality	LetDef1	True	Passed	Model Under Test Equivalent Model
4eaeeb3cd7bee6c84acb2252ddb06ba67dcb3fa6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagCardinality	LetDef1	False	Passed	Model Under Test Equivalent Model
85f93657ecea967d3fafb810d541b1ebaa7d1e5e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagOfAll	LetDef1	True	Passed	Model Under Test Equivalent Model
c162b99b4e01197dd1b6169b93c516db9acbc156	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagOfAll	LetDef1	False	Passed	Model Under Test Equivalent Model
73e6a2cc7134b505c307db8699c0453ac294d1d0	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation Plug Feature: LET definitions are reduced to global definitions	BagSubBag	LetDef1	True	Passed	Model Under Test Equivalent Model
cf4d820778094113cb9bb62096bd59a5f955e65a	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation Plug Feature: LET definitions are reduced to global definitions	BagSubBag	LetDef1	False	Passed	Model Under Test Equivalent Model
c56c3ff81f1066debb54652b59b01273fac5edc1	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	LetDef1	True	Passed	Model Under Test Equivalent Model
cc21b40a98e782c35c3f2ed2d556e65b673acf01	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	LetDef1	False	Passed	Model Under Test Equivalent Model
bb8b7228fb7c1d7accfb6c0ec15b39f4e3d11f07	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FiniteSetsCardinality	LetDef1	True	Passed	Model Under Test Equivalent Model
4b5d1fb036fcc9ce33bb4ca40a8893b67191cf7b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FiniteSetsCardinality	LetDef1	False	Passed	Model Under Test Equivalent Model
74b82ce3cddb218c0198018cc37defbfaa53edb4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqHead	LetDef1	True	Passed	Model Under Test Equivalent Model
9f07b5264e97408efc06d250c1223987bab64af0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqHead	LetDef1	False	Passed	Model Under Test Equivalent Model
6b1870401c7cd0e9d9995211e478661f37f1adea	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqTail	LetDef1	True	Passed	Model Under Test Equivalent Model
6be3dbdcc8d03a35ae07496eb96bb6efac15f221	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqTail	LetDef1	False	Passed	Model Under Test Equivalent Model
423ed142123b4b909e0e5a17e89eedbcddfa0b66	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDef1	True	Passed	Model Under Test Equivalent Model
97487f60a8635f0256a2a3c60129f7e568c4686b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDef1	False	Passed	Model Under Test Equivalent Model

Index

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