Index

Tests by case feature TlcExtendFun; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
7c64d47c6cb86fd071b3863f1f000aa207f71588 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: Replace spec with the same without comments
TlcExtendFun OneLineComment True Passed
94257164656011560b5e6a1ff8073a3527678637 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: Replace spec with the same without comments
TlcExtendFun OneLineComment False Passed
dd6da99fc0cddad71c7d8a9cd778dc472391ce62 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: Replace spec with the same without comments
TlcExtendFun MultiLineComment True Passed
01ef5249a738665c9a4a4ffc2d1a2eef2336558c 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: Replace spec with the same without comments
TlcExtendFun MultiLineComment False Passed
4829cf6f55f2d93b3ed8ee6839c2f3cc364c7834 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]]
TlcExtendFun Let True Passed
89cc825fafb7209ff8a99513f1e9f1ccc4689faa 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]]
TlcExtendFun Let False Passed
b4291bd8b1ede56125a02ae5850220b6c512ec23 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]]
TlcExtendFun Fun True Passed
6f53eeb31c4af8a018040545beb931dff81d8f3f 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]]
TlcExtendFun Fun False Passed
4c33f1e79d608251865ab091caeb737805b1a1c2 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]]
TlcExtendFun Choose True Passed
9f070acd7bc36d9685652ed3ae629988d2fd12b1 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]]
TlcExtendFun Choose False Passed
884bc6926eab116cb4a542b67085c4617f96a5bc 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]]
TlcExtendFun FunApp True Passed
4c85a3e7be3ab3ee7a64e9acc01eaff6ca3779c7 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]]
TlcExtendFun FunApp False Passed
f82baf83c1121d975d8a2b5c29901c3b9b5542c8 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]]
TlcExtendFun Prime True Passed
8a3f4c8b8438d096ee2eca023de42faac2372fa6 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]]
TlcExtendFun Prime False Passed
793a757d454c809c75ff670ba021951109e18fd0 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]]
TlcExtendFun DefFun True Passed
c93d533d00d003841e69660a9eab0355976934d8 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]]
TlcExtendFun DefFun False Passed
b79b355fd757a272b405cfa8e125ca1c51b4b957 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 LetDefFun True Passed
c5ca6712b1562912107a0fb117895dd2b32c1f90 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 LetDefFun False Passed
3ab6e68ce5dbc3642a3d43b5ba91ce144c3f2463 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]]
TlcExtendFun DefFunRecursive True Passed
ab859765ad63d93288c651654cf0f97454bb189c 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]]
TlcExtendFun DefFunRecursive False Passed
b0fca185a4839d115a07e0ad599980af8de958b3 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 LetDefFunRecursive True Passed
ee3528d83297084a220b45fc2ebcf3d067f85501 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 LetDefFunRecursive False Passed
94c4c789412563b8c099da024012311a80e81627 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]]
TlcExtendFun Def0 True Passed
247ac28cc29818d508a13edde95fa6cbfac986af 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]]
TlcExtendFun Def0 False Passed
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
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
2c8bbbdf27935dbc0e83595e428f24fba2647ae5 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]]
TlcExtendFun Def1 True Passed
ba15eeee35ad07465d251ca7541879cdb3111a79 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]]
TlcExtendFun Def1 False Passed
4348606bbc05ae5ed7ac1f85f74f35411cd247c7 TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
  • Plug Feature: LET definitions are reduced to global definitions
TlcExtendFun LetDef1 True Passed
17508a00b5e49f0784ae405198d063a5f3227b18 TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
  • Plug Feature: LET definitions are reduced to global definitions
TlcExtendFun LetDef1 False Passed
d49790e0e965fe483e614157465f435686a51b58 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]]
TlcExtendFun Def2 True Passed
313c688e69048a626b0be77c89a3c481793b286b 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]]
TlcExtendFun Def2 False Passed
eb82b33e9b8b93238d29fc82f2632eebf79a1095 TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
  • Plug Feature: LET definitions are reduced to global definitions
TlcExtendFun LetDef2 True Passed
a46b0536ef4c112c4e1a75fd348cf9a752391005 TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
  • Plug Feature: LET definitions are reduced to global definitions
