Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
18ec875dd06d22999ec14de7fcc6df066b485933 TLC with reduction strategy:
  • Plug 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)
Eq RecordSet True Passed
a477c4a747bd062c524b47bfb9b8cf4a6714d21b TLC with reduction strategy:
  • Plug 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)
Eq RecordSet False Passed
9ef76e38748c9bfa7e14addbcbbc153bc3d96f46 TLC with reduction strategy:
  • Plug 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)
Ne RecordSet True Passed
1cf3fa1314dcd04c1c86b87d6e8f6726632cb516 TLC with reduction strategy:
  • Plug 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)
Ne RecordSet False Passed
322b21d2a3fb0e99c8fc3e4793c7a8a98cf75239 TLC with reduction strategy:
  • Plug 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)
Let RecordSet True Passed
df5a0b923cb7a1bf20dd134df23c4859fd9dfffb TLC with reduction strategy:
  • Plug 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)
Let RecordSet False Passed
9aafae2107f57479d4adf06c404082f0ee7d9efc TLC with reduction strategy:
  • Plug 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)
Set0 RecordSet True Passed
c4ff4f894d8d55c3b06c1661415528a0c25dd397 TLC with reduction strategy:
  • Plug 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)
Set0 RecordSet False Passed
4ea6ba9060a25a11a1255be4fa3886842e531c81 TLC with reduction strategy:
  • Plug 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)
Set1 RecordSet True Passed
4abb7310c9fbb4577312582387fe55f3368ff9cc TLC with reduction strategy:
  • Plug 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)
Set1 RecordSet False Passed
000f1e04728cc8b41a44f3c74162b467339b9c60 TLC with reduction strategy:
  • Plug 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)
Set2 RecordSet True Passed
2ec7dfdfe49e37e80291b90a2c5caf8ef3561373 TLC with reduction strategy:
  • Plug 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)
Set2 RecordSet False Passed
c468d896cf65e0d0673deb986651b88b3dc8da0e TLC with reduction strategy:
  • Plug 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)
Fun RecordSet True Passed
0f1d7037693dc2588621f49df6b00488ac1261b1 TLC with reduction strategy:
  • Plug 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)
Fun RecordSet False Passed
b5940710d5241bad83217963002f991ba2179888 TLC with reduction strategy:
  • Plug 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)
In RecordSet True Passed
8700eef09672cefde024aad5d2793daf6d77707b TLC with reduction strategy:
  • Plug 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)
In RecordSet False Passed
287b02b3044dcb2307c24e3ec25b3abfd0d25d0d TLC with reduction strategy:
  • Plug 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)
NotIn RecordSet True Passed
7f2a6f140ede03c6691d0037cf0e0355de7c6954 TLC with reduction strategy:
  • Plug 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)
NotIn RecordSet False Passed
9814b53cf79b684082eea719417d9173f604d179 TLC with reduction strategy:
  • Plug 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)
Record RecordSet True Passed
c580f033b4b0f943ddb3ba63ce16c042493f8381 TLC with reduction strategy:
  • Plug 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)
Record RecordSet False Passed
69641981ea412acdd2cd50eb951473efa31fc39a TLC with reduction strategy:
  • Plug 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)
Tuple RecordSet True Passed
cffb8017ab0b9102263726a29a2df3ac8f67e7cf TLC with reduction strategy:
  • Plug 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)
Tuple RecordSet False Passed
8767ced8a08a45ba8c9a44322f420216d2791bae TLC with reduction strategy:
  • Plug 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)
FunApp RecordSet True Passed
2009f007c92efce69fbdaac5a4031e6355136aae TLC with reduction strategy:
  • Plug 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)
FunApp RecordSet False Passed
e261ff1b64e5fa65852960d51540f2a7c0e8aa3e TLC with reduction strategy:
  • Plug 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)
Except1Fun RecordSet True Passed
32c7c553bb1ca1a4915ea3df8dba4c0164c445bb TLC with reduction strategy:
  • Plug 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)
