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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
4f7ca26c505f244a121f61d8e78c58158cca531b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	And	LetDef0	True	Passed	Model Under Test Equivalent Model
f987a74cc4c995c1885872cda735527645ce625b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	And	LetDef0	False	Passed	Model Under Test Equivalent Model
c186db44c3ae108c196807ecb80e951552050b18	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B) Plug Feature: LET definitions are reduced to global definitions	AndMultiLine	LetDef0	True	Passed	Model Under Test Equivalent Model
1a42ab99f2855979882e5cdd67c5a200c8b101ac	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B) Plug Feature: LET definitions are reduced to global definitions	AndMultiLine	LetDef0	False	Passed	Model Under Test Equivalent Model
2c71034e132c870b1103eee631dbbabab7aa6df4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Imply	LetDef0	True	Passed	Model Under Test Equivalent Model
3dc06e9ef7100c4686b1cb038dbf659d9ed3040a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Imply	LetDef0	False	Passed	Model Under Test Equivalent Model
d42e22894b4538046f84d64ee841c11ad43aab04	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Not	LetDef0	True	Passed	Model Under Test Equivalent Model
9fbd8698755ce75ae30d3a75948b3af2c70bdf3c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Not	LetDef0	False	Passed	Model Under Test Equivalent Model
cc2627a54912af0af2bd28e8222592729c3ebaac	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B) Plug Feature: LET definitions are reduced to global definitions	Or	LetDef0	True	Passed	Model Under Test Equivalent Model
6e7ac9f7d923bd34ef17a6cf3a63a7ed2d7ccc91	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B) Plug Feature: LET definitions are reduced to global definitions	Or	LetDef0	False	Passed	Model Under Test Equivalent Model
3a20f62dc947b2a8815328a9e092cf1b1291eee3	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B) Plug Feature: LET definitions are reduced to global definitions	OrMultiLine	LetDef0	True	Passed	Model Under Test Equivalent Model
98dc6097adfa9de5b7e56fb1ef8f4ea5ee848656	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B) Plug Feature: LET definitions are reduced to global definitions	OrMultiLine	LetDef0	False	Passed	Model Under Test Equivalent Model
db5fbca5be5882372ce55486a83babf0442d8cea	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AndProp	LetDef0	True	Passed	Model Under Test Equivalent Model
5df6e902f80826156290c8fbd89564f75749cad2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AndProp	LetDef0	False	Passed	Model Under Test Equivalent Model
297e429514e63ac1cc3d96c79b2fce61f6ddb1a1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Boxed	LetDef0	True	Passed	Model Under Test Equivalent Model
f748ef89933ce74001770331e80c4cac10208706	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Boxed	LetDef0	False	Passed	Model Under Test Equivalent Model
cb18f7a10bbb44c2cdc6ba6aada9ed90ca5cc443	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDef0	True	Passed	Model Under Test Equivalent Model
f612a96a763d85f1a518c850ae3ea5c85b1bc126	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Eq	LetDef0	False	Passed	Model Under Test Equivalent Model
b3af95c5f4bf104b4224a7d9206a0dbdb5a03c1e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Ne	LetDef0	True	Passed	Model Under Test Equivalent Model
a9295de3697348fa931581b5463eaad11f18c07b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Ne	LetDef0	False	Passed	Model Under Test Equivalent Model
e3d3210278e3cabf3378f074cf17e506539ab120	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Let	LetDef0	True	Passed	Model Under Test Equivalent Model
3043cd522b14362d6482121d66d5463d8b265a5a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Let	LetDef0	False	Passed	Model Under Test Equivalent Model
45468fdfed6b98b96055a5be454ba816762cad49	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDef0	True	Passed	Model Under Test Equivalent Model
62071e37121b865eef32bb23d0ac3a4542522664	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set0	LetDef0	False	Passed	Model Under Test Equivalent Model
fc2b0625295e78aacf6476473394906012d0f212	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDef0	True	Passed	Model Under Test Equivalent Model
933b0119cd99260745750945d3b5fea56b865b06	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set1	LetDef0	False	Passed	Model Under Test Equivalent Model
4284dad668f13557a993e36d14e7c0d4ac65926e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDef0	True	Passed	Model Under Test Equivalent Model
ba007b696ed1161d9ddffeb373053df9b63de7f2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDef0	False	Passed	Model Under Test Equivalent Model
706ce10b8fae374b0b3581b8e4226b0fa45fff5a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Fun	LetDef0	True	Passed	Model Under Test Equivalent Model
d60b500f937d9a1e106cd85a01d1971e39696b75	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Fun	LetDef0	False	Passed	Model Under Test Equivalent Model
29c1792fc93e5ac3e54bebb8c213e5c60e3bbfa8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDef0	True	Passed	Model Under Test Equivalent Model
ec2a8e1875f4b36bfc5fbd207a350334b32f18b2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDef0	False	Passed	Model Under Test Equivalent Model
d65172931a2725909b6c90ed1a400f3b6994bdf4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDef0	True	Passed	Model Under Test Equivalent Model
3c905c70b79fec7077a322735bfffb6165d13a88	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NotIn	LetDef0	False	Passed	Model Under Test Equivalent Model
a6d584f4791c3566826ae3bd5237a136a1e0e342	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Exists	LetDef0	True	Passed	Model Under Test Equivalent Model
17a520bcf3cae1e08efcdc6348a49ceabb4d9e1a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Exists	LetDef0	False	Passed	Model Under Test Equivalent Model
66579749c168227a2f8e15642c332dc57e6482da	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Forall	LetDef0	True	Passed	Model Under Test Equivalent Model
a060af23843b0bfa40e9fdd6cddc538e03e6e368	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Forall	LetDef0	False	Passed	Model Under Test Equivalent Model
a0ecc9911ca733e59d4cd2dacf49c88d0be649c8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Choose	LetDef0	True	Passed	Model Under Test Equivalent Model
9619ce95d744020d8948a239105c66dc923a8b1c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Choose	LetDef0	False	Passed	Model Under Test Equivalent Model
03cc5cc13745bc542199ff6940a42b1660caa7c6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDef0	True	Passed	Model Under Test Equivalent Model
62117a7c70c72a2c52bd831705a314db9ae4fb11	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDef0	False	Passed	Model Under Test Equivalent Model
c89ad70f5909d1634a4858ccaf0f5e71d03eaa7c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDef0	True	Passed	Model Under Test Equivalent Model
7f645432c8f497ceec16e5709e7f57bb778eaaee	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Tuple	LetDef0	False	Passed	Model Under Test Equivalent Model
d398d33751cbea07cb84f3eb275f9f0db9a5c190	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDef0	True	Passed	Model Under Test Equivalent Model
f6b3656b47ce3d6d578cabda36e463466c543f12	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDef0	False	Passed	Model Under Test Equivalent Model
158f85b7278fa76eedb6c7e08d9bb6cf2839cb88	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDef0	True	Passed	Model Under Test Equivalent Model
89265aa11d8fd6432d29cd3c8bd50af6165302e9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDef0	False	Passed	Model Under Test Equivalent Model
01c1681a353010cd1aee76b668e3e3fd0b44fcb4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDef0	True	Passed	Model Under Test Equivalent Model
3444e9bac2ade5cadd40de792dee67455073e15f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Fun	LetDef0	False	Passed	Model Under Test Equivalent Model
7f96621b5f71ba11d382f8780f908f297546af76	TLC with reduction strategy: Case Feature: @ is reduced to F[arg] Plug Feature: LET definitions are reduced to global definitions	Except1FunWithAt	LetDef0	True	Passed	Model Under Test Equivalent Model
55a498c5bf3cdce3444ef7b50af7bc9edef566f9	TLC with reduction strategy: Case Feature: @ is reduced to F[arg] Plug Feature: LET definitions are reduced to global definitions	Except1FunWithAt	LetDef0	False	Passed	Model Under Test Equivalent Model
0b27128f5f24fb1b625f3a4de9cbe8c6547b476c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDef0	True	Passed	Model Under Test Equivalent Model
ab462e3df338d622b709e671645b4985e2b19019	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except1Rec	LetDef0	False	Passed	Model Under Test Equivalent Model
86721c093df02d1f8e753ee5cd73759ac82cabe3	TLC with reduction strategy: Case Feature: @ is reduced to F.arg Plug Feature: LET definitions are reduced to global definitions	Except1RecWithAt	LetDef0	True	Passed	Model Under Test Equivalent Model
2c4cab3022ee9b155fe43c3b05c7634f7600a32a	TLC with reduction strategy: Case Feature: @ is reduced to F.arg Plug Feature: LET definitions are reduced to global definitions	Except1RecWithAt	LetDef0	False	Passed	Model Under Test Equivalent Model
0c1efa83f9e4aba17d571376691e3ccad325d0a4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDef0	True	Passed	Model Under Test Equivalent Model
53c07ca194df393d09b2d6d66b11f29311b1383f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2Fun	LetDef0	False	Passed	Model Under Test Equivalent Model
a42455c2b8715e4cc59c97c31f0164c239c47c19	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2FunTuple	LetDef0	True	Passed	Model Under Test Equivalent Model
0dee49ca859225cb8e9d0af44e94fa03b6759a72	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except2FunTuple	LetDef0	False	Passed	Model Under Test Equivalent Model
d18c213cb18ab9bfbe4bb6f8a512a7686e085e32	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDef0	True	Passed	Model Under Test Equivalent Model
6da1169f1d44ff305bdfb40f916cfde3988ddbd9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDef0	False	Passed	Model Under Test Equivalent Model
410ed91e5b560e922f4fcf29af6bbf0648b0206e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumUnaryMinus	LetDef0	True	Passed	Model Under Test Equivalent Model
1644e7b9def651d2930306f8d2cb0c931979f97c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumUnaryMinus	LetDef0	False	Passed	Model Under Test Equivalent Model
936b684c06d7340b14d647c5e6f0c9c9737686d5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumPlus	LetDef0	True	Passed	Model Under Test Equivalent Model
7a43bf730e3740f2f34565d3fb875215f6b4961b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumPlus	LetDef0	False	Passed	Model Under Test Equivalent Model
b44507507f9ad3865a9a88e3d7e708f02082dda8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMinus	LetDef0	True	Passed	Model Under Test Equivalent Model
fd30e4c9770d30f0fcbd49319a60fde77fa5b45a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMinus	LetDef0	False	Passed	Model Under Test Equivalent Model
b7c1b97cd6ee146fb7cd285ae6d623e6b49c3c04	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMul	LetDef0	True	Passed	Model Under Test Equivalent Model
d4820897f63e588c072c0b2285ac3918c0d24ed4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMul	LetDef0	False	Passed	Model Under Test Equivalent Model
20dbde3afca9f166215c9f406a8c43e328c04df6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumDiv	LetDef0	True	Passed	Model Under Test Equivalent Model
551fedb5faf41c0702e7e1112dda6fcf076d0746	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumDiv	LetDef0	False	Passed	Model Under Test Equivalent Model
b2b8e2a3faa35c730e0d9af2e7a4579640202215	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMod	LetDef0	True	Passed	Model Under Test Equivalent Model
8b2535a4ba27f4c42badfb7d329695bfd3208f1a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumMod	LetDef0	False	Passed	Model Under Test Equivalent Model
5cb322f34b5ef0119d5056a8693277e479388879	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumPow	LetDef0	True	Passed	Model Under Test Equivalent Model
59f24b5eee2cbad24bc040b60e54032c2326aa03	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumPow	LetDef0	False	Passed	Model Under Test Equivalent Model
553d4582a39f0aa92f7c101cdaab0523c0ef1da1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumGt	LetDef0	True	Passed	Model Under Test Equivalent Model
2d5958b56f23e8c5ff49096aba5ab3a8c8ae6646	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumGt	LetDef0	False	Passed	Model Under Test Equivalent Model
9cf950fd7ef94e82d241ee8684e533af287094e5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumGe	LetDef0	True	Passed	Model Under Test Equivalent Model
91b21c0918b188c39383a609eba0ea9149d4ecb2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumGe	LetDef0	False	Passed	Model Under Test Equivalent Model
be5cc5bf9607f3a71e70dfafeca62c33ed95b312	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumLt	LetDef0	True	Passed	Model Under Test Equivalent Model
99396d738cf497415d8c1486417b34f06d29fa80	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumLt	LetDef0	False	Passed	Model Under Test Equivalent Model
34d4d768b0ed66111a7005de050bac80688710f1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumLe	LetDef0	True	Passed	Model Under Test Equivalent Model
a4effaa09826be6c24afc55953fb3efffdcec223	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	NumLe	LetDef0	False	Passed	Model Under Test Equivalent Model
77d2ff302fac7e73f0ff1a9cda9dba32ee719d7e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDef0	True	Passed	Model Under Test Equivalent Model
f3c532fa7919f4e53eff217da0fb8f465d5e0512	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFun	LetDef0	False	Passed	Model Under Test Equivalent Model
06f8e554595a52f3e6e88c1e3b8db59093e797db	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDefFun	LetDef0	True	Passed	Model Under Test Equivalent Model
66bbd3c0ff6461ed274b178719c76ba3d58e678c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDefFun	LetDef0	False	Passed	Model Under Test Equivalent Model
304a4e7e9bc8f6b176ebf8f37a644c8c72e4d882	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDef0	True	Passed	Model Under Test Equivalent Model
e8e7b392471478eb75c423e557b72d21cc2ff6ce	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDef0	False	Passed	Model Under Test Equivalent Model
02a2b5a44178ac4c68941fae50ed6a9351a202c5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	LetDef0	True	Passed	Model Under Test Equivalent Model
c1b25ac230bce711efdb2063005af94e3f42883e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	LetDef0	False	Passed	Model Under Test Equivalent Model
72976850c01bbda339cec6a05745db6f71a3cf7d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDef0	True	Passed	Model Under Test Equivalent Model
7c58658231cf7aee1fc87e451a8213a480883d26	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def0	LetDef0	False	Passed	Model Under Test Equivalent Model
6fa34718e9698df40031885bde641c27dc9b7410	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef0	LetDef0	True	Passed	Model Under Test Equivalent Model
dd3ed2ff5d879215f31c38170449c9241ef41f95	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef0	LetDef0	False	Passed	Model Under Test Equivalent Model
b16bff2e7eae1c1fdf242bcb65ec0eb30a01c458	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDef0	True	Passed	Model Under Test Equivalent Model
71422bf59e16f643180bb392713792c264045b0a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1	LetDef0	False	Passed	Model Under Test Equivalent Model
6b16de1082d98ecd3c79ba74d2f5e3f47a58ede6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef1	LetDef0	True	Passed	Model Under Test Equivalent Model
c04403256589af8c489f6f99c5b48b83f6b26549	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef1	LetDef0	False	Passed	Model Under Test Equivalent Model
e150b1994b29261eb5a26753c27a382e6a320f1c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDef0	True	Passed	Model Under Test Equivalent Model
e6c8c03fbd4eedec04de3fb16c449d310530d726	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def2	LetDef0	False	Passed	Model Under Test Equivalent Model
02c4a584b382523fad0b5c61d44ae12a27062789	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef2	LetDef0	True	Passed	Model Under Test Equivalent Model
5e91c605dd56dd8a4d04ccb5f8512d0a47ea11e5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef2	LetDef0	False	Passed	Model Under Test Equivalent Model
e8d6f9a02a56258740b89cbec859ce25d4fabccd	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDef0	True	Passed	Model Under Test Equivalent Model
eb073ed5399e2478d26c683bcb83eadfb4d9d9dd	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Def1Recursive	LetDef0	False	Passed	Model Under Test Equivalent Model
7b4d4033c17326a4a9cd5a669e765fe901dabd5d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef1Recursive	LetDef0	True	Passed	Model Under Test Equivalent Model
3eb7488e93ecfdeedd03b70afa78ba27fe3ba308	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions Plug Feature: LET definitions are reduced to global definitions	LetDef1Recursive	LetDef0	False	Passed	Model Under Test Equivalent Model
3bf8083574989ee37a54d29b73855352df2dbe06	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Extends	LetDef0	True	Passed	Model Under Test Equivalent Model
49f7d963bd5f64ee0c424b035832f8f052a9604d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Extends	LetDef0	False	Passed	Model Under Test Equivalent Model
8bc8f9a22e3302ba03e0a88934b4be19f4c8cad9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ExtendsInDifferentFolder	LetDef0	True	Passed	Model Under Test Equivalent Model
89edb21aa6d41b12d836db3bfcc5b7a791e4bf6f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ExtendsInDifferentFolder	LetDef0	False	Passed	Model Under Test Equivalent Model
1b7a0df2533bcf8eba8fd3d57e64c4d9c9793900	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Variable	LetDef0	True	Passed	Model Under Test Equivalent Model
d490fb003ce13c15ed501ab51a9d97962051facf	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Variable	LetDef0	False	Passed	Model Under Test Equivalent Model
88d082aac06e05e1d8b34be01a39cfae8d9a4a30	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	LetDef0	True	Passed	Model Under Test Equivalent Model
a8a5268351751b4b232b7649b6d91f5c869d38c4	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	LetDef0	False	Passed	Model Under Test Equivalent Model
6ba58c20f166d9b2c946223984fe932016a357fb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDef0	True	Passed	Model Under Test Equivalent Model
c19c025189ae862b7c254dc1ee3976ed12d48294	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Constant	LetDef0	False	Passed	Model Under Test Equivalent Model
220460d8e45dee139fa24fbf3fbe1cd377d721b6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDef0	True	Passed	Model Under Test Equivalent Model
ffaa1f761799b1e3d88446e34b95907e0de52cc4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	ConstantRank1	LetDef0	False	Passed	Model Under Test Equivalent Model
cde00abb4446a66f16e12f2d102294744d99baae	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDef0	True	Passed	Model Under Test Equivalent Model
b12154522d052bf8787f41005f9d63688c4dfe9a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Instance	LetDef0	False	Passed	Model Under Test Equivalent Model
f217c4e4c6b8cefd3f90c619057c9e9654404ca3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDef0	True	Passed	Model Under Test Equivalent Model
a3f59d2d3b4a2954492a79b948c433f63e45593a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWith	LetDef0	False	Passed	Model Under Test Equivalent Model
9762d19d11a67f40883afa59d5f3e1cbb94c5ee5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamed	LetDef0	True	Passed	Model Under Test Equivalent Model
a1cade250705791c04a779e7e1de9a6e35e8d71a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamed	LetDef0	False	Passed	Model Under Test Equivalent Model
35a9360c08d27f327121eb0954f08c2510603e98	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedWith	LetDef0	True	Passed	Model Under Test Equivalent Model
639227a5fdd37a662b9aa661bd8beebc9981c753	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedWith	LetDef0	False	Passed	Model Under Test Equivalent Model
dbbd5aa455dd3113658a1f840f6a9f63bd66058a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceInFolder	LetDef0	True	Passed	Model Under Test Equivalent Model
0d861eacdc50e3f6737ed7bb2d39dcd94128182b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceInFolder	LetDef0	False	Passed	Model Under Test Equivalent Model
3acb384344aa20cf963493caa7dc072ebc0b669e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWithInFolder	LetDef0	True	Passed	Model Under Test Equivalent Model
d9214530ce35b2a62cb7314fc2c52885d50afc03	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceWithInFolder	LetDef0	False	Passed	Model Under Test Equivalent Model
b36bfae187548a910596a2c971e53278310759df	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedInFolder	LetDef0	True	Passed	Model Under Test Equivalent Model
8802b55472e17885d45d880c928dff1234b984ab	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedInFolder	LetDef0	False	Passed	Model Under Test Equivalent Model
0ea164dfc6ec94d31d1dcadb0c6c9741377b37b5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedWithInFolder	LetDef0	True	Passed	Model Under Test Equivalent Model
05f76cb89ff613ff0a161a38658723798af6d842	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	InstanceNamedWithInFolder	LetDef0	False	Passed	Model Under Test Equivalent Model
1e81a9752e0daf4a2841354fde3e187796030d9e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Enabled	LetDef0	True	Passed	Model Under Test Equivalent Model
01ca6d6a9960fbd01ab087d9ca612c9958b3f948	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Enabled	LetDef0	False	Passed	Model Under Test Equivalent Model
077311c1999faa37a5cf410cc1ed5c817ee48662	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Assume	LetDef0	True	Passed	Model Under Test Equivalent Model
b42a31ebb559dde38e55a797362070a58b1bb126	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Assume	LetDef0	False	Passed	Model Under Test Equivalent Model
f5cf721e742158b9fba23747a0b568a34410f558	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AssumeNamed	LetDef0	True	Passed	Model Under Test Equivalent Model
157dfee18841817b68d664419e593d1f99c9fa71	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	AssumeNamed	LetDef0	False	Passed	Model Under Test Equivalent Model
9922d82ea7173e762e2e989afe0807ba64d03c95	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDef0	True	Passed	Model Under Test Equivalent Model
e01f86a296d09584b56d0ed8c080a09602c86549	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDef0	False	Passed	Model Under Test Equivalent Model
1b444e9e63ca0ed6493929688da2bbc7ddd4758e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross2	LetDef0	True	Passed	Model Under Test Equivalent Model
8d7da18b66497590c1a14af59ca6f950cd27057f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross2	LetDef0	False	Passed	Model Under Test Equivalent Model
a09cd86200e827d7ddc76d833a45097f20263a89	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross3	LetDef0	True	Passed	Model Under Test Equivalent Model
e64746f571ae74839e0a10517c7987fecccec53d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Cross3	LetDef0	False	Passed	Model Under Test Equivalent Model
268f43ab80cf217d4c5edcad3e603b69bfaebe69	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	LetDef0	True	Passed	Model Under Test Equivalent Model
0540723223eac3c8371093cfe65e0762a89dc861	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	LetDef0	False	Passed	Model Under Test Equivalent Model
89df8873fcd7def05debff7491306f42038faeca	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	LetDef0	True	Passed	Model Under Test Equivalent Model
712b341ba91960177a675eeb733b4248866de78a	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	LetDef0	False	Passed	Model Under Test Equivalent Model
687a57397018fade20b90a617e951ca36fbfa00a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetDiff	LetDef0	True	Passed	Model Under Test Equivalent Model
31b936798ab75817a8b7a8895e9dfbed3d0375cf	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetDiff	LetDef0	False	Passed	Model Under Test Equivalent Model
2c90c185aff54a254102e6804fc668a604acaf0c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetUnion	LetDef0	True	Passed	Model Under Test Equivalent Model
794ad744ff8a682b90465d002f9bc8a86106bb0c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetUnion	LetDef0	False	Passed	Model Under Test Equivalent Model
43eb5a13725b28d5246d448eb03e8479b5adf135	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetIntersect	LetDef0	True	Passed	Model Under Test Equivalent Model
b60f5a2310ddfcd7e907cc00e86ee69d3fea2ef3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SetIntersect	LetDef0	False	Passed	Model Under Test Equivalent Model
e992552ed10a4be0693ff3dd9400272ab53868e3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SubsetEq	LetDef0	True	Passed	Model Under Test Equivalent Model
0c16198ae48dec71693500ee14452644a281507a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SubsetEq	LetDef0	False	Passed	Model Under Test Equivalent Model
76d04b2905fb69b65d9bc491c462cb1829cc0876	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfCond	LetDef0	True	Passed	Model Under Test Equivalent Model
3226cb4e0bca038c2bb8ac5ef3045b70ce34ae32	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfCond	LetDef0	False	Passed	Model Under Test Equivalent Model
70320147be06b5bd5c41606615373503d917d5db	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDef0	True	Passed	Model Under Test Equivalent Model
67a398e4ecab0d5af4e90facdac50b1886072ce8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfThen	LetDef0	False	Passed	Model Under Test Equivalent Model
5dfd8b147ef8248197ae7b86bda8650c6e626d40	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDef0	True	Passed	Model Under Test Equivalent Model
e0f0e09792fc022039e66f49574f714a167decf9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	IfElse	LetDef0	False	Passed	Model Under Test Equivalent Model
2e769c061a72501e203b6d534278e775bc10ca52	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Subset	LetDef0	True	Passed	Model Under Test Equivalent Model
b06810b75c7d8df84568df2cb78458cf70c4e9fa	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Subset	LetDef0	False	Passed	Model Under Test Equivalent Model
69dc0045e5cb063274ab0af61993117f4f9a4627	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDef0	True	Passed	Model Under Test Equivalent Model
49040e40ee967f4f32675368146b632e4f26aeb4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDef0	False	Passed	Model Under Test Equivalent Model
c621815596eb791e3719529ee05498e5338d4cdc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Union	LetDef0	True	Passed	Model Under Test Equivalent Model
5221ee1ee658157cf35c3688c14082eb63692982	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Union	LetDef0	False	Passed	Model Under Test Equivalent Model
36fc78817411522e3967925f5371c6bf1e08604c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDef0	True	Passed	Model Under Test Equivalent Model
f419f75565a4fffca9749f6c1d9d7e23ba140ec7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Unchanged	LetDef0	False	Passed	Model Under Test Equivalent Model
9a9242a0849a01b72e948d5ba5841276ba7321dc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Equivalence	LetDef0	True	Passed	Model Under Test Equivalent Model
1f59d407d6dd1ec140d459b021ba687703395e57	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Equivalence	LetDef0	False	Passed	Model Under Test Equivalent Model
183c4f8d8ea4e771b454fee0bdd6107e4c6beee0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqLen	LetDef0	True	Passed	Model Under Test Equivalent Model
23e0b63acd2c920e6552dc427ff7441ad98d9071	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqLen	LetDef0	False	Passed	Model Under Test Equivalent Model
7378bdb8410120a56d76ae16ec74fcd9e41ea391	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqConcat	LetDef0	True	Passed	Model Under Test Equivalent Model
93a751e55e8b21ff966cfe56dedf75bbcd1b6b57	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqConcat	LetDef0	False	Passed	Model Under Test Equivalent Model
dcf34520e8eab4094332194615a3a1224523f686	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSeq	LetDef0	True	Passed	Model Under Test Equivalent Model
2ca9b0d3fd8a0c8aeebb6a16275ca9ede96118b5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSeq	LetDef0	False	Passed	Model Under Test Equivalent Model
da646df2eac0ecf0f3b2f4d5e70f4b02ff2c6f5a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSelectSeq	LetDef0	True	Passed	Model Under Test Equivalent Model
ddd7d53f8af3c3fe4740084e7a51bfc384891ffb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSelectSeq	LetDef0	False	Passed	Model Under Test Equivalent Model
d93b1e15b4febeccaaaceb1c58c33899f5e96053	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSubSeq	LetDef0	True	Passed	Model Under Test Equivalent Model
7b8bded5feb7525b85f09a92fb8195153ea255fd	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSubSeq	LetDef0	False	Passed	Model Under Test Equivalent Model
ccf8cd5e78d8072423c172dab66d48513fd4ed6f	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	LetDef0	True	Passed	Model Under Test Equivalent Model
2c9d27907897e8de1ffb41ec7711ad0518487588	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	LetDef0	False	Passed	Model Under Test Equivalent Model
7126b5f34183bdcbeb98805f15a3f4fe579dec09	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	LetDef0	True	Passed	Model Under Test Equivalent Model
dc97071356a6ee4dca52130d5e557f4ebb6911cc	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	LetDef0	False	Passed	Model Under Test Equivalent Model
c9fba643e410fa824c96263c9f5c7711af84b413	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	LetDef0	True	Passed	Model Under Test Equivalent Model
e568ce79f8915c60f821496ed6be343450da226b	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	LetDef0	False	Passed	Model Under Test Equivalent Model
8286112fa5cb033a55aea17520b429b4a013c9c1	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	LetDef0	True	Passed	Model Under Test Equivalent Model
a5a6bb6546ddb57ee4320482f02bd2f88989ffbd	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	LetDef0	False	Passed	Model Under Test Equivalent Model
7665ad68d5505a0edff5f032d297816b25bcca8d	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation Plug Feature: LET definitions are reduced to global definitions	TlcSortSeq	LetDef0	True	Passed	Model Under Test Equivalent Model
fead12dad7b0a0ac7a671a6aedaf8507776e1ab3	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation Plug Feature: LET definitions are reduced to global definitions	TlcSortSeq	LetDef0	False	Passed	Model Under Test Equivalent Model
8a063ba0f15c347573e871efec8cf3ae43eeaca8	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr Plug Feature: LET definitions are reduced to global definitions	TlcEval	LetDef0	True	Passed	Model Under Test Equivalent Model
8926a21adc570c61365050605e36f963deac172e	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr Plug Feature: LET definitions are reduced to global definitions	TlcEval	LetDef0	False	Passed	Model Under Test Equivalent Model
10687f28bd857a5f1e615fab7887cfc9b09d162c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagToSet	LetDef0	True	Passed	Model Under Test Equivalent Model
62767b2b3fddd2049fa37bb83dff67675ebd114f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagToSet	LetDef0	False	Passed	Model Under Test Equivalent Model
a2dd31f0e0ee087f036f5100e50d49f54cdad39b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSetToBag	LetDef0	True	Passed	Model Under Test Equivalent Model
3f6dde82a71a35a2cffd852b9d692ed67a29cfc1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSetToBag	LetDef0	False	Passed	Model Under Test Equivalent Model
99c0885221a34db80353dc044702a99b6bb9be83	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagIn	LetDef0	True	Passed	Model Under Test Equivalent Model
55f386bb1d78e673eb4bf1acd7e73a8e615fcbc0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagIn	LetDef0	False	Passed	Model Under Test Equivalent Model
62b84c8886c11060a2cc35a98039271c95cd81df	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagAddBag	LetDef0	True	Passed	Model Under Test Equivalent Model
1cfd998aeae44ccea5ca9437b48c4556ce33e17b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagAddBag	LetDef0	False	Passed	Model Under Test Equivalent Model
909c4c22b62c7bbc2f3c26b12775204122ba7d76	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagSub	LetDef0	True	Passed	Model Under Test Equivalent Model
79f5f0ff4be18c08d6253fdb6ed98c5f5ed37cdc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagSub	LetDef0	False	Passed	Model Under Test Equivalent Model
ec8a1b540ccf3add5894a120777f6b36f5b362f0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagCopiesIn	LetDef0	True	Passed	Model Under Test Equivalent Model
d60e267dee738dc3dd46e84967ea831e2526dd55	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagCopiesIn	LetDef0	False	Passed	Model Under Test Equivalent Model
261d7cef2301c6af623b9fca5cbb5d007b011062	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSubsetEqBag	LetDef0	True	Passed	Model Under Test Equivalent Model
632efc756a64f5b84a0e512a0c62fdcdcd683419	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagSubsetEqBag	LetDef0	False	Passed	Model Under Test Equivalent Model
98233bb172043e221edec76b18ab044d3969d651	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagUnion	LetDef0	True	Passed	Model Under Test Equivalent Model
9e7c41dae8536e1b7d4aed03d3fcec0e21b66200	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagUnion	LetDef0	False	Passed	Model Under Test Equivalent Model
59994fe93332f162ad3a68592596fd7c5c914234	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagCardinality	LetDef0	True	Passed	Model Under Test Equivalent Model
9b7ef6ee85d5a58b29f97cabe14c0013e1d6eaf6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagCardinality	LetDef0	False	Passed	Model Under Test Equivalent Model
d167f59167505ae02918c9584134ef6be49fa59d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagOfAll	LetDef0	True	Passed	Model Under Test Equivalent Model
cf09e0ceac0cf69aaddc66b1deb97c03d24e0585	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	BagBagOfAll	LetDef0	False	Passed	Model Under Test Equivalent Model
d45d3088346380456a6d6eda83e19e8f07fd9637	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation Plug Feature: LET definitions are reduced to global definitions	BagSubBag	LetDef0	True	Passed	Model Under Test Equivalent Model
82edad8fd51cead3c57221751a99e3e6b82ae02a	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation Plug Feature: LET definitions are reduced to global definitions	BagSubBag	LetDef0	False	Passed	Model Under Test Equivalent Model
6d2f7778acb875228a89b76fc3738dd9d323d6f9	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	LetDef0	True	Passed	Model Under Test Equivalent Model
fff93bdcc3888176fb291272e9a55d839d2eb574	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	LetDef0	False	Passed	Model Under Test Equivalent Model
6d0da67d01725514e0a1e2ef4f988df2634d56f4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FiniteSetsCardinality	LetDef0	True	Passed	Model Under Test Equivalent Model
fd0ab26042f150ebf5e4754fe8274ce0fe6a4048	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FiniteSetsCardinality	LetDef0	False	Passed	Model Under Test Equivalent Model
7a854ce0f13483c6fb8ce84104587d394d65271c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqHead	LetDef0	True	Passed	Model Under Test Equivalent Model
2b83de403fff2e3942b6443bb91acb552771c8d2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqHead	LetDef0	False	Passed	Model Under Test Equivalent Model
416df4a48f7ffca450c137c62bccbfffea40c9a1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqTail	LetDef0	True	Passed	Model Under Test Equivalent Model
7831ff9c37b93cdec6517f8ebd3f6ba69d17300e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqTail	LetDef0	False	Passed	Model Under Test Equivalent Model
b7d8da2b5a75b6f984f432a685fa9803696ea596	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDef0	True	Passed	Model Under Test Equivalent Model
3c0af8b97444caaf4f1a1eb1d0a2a73bc9ca9a95	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDef0	False	Passed	Model Under Test Equivalent Model

Index

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