TlcExtendFun LetDef2 False Passed
330ba6f19bc3803e575e271baa796b0facef3c60 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]]
TlcExtendFun Def1Recursive True Passed
3978d8a47eca02de0e69c73b09a04d946d9b67f9 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]]
TlcExtendFun Def1Recursive False Passed
b3c4540fb944fa3f68b734796ee8d94970665231 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 LetDef1Recursive True Passed
ee1cdc3113f09acce238eea8aea0415ab40447e1 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 LetDef1Recursive False Passed
de87f66215e716349d95d84cc8988afff4a089f0 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]]
TlcExtendFun Extends True Passed
391485e7d515691280f28b333ebc9bc41af64a8e 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]]
TlcExtendFun Extends False Passed
cdabdd3fd41c774bd8006cede96001736c4cc2a4 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]]
TlcExtendFun ExtendsInDifferentFolder True Passed
614e9b114c2dd52a65a570b2edec8d65e24f9ecb 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]]
TlcExtendFun ExtendsInDifferentFolder False Passed
ffdfbcb94877f2f48a792dd3f1dc1ea5159f805d 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]]
TlcExtendFun Variable True Passed
6b30c1d6c22f67212219ff3cf97e97de5c32cc68 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]]
TlcExtendFun Variable False Passed
6def6af5c5b110c4665a2d712ef3200ebb038949 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]]
TlcExtendFun Constant True Passed
c754876bb7701349e925160e55555e68cd285b42 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]]
TlcExtendFun Constant False Passed
b9ed4f964dcedbbd2daebc0627bc99e62ad52d98 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]]
TlcExtendFun ConstantRank1 True Passed
56798a72cb8df5b53570a24b60b4928573c27a12 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]]
TlcExtendFun ConstantRank1 False Passed
f49e049c64ff1bc4977c6fc765ef065fcdb02375 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]]
TlcExtendFun Instance True Passed
8c2668c029f53b341acd561dffb2b378acaa5364 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]]
TlcExtendFun Instance False Passed
c6d1350dddba32889a55d2a9b1f02b40bdb6c529 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]]
TlcExtendFun InstanceWith True Passed
587711775fc10f92f565e77e8c793a807eea3151 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]]
TlcExtendFun InstanceWith False Passed
e94f643adb58ac4d62b8d4f04e54a4ef8c16a676 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]]
TlcExtendFun InstanceNamed True Passed
84af4fbe6c38f0b66cd38bf5e5544f73e23b0f79 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]]
TlcExtendFun InstanceNamed False Passed
dd7faffaccd864d07ec32b9df637d77c092d5e65 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]]
TlcExtendFun InstanceNamedWith True Passed
2431aaa544d13e12b41a47d9d3400ec1b0562bbe 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]]
TlcExtendFun InstanceNamedWith False Passed
9bde8e80f26ab37bee2bdf8e14c405d2eb06848e 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]]
TlcExtendFun InstanceInFolder True Passed
e954236b328cedb485ada1fa141c1ec660348f55 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]]
TlcExtendFun InstanceInFolder False Passed
09c18a7a7a7276fafd28dd63e5f1083370ab208a 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]]
TlcExtendFun InstanceWithInFolder True Passed
b719191bc63d70970bd5a82dea85678dec2f0077 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]]
TlcExtendFun InstanceWithInFolder False Passed
1d6346b9b563aa84deaf2b7346e5d6184da25917 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]]
TlcExtendFun InstanceNamedInFolder True Passed
df70456e9135810e5fe94f6a0ec681b6bb560511 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]]
TlcExtendFun InstanceNamedInFolder False Passed
4ba885f3c4c82b324276bf02eca0b071727a644a 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]]
TlcExtendFun InstanceNamedWithInFolder True Passed
dabbefc9f12edc7dcd82d02e122e5ddf3e52aa4b 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]]
TlcExtendFun InstanceNamedWithInFolder False Passed
1f614ffd4f5ab721793a5a4343d191bd22fcfbd0 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]]
TlcExtendFun IfCond True Passed
a7847ff36dbd1e2ba42f4560facf2852f2ce82f5 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]]
TlcExtendFun IfCond False Passed
db671be30267064b35604e596c41a4affe0d9a87 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]]
TlcExtendFun IfThen True Passed
bba4031779ecf68f589fe631d0cb9f67c643f135 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]]
TlcExtendFun IfThen False Passed
35f53ce48f7ec26443abb1d960fb2a509f68dcd9 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]]
TlcExtendFun IfElse True Passed
2943eada9b3a1e7d3519c3ae6e7a4de99640110e 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]]
TlcExtendFun IfElse False Passed
1c9e65906ecd1a2543d02cd7075e53188719792f 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: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcExtendFun TlcSingletonFun True Passed
c4704e3d2484079984e6e1c2baedbdd2c1f95a82 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: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcExtendFun TlcSingletonFun False Passed
a9ee7b5257ddb2472336f4f4edf715afce8c4dab 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: 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]]
TlcExtendFun TlcExtendFun True Passed
3c0b7b539f8b56ee00e701ca9a52177ed5de8afb 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: 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]]
TlcExtendFun TlcExtendFun False Passed
58173320c39c18d7e01e50c4094703df7db82e09 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: TLCEval(expr) is reduced to just expr
TlcExtendFun TlcEval True Passed
e869aeb65dfefff5939900c2a89a62f98d27a464 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: TLCEval(expr) is reduced to just expr
TlcExtendFun TlcEval False Passed
ed79e0f5ba310b71df0f41dd4370bf3b6cf87064 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]]
TlcExtendFun SeqHead True Passed
d8c45d2401a813838365d675f84f9f4e3138c45b 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]]
TlcExtendFun SeqHead False Passed