Except1Fun RecordSet False Passed
add90ba00547b1a38ba46213e4731b04c0c32070 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug 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)
Except1FunWithAt RecordSet True Passed
70039a77cd6748a947db69b55971c3fd1439f721 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug 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)
Except1FunWithAt RecordSet False Passed
27fa2994eb356a8c28cf5944f279b0ef3c117489 TLC with reduction strategy:
  • Plug 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)
Except1Rec RecordSet True Passed
e3f1fdeb6b073fcd29eec0c6a0f669e43b143b9e TLC with reduction strategy:
  • Plug 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)
Except1Rec RecordSet False Passed
f7aad6f932c082d8c42298ef5cb693bf04fa0734 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug 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)
Except1RecWithAt RecordSet True Passed
2ecffba2a49818237ab287fc0caf6e88298977e5 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug 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)
Except1RecWithAt RecordSet False Passed
f310e647bd106dffc472c3af33c8ae0c196e6d64 TLC with reduction strategy:
  • Plug 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)
Except2Fun RecordSet True Passed
c44093972b345fa5bfb6c24a808653e656485259 TLC with reduction strategy:
  • Plug 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)
Except2Fun RecordSet False Passed
ea1a921abcd473d325a49a591c816cafda38a763 TLC with reduction strategy:
  • Plug 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)
Prime RecordSet True Passed
31e0b585c4c8676d864241e10da5808879f24c42 TLC with reduction strategy:
  • Plug 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)
Prime RecordSet False Passed
8d5308a64698120513caeb95542c59716e764bd6 TLC with reduction strategy:
  • Plug 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)
DefFun RecordSet True Passed
ab886376e0ef4a1b23a70c77a4fbd6097dca05c5 TLC with reduction strategy:
  • Plug 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)
DefFun RecordSet False Passed
80bfa3cdb189ca5f89dfebccef2bc0df1c912042 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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)
LetDefFun RecordSet True Passed
ff725806e4d33116d6922afc92bb5ea5b4608c95 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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)
LetDefFun RecordSet False Passed
ad18daf77b83987e27f6770ef553bbea5326e869 TLC with reduction strategy:
  • Plug 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)
DefFunRecursive RecordSet True Passed
eb17fce6b498a3c6dd38242c506416dd24bb4629 TLC with reduction strategy:
  • Plug 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)
DefFunRecursive RecordSet False Passed
753ae0485c7aa97298d16c3bf6ef26e7f17c136c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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)
LetDefFunRecursive RecordSet True Passed
7ee56ed08ad878d6d1516c47823568d2ea0e1565 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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)
LetDefFunRecursive RecordSet False Passed
010ef5a307b07178b8c1f7a1ae3fb9f0aaa6cd7b TLC with reduction strategy:
  • Plug 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)
Def0 RecordSet True Passed
85ac444ca93a2dc55472607efb93277ad0ed3daa TLC with reduction strategy:
  • Plug 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)
Def0 RecordSet False Passed
b968ee9abe05478e33c2db27ca2350f676a42a41 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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)
LetDef0 RecordSet True Passed
ec66ba4960c1729f1885dcb3cfc79efe0869b542 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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)
LetDef0 RecordSet False Passed
c3516e049ffe6a756c23e58d33587c11ab1c283f TLC with reduction strategy:
  • Plug 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)
Def1 RecordSet True Passed
f6a2aad2a2d66604737772de2b8292e2cabb894d TLC with reduction strategy:
  • Plug 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)
Def1 RecordSet False Passed
9afed542bc358395323bb0e3234c293cfd6ba7a9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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)
LetDef1 RecordSet True Passed
8e8aa54ad664f6b5599d4fe2c8b56ae0a4c13e9f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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)
LetDef1 RecordSet False Passed
30d302330b4c188f08fff9230a0c54f7b387adde TLC with reduction strategy:
  • Plug 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)
Def2 RecordSet True Passed
cf43c8409064f75c8df2b91b8a7f77aa6da6d122 TLC with reduction strategy:
  • Plug 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)
