Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
aca48e45d87cf75011fc82fa38fe24636e885d8d TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Eq TlcPermuteFun True Passed
f6ffa8aa0bae12d3ab99db2736bc26fc0edb83b3 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Eq TlcPermuteFun False Passed
9c0a88505bdda8429f0b8946f72a1bad0c9799cb TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Ne TlcPermuteFun True Passed
bd23d9035aa342378d2eac6af7d598670f812b1d TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Ne TlcPermuteFun False Passed
ba87d89e64399593674afb676df3bae293ac6aaf TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Let TlcPermuteFun True Passed
c5576fbad91e5c43ee63a63144dc1adae6002026 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Let TlcPermuteFun False Passed
7d51baf9b39e0150dc1c1a12c5d6747b744e3848 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Set0 TlcPermuteFun True Passed
abf528726a99d4f5c9a874054e6db36cf4d30bd1 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Set0 TlcPermuteFun False Passed
50ac5cd0b276ee1763caeac3265556a39d995d49 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Set1 TlcPermuteFun True Passed
f9202d17c988c29deb2c2c94823d007fdf6b5336 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Set1 TlcPermuteFun False Passed
b97f5648ca688bd4a9dbfd10ade47cee413ea959 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Set2 TlcPermuteFun True Passed
a4b935f1b42c6914e5709549a4a87f1864bd6238 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Set2 TlcPermuteFun False Passed
bc6e7b08bf75f6ad8ff12731b8af93fd85adffa0 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Fun TlcPermuteFun True Passed
6607df309d8f1a738b6a2119d846fd4fc794c506 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Fun TlcPermuteFun False Passed
d4728ef479da1146e5a0c9d9cd4eb24fdaef8ac8 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
In TlcPermuteFun True Passed
4571b02cce03f161f74f436fdec2fe1c75091e70 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
In TlcPermuteFun False Passed
bcef4cf7ed254658d4bba17ca3a6539107bf1046 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
NotIn TlcPermuteFun True Passed
f11d9f37ccefa189b2e7f7c207563c687b7b7ced TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
NotIn TlcPermuteFun False Passed
61c20715759f2dc4aef9a2f7f501aa1827b72f26 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Record TlcPermuteFun True Passed
716fc49be478ecd3852fefd7dda0c5438bb522fe TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Record TlcPermuteFun False Passed
2185f55e8fb9b2602a037c4ded9853def5fd1f99 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Tuple TlcPermuteFun True Passed
2bd7f0d01401219e1a7318f353c22e0ae97706d0 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Tuple TlcPermuteFun False Passed
cd0d073f58b81857bc1116e347c96106f97a079b TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
FunApp TlcPermuteFun True Passed
206c61b3dc093d0feab5ebcdd84366128a910ed0 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
FunApp TlcPermuteFun False Passed
d5047435e801342cd03b4f109d483214e08788dd TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Except1Fun TlcPermuteFun True Passed
7335a4cc64e20f4ce292a0cfbd7b315605cc7e4a TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Except1Fun TlcPermuteFun False Passed
0d40756ffb386b05a4e92c1cd225adfcadb26bad TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Except1FunWithAt TlcPermuteFun True Passed
2437bb5622fb55c486c073705da79f9e07a584fd TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Except1FunWithAt TlcPermuteFun False Passed
3544fef96c0cb34887d2cab1e4c6a127ddc9a65d TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Except1Rec TlcPermuteFun True Passed
cc3e9f14c5a90f6a12dc15cbd75e7d137ee1caed TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Except1Rec TlcPermuteFun False Passed
e1e6f70cfc34d39094416ee178216424df81d578 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Except1RecWithAt TlcPermuteFun True Passed
1715169133242cec1ad392b3864ae39e34044cfa TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Except1RecWithAt TlcPermuteFun False Passed
b1637be5986efafbcf5afc2d6bc45762d1130e7c TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Except2Fun TlcPermuteFun True Passed
7a916adabd28c171f9e19b74c7187054ae57fc08 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Except2Fun TlcPermuteFun False Passed
2401e7389ab807839a2435c6eb4d9f4fa29c84bb TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Prime TlcPermuteFun True Passed
9ba28b6c225379e2536068f3730dc66bdf039d41 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Prime TlcPermuteFun False Passed
d7a333efee59dbccd9fb16a3061f8ff78d937e71 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
DefFun TlcPermuteFun True Passed
5dda33e2554cf5b4b996af2db03c3eec08fe72f6 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
DefFun TlcPermuteFun False Passed
06e98bc92af7f4a62cc43d7ccadb6ee37eeb0923 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
LetDefFun TlcPermuteFun True Passed
1567311d8c2d65f4717f4054a04ebdfe299403ac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
LetDefFun TlcPermuteFun False Passed
40105ffa0d0421d260884b26b0187e830be4bc77 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
DefFunRecursive TlcPermuteFun True Passed
a4a03dc60eded132cbd5c9bd3ab4327dda8bca0b TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
DefFunRecursive TlcPermuteFun False Passed
97bbb16a1e72321f8d26ecfc130b75814f6a6277 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
LetDefFunRecursive TlcPermuteFun True Passed
98f32334b6a55d95e2a002f803fd82d7e45b4a02 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
LetDefFunRecursive TlcPermuteFun False Passed
f10dff435863427d398c6dcdafe0df9c9f09b32d TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Def0 TlcPermuteFun True Passed
5230e3d3de3040b2926c1f204bb4d19221078f23 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Def0 TlcPermuteFun False Passed
2a9cd0347bfaff4a1aa3396b51ef53cf075b9da6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
LetDef0 TlcPermuteFun True Passed
b41016f06de2df64d2716715b3bb2761f36ffff7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
LetDef0 TlcPermuteFun False Passed
b4e10863010c68c4ef3b7a15b7ffc8c5578e5172 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Def1 TlcPermuteFun True Passed
3c589d00f752e182c0faf4f955c4d60136541162 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Def1 TlcPermuteFun False Passed
b0683d07525e5f41f8a8dd4ffdb1506b865257e7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
LetDef1 TlcPermuteFun True Passed
2f646f41c5d805c0c4dfba0b953efe293c37a67d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
LetDef1 TlcPermuteFun False Passed
cdd4c8f6b6768d673426c9abc9d2ec2cfc15245a TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Def2 TlcPermuteFun True Passed
96ff50c0eefe8a00c20e00fa5f13363a6bf6e8d7 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Def2 TlcPermuteFun False Passed
f53aac28c3f753854330692370f133c36c8f449c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
LetDef2 TlcPermuteFun True Passed
f1ad1ab41ab2934c2c2c6252756eea6a43d2c4a5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
LetDef2 TlcPermuteFun False Passed
c2d3a4264ea95cf8fce198e02e5649097bf12593 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Def1Recursive TlcPermuteFun True Passed
5fd8ec35101c1d4b8eb3479157e00fc024c29c86 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Def1Recursive TlcPermuteFun False Passed
9e6cff00756ba2c5189036463814155db908c221 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
LetDef1Recursive TlcPermuteFun True Passed
6d6a835e1e9ecc4de8e96220708abbd26da6dace TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
LetDef1Recursive TlcPermuteFun False Passed
f7f858a5bf04954e2a26c43e33efb80e53509d72 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Extends TlcPermuteFun True Passed
f7f17fa7c0a08994a1431b232a5a1436f011e7cf TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Extends TlcPermuteFun False Passed
02262e74c6c22b0dde460abe8f03dabfa0f72d0f TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
ExtendsInDifferentFolder TlcPermuteFun True Passed
0623a670591c3f1fe7f65610d8f5b9af2fe76978 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
ExtendsInDifferentFolder TlcPermuteFun False Passed
301487d6b829e8d81c22df0224bb431ca76ddc72 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Variable TlcPermuteFun True Passed
75638a75f1d7c6e248a3a63165f3322073257642 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Variable TlcPermuteFun False Passed
9fb1332d67a25b5ea11e3857e891082fc5f42578 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: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
VariableViewExclude TlcPermuteFun True Passed
32562c324823527058f36b6c72878120b838dd5e 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: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
VariableViewExclude TlcPermuteFun False Passed
45beeeb4753d06bd0f01514b1c2a16826f1f6926 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Constant TlcPermuteFun True Passed
b657c06c52e6670765e47e057c3ee45069b3a77c TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Constant TlcPermuteFun False Passed
94065538dacd924e42f041fb0349bc3aef5f4acc TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
ConstantRank1 TlcPermuteFun True Passed
443977cd8e3b79fea68573ea24eb907846f243b3 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
ConstantRank1 TlcPermuteFun False Passed
4ff10b349ba3338f48f634ccda09ea5c48b27b52 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Instance TlcPermuteFun True Passed
0e80fa173ad975cbe7fb56988ddf55150dc080dd TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Instance TlcPermuteFun False Passed
d080ebec07b1b34c908386ae5417bc318eb24eaa TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceWith TlcPermuteFun True Passed
f4a4569de117e383d08d10b549105c21cdd48fd7 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceWith TlcPermuteFun False Passed
21ddff623839238961e1b93eac5eab39ee5e6d7d TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceNamed TlcPermuteFun True Passed
b361d807350d30eedc6b15249a4ef9e67c43d986 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceNamed TlcPermuteFun False Passed
9aca63d55bbfa21f728197aabfd0c35878595100 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceNamedWith TlcPermuteFun True Passed
2c02b629557d8bcc80746700bd995204cfc89a98 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceNamedWith TlcPermuteFun False Passed
baff342eb51267a8862757793f89a3a2ad604a96 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceInFolder TlcPermuteFun True Passed
065c74d1084a61103048025a1899c8d718a24ded TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceInFolder TlcPermuteFun False Passed
a8d6ae39eb1d436ceef3946ff255d5b32228506a TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceWithInFolder TlcPermuteFun True Passed
4a897b8e5790cab012737acb7e200cc1f043dbe7 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceWithInFolder TlcPermuteFun False Passed
973c231ac60ef07a50a015f8f2e13bb2fb27945d TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceNamedInFolder TlcPermuteFun True Passed
8dacb2ace98418c808264727ef5c0e7ceba8e7ed TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceNamedInFolder TlcPermuteFun False Passed
af9af71d1b9b7a705ee0051471a99f2d720bfe20 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceNamedWithInFolder TlcPermuteFun True Passed
8d13913dbffd983e979bc826926a498148a12a1a TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceNamedWithInFolder TlcPermuteFun False Passed
cb5f382ec001fb8267ed2955759b565fdb9615ab TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Lambda TlcPermuteFun True Passed
438c19e3e606d5a64f66d1e6f9dfd7b98d37ddff TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Lambda TlcPermuteFun False Passed
2bbc9f58fea2d7025ca2924d5d1f4f55aa9842b6 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Cross2 TlcPermuteFun True Passed
39661daaf0dfb0b22c87401cc1395df9a6346756 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Cross2 TlcPermuteFun False Passed
c2d7dbd7d25726ac46554326a281cf4190ab354d TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Cross3 TlcPermuteFun True Passed
445e183f22b06f95632b6b2af9a82bd03572f5c4 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Cross3 TlcPermuteFun False Passed
51dc1aafcd3828211673a3fc5c6ecfc67b732650 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: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
FunSet TlcPermuteFun True Passed
cbf1e7e7d9c60dc639fcbcf384d41f0f4c25ba42 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: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
FunSet TlcPermuteFun False Passed
be79c9344c95988217650a36c9ad84457bc4243e 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: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
RecordSet TlcPermuteFun True Passed
7b42313a4b43e4289afb6e36ad89fe4438c8ce8f 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: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
RecordSet TlcPermuteFun False Passed
e71c409003a2d0823d39cb482b317aa91ac5c24a TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
SetDiff TlcPermuteFun True Passed
fcea10f31ccc885decdaf7c460eea6232c8d3a72 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
SetDiff TlcPermuteFun False Passed
5c13574b8ca0a0dc991e7dd6186ce0475e941f0c TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
SetUnion TlcPermuteFun True Passed
85e47bb03e855f69c7bea5486d7cad1c5674634b TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
SetUnion TlcPermuteFun False Passed
f271ed41e273d694034078427a061d32f2ccb773 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
SetIntersect TlcPermuteFun True Passed
472d5eb641180133f154382e6ba6c0fba3be5997 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
SetIntersect TlcPermuteFun False Passed
8d23ee4aec165ccbedac5f5089100ad0da263d86 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
SubsetEq TlcPermuteFun True Passed
de19a172057fdcfceb06e56815c7042fda457e04 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
SubsetEq TlcPermuteFun False Passed
304fbe4fa2ae3aa9b5efd24f9340536fed25a07b TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
IfThen TlcPermuteFun True Passed
daec552f0cbfd4dd7cddad54ced35cb2210613bb TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
IfThen TlcPermuteFun False Passed
69cd61906479b0a575e34e11ae3a0528b5c26e9c TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
IfElse TlcPermuteFun True Passed
18ab76c1ce1dd0d9c362baa23021ae40162ff58e TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
IfElse TlcPermuteFun False Passed
0f411e47d63a89910e209d4eafa94b82231f6f8d TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Subset TlcPermuteFun True Passed
4f8f8e4278179db0650dfebd73ef9eed73f019ea TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Subset TlcPermuteFun False Passed
5250615f8595ae39c4c80ec5bb9bd41f4728bfb6 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Unchanged TlcPermuteFun True Passed
792e9973f88d9afeb94e013bcb70b03047c58029 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Unchanged TlcPermuteFun False Passed
6711d6aa60217297c00d2c0dd79410c4c4e233f6 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
SeqSeq TlcPermuteFun True Passed
f44d2461bcb27029745941109ea2ac675583a70b TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
SeqSeq TlcPermuteFun False Passed
386390a0ff8e09311c4ffbfdd50f85a1b2218076 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcSingletonFun TlcPermuteFun True Passed
76a167da929ad4a3e36a3892bbaed7d95cec5600 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcSingletonFun TlcPermuteFun False Passed
81e22650cb38a4bc83515e7876de193f3b641ca3 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun TlcPermuteFun True Passed
b2434f93a6fde990156aff4238b3230ca2665eed TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun TlcPermuteFun False Passed
d056dac3711cc2c5686558c67a18b4e7745ba5d5 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcEval TlcPermuteFun True Passed
22d853b5c0d0121a02cde213df39ffe80ea50f91 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcEval TlcPermuteFun False Passed
8d0c5f8e7d3bba47bce5b5ddf89d066a066306a4 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
BagSetToBag TlcPermuteFun True Passed
970326c351c6929e57e12c6d0b66e6b7c5d964ee TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
BagSetToBag TlcPermuteFun False Passed
d9d437fa283da58a0de2ea8a4a874ff507ed015d TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
BagBagIn TlcPermuteFun True Passed
672a47cb78c47630d31e0b925aa35d5a232e7cae TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
BagBagIn TlcPermuteFun False Passed
0504becd7b691663b1dfbe5334446d7a0d8c3032 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
BagCopiesIn TlcPermuteFun True Passed
f6d6122d2fb046e17fe0dc54cf6fc5e2645360fb TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
BagCopiesIn TlcPermuteFun False Passed
b2841fea811ed7aa2ca0e85e7448500fa10b70ae 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: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
FiniteSetsIsFiniteSet TlcPermuteFun True Passed
9ffbba8ef2da57992519aac88b370ce45c3af09a 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: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
FiniteSetsIsFiniteSet TlcPermuteFun False Passed
7ad4a59d16a764e04c5b70bbfdfe4a428c0c8fd0 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
FiniteSetsCardinality TlcPermuteFun True Passed
7bd472e340af2b1ac1ee2aede2ae977018e1e0ff TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
FiniteSetsCardinality TlcPermuteFun False Passed
a5d4f040d6d9ad59f37dbf387ff24e8e36dc2131 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
SeqAppend TlcPermuteFun True Passed
e296811f9ed83df9e19757e6abb39eb9d92f8190 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
SeqAppend TlcPermuteFun False Passed