Def2 RecordSet False Passed
81cf2290e3b89d0f896b171367b0e0873e4122df TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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)
LetDef2 RecordSet True Passed
3c54dd9e7992ce5dfac79ae3567c7a4291cb4913 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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)
LetDef2 RecordSet False Passed
0d85bab6f7349c0829438061a50ec4837553cdf3 TLC with reduction strategy:
  • Plug 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)
Def1Recursive RecordSet True Passed
f0bc94d957d88d85fe1bc88d149cd8b560d7caed TLC with reduction strategy:
  • Plug 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)
Def1Recursive RecordSet False Passed
cba15d2cc3017573ced4e30b85ffbcbca9956e1d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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)
LetDef1Recursive RecordSet True Passed
f1d80ab16d399cca45153f16df0481b937d610d1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug 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)
LetDef1Recursive RecordSet False Passed
1cb2200b81d2548dc01b314bcd12b72a3a3ceca8 TLC with reduction strategy:
  • Plug 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)
Extends RecordSet True Passed
ddc1a3fbc434c3e29fb83437ed1bad672f87a557 TLC with reduction strategy:
  • Plug 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)
Extends RecordSet False Passed
f4725dc52ca31881bf4e89e74c116a8b38e4e7f8 TLC with reduction strategy:
  • Plug 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)
ExtendsInDifferentFolder RecordSet True Passed
d83a8834ab7adf6f72fb863c82d5cea77db4c9c4 TLC with reduction strategy:
  • Plug 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)
ExtendsInDifferentFolder RecordSet False Passed
e179b044120c71cf8906e1120768b949c1166be6 TLC with reduction strategy:
  • Plug 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)
Variable RecordSet True Passed
22fd78ce7d6d3265c8af64619d36ee55efb57007 TLC with reduction strategy:
  • Plug 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)
Variable RecordSet False Passed
a20120894902f49555c025eca9abd9ea456d05cd 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: 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)
VariableViewExclude RecordSet True Passed
25b846b83bb3a1c69cab48c2a32e110d35983278 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: 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)
VariableViewExclude RecordSet False Passed
2ef80eea0e0c954aa92ed3b988ba959cc96955eb TLC with reduction strategy:
  • Plug 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)
Constant RecordSet True Passed
e1e783757670d3b2fb000d16c0ca9e139f11b2e6 TLC with reduction strategy:
  • Plug 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)
Constant RecordSet False Passed
630d32b1411e20e1ef78449fd71f63138eeea01c TLC with reduction strategy:
  • Plug 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)
ConstantRank1 RecordSet True Passed
e38a180fff2cdf754215fb218cdf1f9b30e1e494 TLC with reduction strategy:
  • Plug 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)
ConstantRank1 RecordSet False Passed
86e24979ae30001643bf29584c8a10803a20d27a TLC with reduction strategy:
  • Plug 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)
Instance RecordSet True Passed
7a20bf3ba9ab56e0fafb046c5efe7ab7aa11fe90 TLC with reduction strategy:
  • Plug 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)
Instance RecordSet False Passed
53a1f8aba27ae88439d89f6358f8cf63cdb53f6f TLC with reduction strategy:
  • Plug 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)
InstanceWith RecordSet True Passed
51383b2fcd8747da6ab217c65cc04c04c1476e4f TLC with reduction strategy:
  • Plug 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)
InstanceWith RecordSet False Passed
8526bdde8c1ac39f5418ca2df508d1bfb347170d TLC with reduction strategy:
  • Plug 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)
InstanceNamed RecordSet True Passed
5de9722b52f4213facdb054395f36cbe9420b74b TLC with reduction strategy:
  • Plug 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)
InstanceNamed RecordSet False Passed
190de50c1488fd1873c697b98a1191c4a4798432 TLC with reduction strategy:
  • Plug 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)
InstanceNamedWith RecordSet True Passed
717af47f4c11c18894786bfa1c6cf0065fa37972 TLC with reduction strategy:
  • Plug 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)
InstanceNamedWith RecordSet False Passed
dbe397d802c15a7c5471c38735222595e325e4b1 TLC with reduction strategy:
  • Plug 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)
InstanceInFolder RecordSet True Passed
abfbdc5b5f4f8dddd5e7d93a655390ab0ef5ee68 TLC with reduction strategy:
  • Plug 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)
InstanceInFolder RecordSet False Passed
8dab1333c508d2a745d2f433d80c97764ba2e149 TLC with reduction strategy:
  • Plug 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)
InstanceWithInFolder RecordSet True Passed
12009768d815033d9a7724e1583144aaff9b613c TLC with reduction strategy:
  • Plug 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)
InstanceWithInFolder RecordSet False Passed
424ba43e994a4c01f0e97130fa0e67aecf34a209 TLC with reduction strategy:
  • Plug 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)
InstanceNamedInFolder RecordSet True Passed
70463af098804f6408a6aeb05b96e14d851a3342 TLC with reduction strategy:
  • Plug 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)
InstanceNamedInFolder RecordSet False Passed
70a1138dccb35f02069b72aff44f84ab97570c42 TLC with reduction strategy:
  • Plug 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)
InstanceNamedWithInFolder RecordSet True Passed
bea8580fa52e533510ffbd3394d3690e742ac563 TLC with reduction strategy:
  • Plug 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)
InstanceNamedWithInFolder RecordSet False Passed
357bede6315bae19fc00250b83d711370b404920 TLC with reduction strategy:
  • Plug 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)
Lambda RecordSet True Passed
c778c4714705bc535a29b9f200bb07465ed3c463 TLC with reduction strategy:
  • Plug 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)
Lambda RecordSet False Passed
a88edabdaa96b40451a8ae271e6c0f38c97cf63a TLC with reduction strategy:
  • Plug 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)
Cross2 RecordSet True Passed
85293edf1b37c747d249f6f2525614e5a00b0e25 TLC with reduction strategy:
  • Plug 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)
Cross2 RecordSet False Passed
c58ec3f504deeb0ef1281f8666556dc0cc13c18d TLC with reduction strategy:
  • Plug 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)
Cross3 RecordSet True Passed
9bedad3e5d5cb6e1804ee0317d6f1667ecf70f3d TLC with reduction strategy:
  • Plug 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)
Cross3 RecordSet False Passed
90456dfc48550d91ac11403fc9b7ae64fde19e00 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: 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)
FunSet RecordSet True Passed
1abd5f70240c39cd0ef6fe12007fbe0ebaf301a1 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: 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)
FunSet RecordSet False Passed
1971eb67371f44718313b64e6eb67963c1a86fec 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: 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)
RecordSet RecordSet True Passed
373dfe4fb0161aafd06e0f547ad935005597e502 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: 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)
RecordSet RecordSet False Passed
33fcc86d2b9b9c6075cba403490a0501093b286d TLC with reduction strategy:
  • Plug 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)
SetDiff RecordSet True Passed
cb5e427f4b1c6a4e3d030aab224ae155c4414a0b TLC with reduction strategy:
  • Plug 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)
SetDiff RecordSet False Passed
62c21fe45b56275c8a25075248b461f345377a21 TLC with reduction strategy:
  • Plug 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)
SetUnion RecordSet True Passed
74ade862c47ccf07888694df9e61dfcb52001019 TLC with reduction strategy:
  • Plug 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)
SetUnion RecordSet False Passed
5c7bfe85283f6165f95ef1ffec83e5351736aa6c TLC with reduction strategy:
  • Plug 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)
SetIntersect RecordSet True Passed
85020d3d7c8986e13d86af855d6fc24f0750088f TLC with reduction strategy:
  • Plug 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)
SetIntersect RecordSet False Passed
ce3736807013f4ee9e93f04dbaef0a4362fe5d58 TLC with reduction strategy:
  • Plug 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)
SubsetEq RecordSet True Passed
2f55258a3ff3640a4e2f939880b02b071fda71c0 TLC with reduction strategy:
  • Plug 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)
SubsetEq RecordSet False Passed
c79c7291622e4b7740895b11b53a55275bb5b6fc TLC with reduction strategy:
  • Plug 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)
IfThen RecordSet True Passed
5338328404219e7c20e67e18bfeb5aaab633884f TLC with reduction strategy:
  • Plug 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)
IfThen RecordSet False Passed
4bf7521854f458080b1146636b64afe49a779293 TLC with reduction strategy:
  • Plug 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)
IfElse RecordSet True Passed
24b9564fef678bcd4799bf09c37215054595af81 TLC with reduction strategy:
  • Plug 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)
IfElse RecordSet False Passed
e44c451658c3388a771c46f2e25dc37a0dddd211 TLC with reduction strategy:
  • Plug 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)
Subset RecordSet True Passed
e8cb21d6f3349b84e8fb45c5e4d72a2904a09a67 TLC with reduction strategy:
  • Plug 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)
Subset RecordSet False Passed
f18a5ef80ad60191732713ce3e234ad57c45e0f0 TLC with reduction strategy:
  • Plug 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)
Unchanged RecordSet True Passed
587ae28a774fe1698bc4895f62dbf2d196ba9dea TLC with reduction strategy:
  • Plug 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)
Unchanged RecordSet False Passed
49e0c47c61dcc205ddf7e99f27abd1852fded1f8 TLC with reduction strategy:
  • Plug 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)
SeqSeq RecordSet True Passed
69273fad48b08886d68ce413775213853fdb9b7f TLC with reduction strategy:
  • Plug 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)
SeqSeq RecordSet False Passed
ab46bfabe8b62f190ca11b0023c0fbcf00f3301b TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug 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)
TlcSingletonFun RecordSet True Passed
84002f6e4e39c45aba841567c336339f3070878a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug 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)
TlcSingletonFun RecordSet False Passed
d28200128de2bd7db503215f710bec4d474d9ae3 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug 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)
TlcPermuteFun RecordSet True Passed
ee3dd35083d9486734d3ad3d2bf86f3205349d10 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug 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)
TlcPermuteFun RecordSet False Passed
db87c79454cda4d4e46326ec752c066bd8f13b11 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug 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)
TlcEval RecordSet True Passed
17d1e467cd4cd8c68926f474da21027bbcb403fe TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug 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)
TlcEval RecordSet False Passed
63410a8ed87b24e05aaf1383802d2d62bcc6ba9b TLC with reduction strategy:
  • Plug 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)
BagSetToBag RecordSet True Passed
de6b55f1141222b020e8599c5e1c8c35dc23619f TLC with reduction strategy:
  • Plug 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)
BagSetToBag RecordSet False Passed
a930220c3b326802908d0a14575614e2f8b6d7c4 TLC with reduction strategy:
  • Plug 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)
BagBagIn RecordSet True Passed
062a35bb458173e82bf8e1b6eb8c45e71e0126f9 TLC with reduction strategy:
  • Plug 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)
BagBagIn RecordSet False Passed
9cdbd71f2ea720e9722aee253d0770dc46fb4e09 TLC with reduction strategy:
  • Plug 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)
BagCopiesIn RecordSet True Passed
d5d108a08331acfea0f89bb1b74ec86db282c99f TLC with reduction strategy:
  • Plug 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)
BagCopiesIn RecordSet False Passed
65f50841c4f931a4e66d159204adb503f96e3070 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: 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)
FiniteSetsIsFiniteSet RecordSet True Passed
99681ec0e3f3167d6c3b9f9d0a86f269eb3dfa41 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: 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)
FiniteSetsIsFiniteSet RecordSet False Passed
62aaf27b0f3de3b51139c4c34847c2431029242e TLC with reduction strategy:
  • Plug 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)
FiniteSetsCardinality RecordSet True Passed
4b44149533d2b767e40fd564641eb3edcb90c321 TLC with reduction strategy:
  • Plug 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)
FiniteSetsCardinality RecordSet False Passed
a6826e444a95253f4432f8ad9ac3e3f0943bd892 TLC with reduction strategy:
  • Plug 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)
SeqAppend RecordSet True Passed
8a30120485ee747cd6bd80ddd75660b101b5e230 TLC with reduction strategy:
  • Plug 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)
SeqAppend RecordSet False Passed