From cfeab4519e4fe3a505d5aef7401f5710ff7f30d0 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Fri, 2 Mar 2018 12:24:49 +0000 Subject: [PATCH] Correct typecheck of tail for seq1, fixes #669 --- .../integration/legacy/sl/DFDexampleSL.vdmsl.result | 2 +- .../overture/typechecker/visitor/TypeCheckerExpVisitor.java | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/core/pog/src/test/resources/integration/legacy/sl/DFDexampleSL.vdmsl.result b/core/pog/src/test/resources/integration/legacy/sl/DFDexampleSL.vdmsl.result index 430b6ff6f4..39c3febcab 100644 --- a/core/pog/src/test/resources/integration/legacy/sl/DFDexampleSL.vdmsl.result +++ b/core/pog/src/test/resources/integration/legacy/sl/DFDexampleSL.vdmsl.result @@ -1 +1 @@ -["legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 77:29: (forall dfdid:DEFAULT`DFDId, dss:DEFAULT`DSs, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, dfdmap:DEFAULT`DFDMap \u0026 ((dfdid in set (dom dfdsig)) \u003d\u003e (dfdid in set (dom dfdsig))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 241:34: (forall fidl:seq of (DEFAULT`FlowId) \u0026 ((not (0 \u003d (len fidl))) \u003d\u003e ((not (1 \u003d (len fidl))) \u003d\u003e is_([FlowIdTypeConf(fidl(i)) | i in set (inds fidl)], seq1 of (DEFAULT`Type)))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 649:14: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in pre_MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPRE\u003e, \u003cPRE\u003e))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1205:3: (forall -:DEFAULT`Id, n:nat, max:nat \u0026 ((max - n) \u003e\u003d 0))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 651:31: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId)))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1148:31: (forall dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, notneeded:set of (DEFAULT`FlowId), pids:set of (DEFAULT`ProcId) \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in ((not ((dom dfdsig) \u003d pids)) \u003d\u003e (forall pid in set ((dom dfdsig) \\ pids) \u0026 ((not ((TransClosure(pid, top, {}) \u003d {}) and (EquivClass(top, {pid}) \u003d (dom dfdsig)))) \u003d\u003e (pid in set (dom dfdsig))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 761:31: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) \u003d\u003e (nid in set (dom dfdsig))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1145:23: (forall dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, notneeded:set of (DEFAULT`FlowId), pids:set of (DEFAULT`ProcId) \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in ((not ((dom dfdsig) \u003d pids)) \u003d\u003e (forall pid in set ((dom dfdsig) \\ pids) \u0026 ((TransClosure(pid, top, {}) \u003d {}) \u003d\u003e is_(top, set of ((DEFAULT`ProcId * DEFAULT`ProcId)))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1440:16: (forall id:(DEFAULT`DFDId | DEFAULT`DSId | DEFAULT`EPId | DEFAULT`Id | DEFAULT`MSId) \u0026 let realid:(DEFAULT`DFDId | DEFAULT`DSId | DEFAULT`EPId | DEFAULT`Id | DEFAULT`MSId | seq of (char)) \u003d (cases id :\nmk_DSId(id\u0027) -\u003e id\u0027,\nmk_DFDId(id\u0027) -\u003e id\u0027,\nmk_EPId(id\u0027) -\u003e id\u0027,\nmk_MSId(id\u0027) -\u003e id\u0027\nothers id\n end) in (forall i in set (inds realid) \u0026 (i in set (inds realid))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 118:45: (forall fidl:seq of (DEFAULT`FlowId) \u0026 ((not (0 \u003d (len fidl))) \u003d\u003e ((not (1 \u003d (len fidl))) \u003d\u003e (forall i in set (inds fidl) \u0026 (i in set (inds fidl))))))","non-empty sequence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1096:27: (forall idl:seq of (DEFAULT`Id) \u0026 ((not (0 \u003d (len idl))) \u003d\u003e ((1 \u003d (len idl)) \u003d\u003e (idl \u003c\u003e []))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 40:11: (forall mk_(dfdid, dss, dfdtopo, dfdmap, dfdsig):DEFAULT`HDFD, mss:DEFAULT`MSs, style:(\u003cEXPL\u003e | \u003cIMPL\u003e) \u0026 pre_MakeInterface(dfdid, dss, dfdtopo, dfdsig, dfdmap))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 837:42: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 let mk_(s, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in ((not (m \u003d \u003cREAD\u003e)) \u003d\u003e (s in set (dom maxm))))))","cases exhaustive obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1773:4: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 (((((exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (dfdtop(flowid) \u003d mk_(id, mk_EPId(any1)))) or (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (dfdtop(flowid) \u003d mk_(mk_EPId(any2), id)))) or (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (dfdtop(flowid) \u003d mk_(nil, id)))) or (exists mk_(id, nil):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (dfdtop(flowid) \u003d mk_(id, nil)))) or (exists mk_(fid, tid):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (dfdtop(flowid) \u003d mk_(fid, tid))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 649:30: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId)))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 749:14: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in pre_MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPOST\u003e, \u003cPRE\u003e)))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 832:32: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 (i in set (inds dst)))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1105:43: (forall idl:seq1 of (DEFAULT`Id) \u0026 ((not ((len idl) \u003d 1)) \u003d\u003e (forall i in set (inds idl) \u0026 (i in set (inds idl)))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 820:40: (forall dfdtopo:DEFAULT`DFDTopo \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or (is_(fid, MSId) or (fid \u003d nil))) and (is_(tid, DFDId) or (is_(tid, MSId) or (tid \u003d nil))))}, top2:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in let piset:set of ([DEFAULT`ProcId]) \u003d ((dunion {{pi_1, pi_2} | mk_(pi_1, pi_2) in set top}) \\ {nil}) in (forall piseq in set PossibleSeqs(piset) \u0026 (forall i, j in set (inds piseq) \u0026 ((j \u003c i) \u003d\u003e (is_(piseq(i), DEFAULT`DFDId) or is_(piseq(i), DEFAULT`MSId))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 851:26: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 (forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (s in set (dom intm)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 746:28: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 ((mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)})) \u003d\u003e (stid in set (dom intm))))))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 204:12: (forall dfdsig:DEFAULT`DFDSig, mss:DEFAULT`MSs \u0026 ((not (forall id in set (dom dfdsig) \u0026 is_(id, DFDId))) \u003d\u003e (exists id in set (dom dfdsig) \u0026 is_(id, MSId))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 529:14: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and pre_MakeImplOpBody(dfdid, dfdtopo, dfdsig)) \u003d\u003e let mk_(din, out, dst):DEFAULT`Signature \u003d dfdsig(dfdid) in pre_MakeImplOpBody(dfdid, dfdtopo, dfdsig)))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1120:28: (forall op:DEFAULT`BinaryOp, es:set of (DEFAULT`Expr) \u0026 ((es \u003c\u003e {}) \u003d\u003e (forall e in set es \u0026 ((not ((card es) \u003d 1)) \u003d\u003e pre_DBinOp(op, (es \\ {e}))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 651:15: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in pre_MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPRE\u003e, \u003cPOST\u003e))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1172:11: (forall fids:set of (DEFAULT`FlowId) \u0026 ((not (fids \u003d {})) \u003d\u003e (exists fid in set fids \u0026 true)))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1767:18: (forall dss:DEFAULT`DSs, dfdsig:DEFAULT`DFDSig \u0026 (forall dsid in set dss \u0026 (forall mk_(-, -, dst) in set (rng dfdsig) \u0026 (forall i in set (inds dst) \u0026 (i in set (inds dst))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 724:18: (forall dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo) in (forall piseq in set eos \u0026 pre_MakePostForEO(piseq, dfdsig, intm, maxm)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 763:27: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) \u003d\u003e (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) \u003d\u003e (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId)))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1037:16: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 ((dfdid in set (dom dfdsig)) \u003d\u003e (forall m1, m2 in set {{stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid))} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4)))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 624:3: (forall dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo) in pre_DBinOp(\u003cOR\u003e, {MakePreForEO(piseq, dfdsig, intm, maxm) | piseq in set eos}))","recursive function obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1177:19: (forall fids:set of (DEFAULT`FlowId) \u0026 ((not (fids \u003d {})) \u003d\u003e (forall fid in set fids \u0026 let pat:seq1 of (DEFAULT`PatternId) \u003d [mk_PatternId(FlowIdVarConf(fid))], first:DEFAULT`TypeBind \u003d mk_TypeBind(pat, FlowIdTypeConf(fid)) in (CardFId(fids) \u003e CardFId((fids \\ {fid}))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1777:44: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)) \u003d\u003e let mk_(mk_EPId(-), id) \u003d dfdtop(flowid) in (id in set (dom dfdsig)))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 208:35: (forall dfdsig:DEFAULT`DFDSig, mss:DEFAULT`MSs \u0026 ((not (forall id in set (dom dfdsig) \u0026 is_(id, DFDId))) \u003d\u003e (forall id in set (dom dfdsig) \u0026 (is_(id, MSId) \u003d\u003e ((not (id in set (dom mss))) \u003d\u003e (id in set (dom dfdsig)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1266:1: (forall n:nat \u0026 ((if ((n \u003d 0) or (n \u003d 1))\nthen n\nelse (n - 1)) \u003e\u003d 0))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1143:13: (forall dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, notneeded:set of (DEFAULT`FlowId), pids:set of (DEFAULT`ProcId) \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in ((not ((dom dfdsig) \u003d pids)) \u003d\u003e (exists pid in set ((dom dfdsig) \\ pids) \u0026 true)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1322:22: (forall id:DEFAULT`StId \u0026 ((not is_(id, DSId)) \u003d\u003e is_(id, seq of (char))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1813:6: (forall id:DEFAULT`DFDId, top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])), dfdmap:DEFAULT`DFDMap, dfdsig:DEFAULT`DFDSig \u0026 (forall dfdid in set (dom dfdmap) \u0026 let mk_(-, -, -, -, dfdsig\u0027):DEFAULT`HDFD \u003d dfdmap(dfdid) in (dfdid in set (dom dfdsig\u0027))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 566:16: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall m1, m2 in set {{stid |-\u003e 0} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 224:42: (forall fidl:seq of (DEFAULT`FlowId) \u0026 (forall i in set (inds fidl) \u0026 (i in set (inds fidl))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 647:28: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 ((not (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))) \u003d\u003e (stid in set (dom intm)))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 142:1: (forall dfdid:DEFAULT`DFDId, dss:DEFAULT`DSs, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, mss:DEFAULT`MSs, style:(\u003cEXPL\u003e | \u003cIMPL\u003e) \u0026 is_(let dst:[DEFAULT`StateDef] \u003d MakeState(dfdid, dss, CollectExtDFs(dfdtopo)), msdescs:set of (DEFAULT`Definition) \u003d MakeMSDescs(dfdsig, mss), dfdop:DEFAULT`OpDef \u003d MakeDFDOp(dfdid, dfdtopo, dfdsig, style) in (if (dst \u003d nil)\nthen ({dfdop} union msdescs)\nelse ({dst, dfdop} union msdescs)), set of (DEFAULT`Definition)))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 674:22: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let mk_(-, out, dst):DEFAULT`Signature \u003d dfdsig(dfdid), fids:set of (DEFAULT`FlowId) \u003d NeedsQuant(dfdtopo, dfdsig, (elems out), {}) in pre_MakeInExpr(out, dst, fids, dfdtopo, dfdsig, intm, maxm) \u003d\u003e (dfdid in set (dom dfdsig))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 207:25: (forall dfdsig:DEFAULT`DFDSig, mss:DEFAULT`MSs \u0026 ((not (forall id in set (dom dfdsig) \u0026 is_(id, DFDId))) \u003d\u003e (forall id in set (dom dfdsig) \u0026 (is_(id, MSId) \u003d\u003e ((id in set (dom mss)) \u003d\u003e (id in set (dom mss)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 804:1: (forall dfdtopo:DEFAULT`DFDTopo \u0026 is_(let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or (is_(fid, MSId) or (fid \u003d nil))) and (is_(tid, DFDId) or (is_(tid, MSId) or (tid \u003d nil))))}, top2:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in let piset:set of ([DEFAULT`ProcId]) \u003d ((dunion {{pi_1, pi_2} | mk_(pi_1, pi_2) in set top}) \\ {nil}) in {piseq | piseq in set PossibleSeqs(piset) \u0026 (forall i, j in set (inds piseq) \u0026 ((j \u003c i) \u003d\u003e (piseq(j) not in set TransClosure(piseq(i), top2, {}))))}, set of (seq1 of (DEFAULT`ProcId))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 644:13: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall m1, m2 in set {{stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid))} | stid in set (dom intm)} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 682:24: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (dfdid in set (dom dfdsig)))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 147:15: (forall dfdid:DEFAULT`DFDId, dss:DEFAULT`DSs, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, mss:DEFAULT`MSs, style:(\u003cEXPL\u003e | \u003cIMPL\u003e) \u0026 pre_MakeDFDOp(dfdid, dfdtopo, dfdsig, style))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1029:16: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e let mk_(din, -, -):DEFAULT`Signature \u003d dfdsig(dfdid), eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo), intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (forall piseq in set eos \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig))))","recursive function obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1366:26: (forall pids:set of (DEFAULT`ProcId) \u0026 ((not (pids \u003d {})) \u003d\u003e ((not ((card pids) \u003d 1)) \u003d\u003e (forall pid in set pids \u0026 (CardPSet(pids) \u003e CardPSet((pids \\ {pid})))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1738:22: (forall mk_(sysid, -, dfdtop, -, dfdsig):DEFAULT`HDFD \u0026 ((sysid in set (dom dfdsig)) \u003d\u003e let mk_(din, out, dst):DEFAULT`Signature \u003d dfdsig(sysid) in ((din \u003d []) \u003d\u003e ((out \u003d []) \u003d\u003e (forall flowid in set (dom dfdtop) \u0026 (flowid in set (dom dfdtop)))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 831:30: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds din) \u0026 (i in set (inds din)))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1031:15: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e let mk_(din, -, -):DEFAULT`Signature \u003d dfdsig(dfdid), eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo), intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm)))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1201:8: (forall id:DEFAULT`Id, n:nat, max:nat \u0026 ((n \u003c\u003d max) \u003d\u003e ((not (n \u003d max)) \u003d\u003e pre_MakePatternSeq((id ^ \"\u0027\"), (n + 1), max))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 751:35: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (nid in set (dom dfdsig))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1063:23: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (nid in set (dom dfdsig))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1735:24: (forall mk_(sysid, -, dfdtop, -, dfdsig):DEFAULT`HDFD \u0026 ((sysid in set (dom dfdsig)) \u003d\u003e (sysid in set (dom dfdsig))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 724:5: (forall dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo) in pre_DBinOp(\u003cOR\u003e, {MakePostForEO(piseq, dfdsig, intm, maxm) | piseq in set eos}))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 645:40: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 (nid in set (dom dfdsig))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 91:36: (forall dfdids:set of (DEFAULT`DFDId), dfdsig:DEFAULT`DFDSig \u0026 ((dfdids subset (dom dfdsig)) \u003d\u003e (forall id in set dfdids \u0026 (id in set (dom dfdsig)))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 563:15: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and pre_MakePostExpr(dfdid, dfdtopo, dfdsig, intm, maxm)) \u003d\u003e pre_MakePostExpr(dfdid, dfdtopo, dfdsig, intm, maxm)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 836:52: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 let mk_(s, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in ((not (m \u003d \u003cREAD\u003e)) \u003d\u003e ((intm(s) - 1) \u003e\u003d 0)))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 840:29: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 (let mk_(-, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (m \u003d \u003cREADWRITE\u003e) \u003d\u003e (i in set (inds dst))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 701:8: (forall out:seq of (DEFAULT`FlowId), dst:DEFAULT`State, fids:set of (DEFAULT`FlowId), dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (pre_MakeExistsBind(fids, dst, intm, maxm, \u003cPOST\u003e) \u003d\u003e let pred:DEFAULT`Expr \u003d MakePostPred(dfdtopo, dfdsig, intm, maxm) in pre_QuantNec(out, dst, fids, intm, maxm)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 820:49: (forall dfdtopo:DEFAULT`DFDTopo \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or (is_(fid, MSId) or (fid \u003d nil))) and (is_(tid, DFDId) or (is_(tid, MSId) or (tid \u003d nil))))}, top2:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in let piset:set of ([DEFAULT`ProcId]) \u003d ((dunion {{pi_1, pi_2} | mk_(pi_1, pi_2) in set top}) \\ {nil}) in (forall piseq in set PossibleSeqs(piset) \u0026 (forall i, j in set (inds piseq) \u0026 ((j \u003c i) \u003d\u003e is_(top2, set of (((DEFAULT`DFDId | DEFAULT`MSId) * (DEFAULT`DFDId | DEFAULT`MSId))))))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1020:14: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e (forall m1, m2 in set {{stid |-\u003e 0} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 207:29: (forall dfdsig:DEFAULT`DFDSig, mss:DEFAULT`MSs \u0026 ((not (forall id in set (dom dfdsig) \u0026 is_(id, DFDId))) \u003d\u003e (forall id in set (dom dfdsig) \u0026 (is_(id, MSId) \u003d\u003e ((id in set (dom mss)) \u003d\u003e is_(id, DEFAULT`MSId))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 749:41: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 745:40: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 (nid in set (dom dfdsig)))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1288:1: (forall id:(DEFAULT`DFDId | DEFAULT`Id | DEFAULT`MSId) \u0026 is_((cases id :\nmk_MSId(id\u0027) -\u003e id\u0027,\nmk_DFDId(id\u0027) -\u003e id\u0027\nothers id\n end), seq of (char)))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 559:14: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and pre_MakePostExpr(dfdid, dfdtopo, dfdsig, intm, maxm)) \u003d\u003e (forall m1, m2 in set {{stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid))} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4)))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 651:35: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (nid in set (dom dfdsig)))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 839:31: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds out) \u0026 (i in set (inds out)))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 249:15: (forall dst:DEFAULT`State \u0026 (forall i in set (inds dst) \u0026 (i in set (inds dst))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 702:21: (forall out:seq of (DEFAULT`FlowId), dst:DEFAULT`State, fids:set of (DEFAULT`FlowId), dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (pre_MakeExistsBind(fids, dst, intm, maxm, \u003cPOST\u003e) \u003d\u003e let pred:DEFAULT`Expr \u003d MakePostPred(dfdtopo, dfdsig, intm, maxm) in (QuantNec(out, dst, fids, intm, maxm) \u003d\u003e pre_MakeExistsBind(fids, dst, intm, maxm, \u003cPOST\u003e))))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1364:17: (forall pids:set of (DEFAULT`ProcId) \u0026 ((not (pids \u003d {})) \u003d\u003e ((not ((card pids) \u003d 1)) \u003d\u003e (exists pid in set pids \u0026 true))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 761:27: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) \u003d\u003e (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1062:49: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1391:16: (forall id:(DEFAULT`DFDId | DEFAULT`DSId | DEFAULT`EPId | DEFAULT`Id | DEFAULT`MSId) \u0026 let realid:(DEFAULT`DFDId | DEFAULT`DSId | DEFAULT`EPId | DEFAULT`Id | DEFAULT`MSId | seq of (char)) \u003d (cases id :\nmk_DSId(id\u0027) -\u003e id\u0027,\nmk_DFDId(id\u0027) -\u003e id\u0027,\nmk_EPId(id\u0027) -\u003e id\u0027,\nmk_MSId(id\u0027) -\u003e id\u0027\nothers id\n end) in (forall i in set (inds realid) \u0026 (i in set (inds realid))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1774:51: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)) \u003d\u003e let mk_(id, mk_EPId(-)) \u003d dfdtop(flowid) in (is_(id, DEFAULT`DFDId) or is_(id, DEFAULT`MSId))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 562:15: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and pre_MakePostExpr(dfdid, dfdtopo, dfdsig, intm, maxm)) \u003d\u003e pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 817:42: (forall dfdtopo:DEFAULT`DFDTopo \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or (is_(fid, MSId) or (fid \u003d nil))) and (is_(tid, DFDId) or (is_(tid, MSId) or (tid \u003d nil))))}, top2:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in let piset:set of ([DEFAULT`ProcId]) \u003d ((dunion {{pi_1, pi_2} | mk_(pi_1, pi_2) in set top}) \\ {nil}) in is_(piset, set of (DEFAULT`ProcId)))","type invariant satisfiable obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1672:1: (exists mk_(-, out, sta):DEFAULT`Signature \u0026 ((sta \u003d []) \u003d\u003e (((out \u003c\u003e []) and (out \u003d [])) \u003d\u003e (exists mk_(-, m) in set (elems sta) \u0026 (m \u003d \u003cREADWRITE\u003e)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 841:42: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 (let mk_(-, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (m \u003d \u003cREADWRITE\u003e) \u003d\u003e let mk_(s, -):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (s in set (dom maxm))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1062:38: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1813:21: (forall id:DEFAULT`DFDId, top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])), dfdmap:DEFAULT`DFDMap, dfdsig:DEFAULT`DFDSig \u0026 (forall dfdid in set (dom dfdmap) \u0026 let mk_(-, -, -, -, dfdsig\u0027):DEFAULT`HDFD \u003d dfdmap(dfdid) in (dfdid in set (dom dfdsig))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 557:14: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and pre_MakePostExpr(dfdid, dfdtopo, dfdsig, intm, maxm)) \u003d\u003e (forall m1, m2 in set {{stid |-\u003e 0} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1780:53: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(nil, id) \u003d dfdtop(flowid)) \u003d\u003e let mk_(nil, id) \u003d dfdtop(flowid) in (is_(id, DEFAULT`DFDId) or is_(id, DEFAULT`MSId))))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 834:44: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 let mk_(s, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in ((m \u003d \u003cREAD\u003e) \u003d\u003e (s in set (dom intm))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1786:47: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(nil, id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(id, nil):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, nil) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(fid, tid):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(fid, tid) \u003d dfdtop(flowid)) \u003d\u003e let mk_(fid, tid) \u003d dfdtop(flowid) in (is_(tid, DEFAULT`DFDId) or is_(tid, DEFAULT`MSId))))))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1072:26: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let mk_(call, pat):(DEFAULT`Call * [DEFAULT`Pattern]) \u003d MakeCallAndPat(nid, dfdsig(nid)), kind:(\u003cOPCALL\u003e | \u003cOPRES\u003e) \u003d FindKind(dfdsig(nid)) in ((not ((len piseq) \u003d 1)) \u003d\u003e let rest:DEFAULT`Stmt \u003d MakeStmtForEO((tl piseq), dfdid, dfdsig) in ((kind \u003d \u003cOPRES\u003e) \u003d\u003e (is_(pat, DEFAULT`PatternId) or is_(pat, DEFAULT`TuplePattern))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1653:18: (forall dfdtopo:map (DEFAULT`FlowId) to (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in is_(top, set of (((DEFAULT`DFDId | DEFAULT`MSId) * (DEFAULT`DFDId | DEFAULT`MSId)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1785:40: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(nil, id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(id, nil):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, nil) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(fid, tid):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(fid, tid) \u003d dfdtop(flowid)) \u003d\u003e let mk_(fid, tid) \u003d dfdtop(flowid) in (fid in set (dom dfdsig))))))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 645:47: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 651:42: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1066:39: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let mk_(call, pat):(DEFAULT`Call * [DEFAULT`Pattern]) \u003d MakeCallAndPat(nid, dfdsig(nid)), kind:(\u003cOPCALL\u003e | \u003cOPRES\u003e) \u003d FindKind(dfdsig(nid)) in (((len piseq) \u003d 1) \u003d\u003e let mk_(-, out, -):DEFAULT`Signature \u003d dfdsig(dfdid) in is_(out, seq1 of (DEFAULT`Id)))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1063:30: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 518:8: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, style:(\u003cEXPL\u003e | \u003cIMPL\u003e) \u0026 ((if (style \u003d \u003cEXPL\u003e)\nthen pre_MakeDFDExplOp(dfdid, dfdtopo, dfdsig)\nelse pre_MakeDFDImplOp(dfdid, dfdtopo, dfdsig)) \u003d\u003e ((not (style \u003d \u003cEXPL\u003e)) \u003d\u003e pre_MakeDFDImplOp(dfdid, dfdtopo, dfdsig))))","type invariant satisfiable obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1647:1: (exists dfdtopo:DEFAULT`DFDTopo \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in (NotRecursive(top) and (forall flowid in set (dom dfdtopo) \u0026 FlowConnectOK(dfdtopo(flowid)))))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 172:12: (forall ids:set of (DEFAULT`StId) \u0026 ((not (ids \u003d {})) \u003d\u003e (exists id in set ids \u0026 true)))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 786:39: (forall fs:set of (DEFAULT`FlowId), dst:DEFAULT`State, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, \u003cREADWRITE\u003e) in set (elems dst) \u0026 ((s in set (dom intm)) and (s in set (dom maxm)))) \u003d\u003e (forall i in set (inds dst) \u0026 (let mk_(-, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (m \u003d \u003cREADWRITE\u003e) \u003d\u003e (s in set (dom intm))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 745:47: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId)))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 124:17: (forall mk_(-, -, sl):DEFAULT`Signature \u0026 (forall i in set (inds sl) \u0026 (i in set (inds sl))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 118:28: (forall fidl:seq of (DEFAULT`FlowId) \u0026 ((not (0 \u003d (len fidl))) \u003d\u003e ((not (1 \u003d (len fidl))) \u003d\u003e is_([FlowIdTypeConf(fidl(i)) | i in set (inds fidl)], seq1 of (DEFAULT`Type)))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 744:13: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall m1, m2 in set {{stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid))} | stid in set (dom intm)} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4)))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 649:34: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (nid in set (dom dfdsig)))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 836:44: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 let mk_(s, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in ((not (m \u003d \u003cREAD\u003e)) \u003d\u003e (s in set (dom intm))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 751:15: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in pre_MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPOST\u003e, \u003cPOST\u003e)))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1023:14: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e (forall m1, m2 in set {{stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid))} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1777:51: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)) \u003d\u003e let mk_(mk_EPId(-), id) \u003d dfdtop(flowid) in (is_(id, DEFAULT`DFDId) or is_(id, DEFAULT`MSId)))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1062:42: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (nid in set (dom dfdsig))))","non-empty sequence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 117:29: (forall fidl:seq of (DEFAULT`FlowId) \u0026 ((not (0 \u003d (len fidl))) \u003d\u003e ((1 \u003d (len fidl)) \u003d\u003e (fidl \u003c\u003e []))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1070:18: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let mk_(call, pat):(DEFAULT`Call * [DEFAULT`Pattern]) \u003d MakeCallAndPat(nid, dfdsig(nid)), kind:(\u003cOPCALL\u003e | \u003cOPRES\u003e) \u003d FindKind(dfdsig(nid)) in ((not ((len piseq) \u003d 1)) \u003d\u003e pre_MakeStmtForEO((tl piseq), dfdid, dfdsig))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 649:41: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId)))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 241:50: (forall fidl:seq of (DEFAULT`FlowId) \u0026 ((not (0 \u003d (len fidl))) \u003d\u003e ((not (1 \u003d (len fidl))) \u003d\u003e (forall i in set (inds fidl) \u0026 (i in set (inds fidl))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1144:29: (forall dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, notneeded:set of (DEFAULT`FlowId), pids:set of (DEFAULT`ProcId) \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in ((not ((dom dfdsig) \u003d pids)) \u003d\u003e (forall pid in set ((dom dfdsig) \\ pids) \u0026 is_(top, set of (((DEFAULT`DFDId | DEFAULT`MSId) * (DEFAULT`DFDId | DEFAULT`MSId)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1068:27: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let mk_(call, pat):(DEFAULT`Call * [DEFAULT`Pattern]) \u003d MakeCallAndPat(nid, dfdsig(nid)), kind:(\u003cOPCALL\u003e | \u003cOPRES\u003e) \u003d FindKind(dfdsig(nid)) in (((len piseq) \u003d 1) \u003d\u003e let mk_(-, out, -):DEFAULT`Signature \u003d dfdsig(dfdid) in let ret:DEFAULT`Return \u003d mk_Return(MakeResult(out)) in ((kind \u003d \u003cOPRES\u003e) \u003d\u003e (is_(pat, DEFAULT`PatternId) or is_(pat, DEFAULT`TuplePattern))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1786:40: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(nil, id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(id, nil):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, nil) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(fid, tid):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(fid, tid) \u003d dfdtop(flowid)) \u003d\u003e let mk_(fid, tid) \u003d dfdtop(flowid) in (tid in set (dom dfdsig))))))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1315:39: (forall id:(DEFAULT`DSId | DEFAULT`Id), n:nat, max:nat, c:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((not ((max \u003d n) and (c \u003d \u003cPOST\u003e))) \u003d\u003e ((not (0 \u003d n)) \u003d\u003e ((not (1 \u003d n)) \u003d\u003e ((n - 1) \u003e\u003d 0)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1774:44: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)) \u003d\u003e let mk_(id, mk_EPId(-)) \u003d dfdtop(flowid) in (id in set (dom dfdsig))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1783:40: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(nil, id) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(id, nil):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(id, nil) \u003d dfdtop(flowid)) \u003d\u003e let mk_(id, nil) \u003d dfdtop(flowid) in (id in set (dom dfdsig)))))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1081:30: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, -):DEFAULT`Signature \u0026 (forall i in set (inds din) \u0026 (i in set (inds din))))","type invariant satisfiable obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1606:1: (exists mk_(hdfd, dd, -):DEFAULT`SA \u0026 (FlowTypeDefined(hdfd, dd) and TopLevelSigOK(hdfd)))","non-empty sequence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 240:39: (forall fidl:seq of (DEFAULT`FlowId) \u0026 ((not (0 \u003d (len fidl))) \u003d\u003e ((1 \u003d (len fidl)) \u003d\u003e (fidl \u003c\u003e []))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1026:27: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e let mk_(din, -, -):DEFAULT`Signature \u003d dfdsig(dfdid), eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo), intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (dfdid in set (dom dfdsig))))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1117:7: (forall op:DEFAULT`BinaryOp, es:set of (DEFAULT`Expr) \u0026 ((es \u003c\u003e {}) \u003d\u003e (exists e in set es \u0026 true)))","recursive function obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1201:8: (forall id:DEFAULT`Id, n:nat, max:nat \u0026 ((n \u003c\u003d max) \u003d\u003e ((not (n \u003d max)) \u003d\u003e (TowardsMax(id, n, max) \u003e TowardsMax((id ^ \"\u0027\"), (n + 1), max)))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 763:38: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) \u003d\u003e (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) \u003d\u003e (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId)))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 761:38: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) \u003d\u003e (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 841:34: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 (let mk_(-, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (m \u003d \u003cREADWRITE\u003e) \u003d\u003e let mk_(s, -):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (s in set (dom intm))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 843:29: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 (i in set (inds dst)))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 676:14: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let mk_(-, out, dst):DEFAULT`Signature \u003d dfdsig(dfdid), fids:set of (DEFAULT`FlowId) \u003d NeedsQuant(dfdtopo, dfdsig, (elems out), {}) in pre_MakeInExpr(out, dst, fids, dfdtopo, dfdsig, intm, maxm) \u003d\u003e pre_MakeInExpr(out, dst, fids, dfdtopo, dfdsig, intm, maxm)))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1842:13: (forall pid:(DEFAULT`DFDId | DEFAULT`MSId), top:set of (((DEFAULT`DFDId | DEFAULT`MSId) * (DEFAULT`DFDId | DEFAULT`MSId))), dset:set of ((DEFAULT`DFDId | DEFAULT`MSId)) \u0026 ((exists mk_(fromid, toid) in set top \u0026 (((fromid \u003d pid) or (fromid in set dset)) and (toid not in set dset))) \u003d\u003e (exists mk_(fromid, toid) in set top \u0026 (((fromid \u003d pid) or (fromid in set dset)) and (toid not in set dset)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 835:42: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 let mk_(s, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in ((m \u003d \u003cREAD\u003e) \u003d\u003e (s in set (dom maxm))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 208:32: (forall dfdsig:DEFAULT`DFDSig, mss:DEFAULT`MSs \u0026 ((not (forall id in set (dom dfdsig) \u0026 is_(id, DFDId))) \u003d\u003e (forall id in set (dom dfdsig) \u0026 (is_(id, MSId) \u003d\u003e ((not (id in set (dom mss))) \u003d\u003e is_(id, DEFAULT`MSId))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1032:14: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e let mk_(din, -, -):DEFAULT`Signature \u003d dfdsig(dfdid), eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo), intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in let optype:DEFAULT`OpType \u003d MakeOpType(dfdsig(dfdid)), parms:seq of (DEFAULT`PatternId) \u003d [mk_PatternId(FlowIdVarConf(din(i))) | i in set (inds din)], bodys:set of (DEFAULT`Stmt) \u003d {MakeStmtForEO(piseq, dfdid, dfdsig) | piseq in set eos}, dpre:DEFAULT`Expr \u003d MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) in pre_MakeNonDetStmt(bodys)))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1655:20: (forall dfdtopo:map (DEFAULT`FlowId) to (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in (NotRecursive(top) \u003d\u003e (forall flowid in set (dom dfdtopo) \u0026 (flowid in set (dom dfdtopo)))))","recursive function obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 174:26: (forall ids:set of (DEFAULT`StId) \u0026 ((not (ids \u003d {})) \u003d\u003e (forall id in set ids \u0026 (Card(ids) \u003e Card((ids \\ {id}))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1097:29: (forall idl:seq of (DEFAULT`Id) \u0026 ((not (0 \u003d (len idl))) \u003d\u003e ((not (1 \u003d (len idl))) \u003d\u003e is_([mk_PatternId(idl(i)) | i in set (inds idl)], seq1 of (DEFAULT`Pattern)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 646:28: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 ((mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)})) \u003d\u003e (stid in set (dom intm)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 749:34: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (nid in set (dom dfdsig))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1224:29: (forall top:set of ((DEFAULT`ProcId * DEFAULT`ProcId)), ids:set of ((DEFAULT`DFDId | DEFAULT`MSId)) \u0026 ((exists mk_(fid, tid) in set top \u0026 (((fid in set ids) and (tid not in set ids)) or ((tid in set ids) and (fid not in set ids)))) \u003d\u003e (forall mk_(fid, tid) in set top \u0026 ((((fid in set ids) and (tid not in set ids)) or ((tid in set ids) and (fid not in set ids))) \u003d\u003e is_((ids union {fid, tid}), set of ((DEFAULT`DFDId | DEFAULT`MSId)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 792:25: (forall fs:set of (DEFAULT`FlowId), dst:DEFAULT`State, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, \u003cREADWRITE\u003e) in set (elems dst) \u0026 ((s in set (dom intm)) and (s in set (dom maxm)))) \u003d\u003e let outl:seq of (DEFAULT`TypeBind) \u003d MakeTypeBindList(fs), stl:seq of (DEFAULT`TypeBind) \u003d [let mk_(s, -):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i), p:seq of (DEFAULT`PatternId) \u003d MakePatternIds(s, (intm(s) + 1), maxm(s), c) in mk_TypeBind(p, StateTypeConf(s)) | i in set (inds dst) \u0026 let mk_(-, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (m \u003d \u003cREADWRITE\u003e)] in is_((outl ^ stl), seq1 of (DEFAULT`TypeBind))))","non-empty sequence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 239:38: (forall fidl:seq of (DEFAULT`FlowId) \u0026 ((not (0 \u003d (len fidl))) \u003d\u003e ((1 \u003d (len fidl)) \u003d\u003e (fidl \u003c\u003e []))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 820:40: (forall dfdtopo:DEFAULT`DFDTopo \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or (is_(fid, MSId) or (fid \u003d nil))) and (is_(tid, DFDId) or (is_(tid, MSId) or (tid \u003d nil))))}, top2:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in let piset:set of ([DEFAULT`ProcId]) \u003d ((dunion {{pi_1, pi_2} | mk_(pi_1, pi_2) in set top}) \\ {nil}) in (forall piseq in set PossibleSeqs(piset) \u0026 (forall i, j in set (inds piseq) \u0026 ((j \u003c i) \u003d\u003e (i in set (inds piseq))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1027:43: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e let mk_(din, -, -):DEFAULT`Signature \u003d dfdsig(dfdid), eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo), intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (forall i in set (inds din) \u0026 (i in set (inds din)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 763:31: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) \u003d\u003e (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) \u003d\u003e (nid in set (dom dfdsig)))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 751:42: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 786:49: (forall fs:set of (DEFAULT`FlowId), dst:DEFAULT`State, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, \u003cREADWRITE\u003e) in set (elems dst) \u0026 ((s in set (dom intm)) and (s in set (dom maxm)))) \u003d\u003e (forall i in set (inds dst) \u0026 (let mk_(-, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (m \u003d \u003cREADWRITE\u003e) \u003d\u003e (s in set (dom maxm))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1097:43: (forall idl:seq of (DEFAULT`Id) \u0026 ((not (0 \u003d (len idl))) \u003d\u003e ((not (1 \u003d (len idl))) \u003d\u003e (forall i in set (inds idl) \u0026 (i in set (inds idl))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1164:34: (forall out:seq of (DEFAULT`FlowId), dst:DEFAULT`State, fids:set of (DEFAULT`FlowId), intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 ((forall mk_(s, -) in set (elems dst) \u0026 ((s in set (dom intm)) and (s in set (dom maxm)))) \u003d\u003e ((not (fids \u003c\u003e {})) \u003d\u003e (forall mk_(s, m) in set (elems dst) \u0026 ((m \u003d \u003cREADWRITE\u003e) \u003d\u003e (s in set (dom maxm)))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 603:21: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 ((dfdid in set (dom dfdsig)) \u003d\u003e let mk_(-, out, dst):DEFAULT`Signature \u003d dfdsig(dfdid) in let fids:set of (DEFAULT`FlowId) \u003d NeedsQuant(dfdtopo, dfdsig, {}, {}), pred:DEFAULT`Expr \u003d MakePrePred(dfdtopo, dfdsig, intm, maxm) in (QuantNec(out, dst, fids, intm, maxm) \u003d\u003e pre_MakeExistsBind(fids, dst, intm, maxm, \u003cPRE\u003e))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 599:22: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 ((dfdid in set (dom dfdsig)) \u003d\u003e (dfdid in set (dom dfdsig))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 517:8: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, style:(\u003cEXPL\u003e | \u003cIMPL\u003e) \u0026 ((if (style \u003d \u003cEXPL\u003e)\nthen pre_MakeDFDExplOp(dfdid, dfdtopo, dfdsig)\nelse pre_MakeDFDImplOp(dfdid, dfdtopo, dfdsig)) \u003d\u003e ((style \u003d \u003cEXPL\u003e) \u003d\u003e pre_MakeDFDExplOp(dfdid, dfdtopo, dfdsig))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 525:24: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and pre_MakeImplOpBody(dfdid, dfdtopo, dfdsig)) \u003d\u003e (dfdid in set (dom dfdsig))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 749:30: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1260:12: (forall sigs:set of (DEFAULT`Signature), stid:DEFAULT`StId \u0026 ((not (sigs \u003d {})) \u003d\u003e (exists sig in set sigs \u0026 true)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 751:31: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1035:16: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 ((dfdid in set (dom dfdsig)) \u003d\u003e (forall m1, m2 in set {{stid |-\u003e 0} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4)))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1082:31: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, -):DEFAULT`Signature \u0026 (forall i in set (inds out) \u0026 (i in set (inds out))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1193:18: (forall id:(DEFAULT`DSId | DEFAULT`Id), n:nat, max:nat, c:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((not ((n \u003d max) and (c \u003d \u003cPOST\u003e))) \u003d\u003e ((not (0 \u003d n)) \u003d\u003e pre_MakePatternSeq(StateVarConf(id), n, max))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1105:28: (forall idl:seq1 of (DEFAULT`Id) \u0026 ((not ((len idl) \u003d 1)) \u003d\u003e is_([FlowIdVarConf(idl(i)) | i in set (inds idl)], seq1 of (DEFAULT`Expr))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1131:30: (forall dfdtopo:DEFAULT`DFDTopo \u0026 (forall fid in set (dom dfdtopo) \u0026 (fid in set (dom dfdtopo))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1065:26: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let mk_(call, pat):(DEFAULT`Call * [DEFAULT`Pattern]) \u003d MakeCallAndPat(nid, dfdsig(nid)), kind:(\u003cOPCALL\u003e | \u003cOPRES\u003e) \u003d FindKind(dfdsig(nid)) in (((len piseq) \u003d 1) \u003d\u003e (dfdid in set (dom dfdsig)))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 225:43: (forall fidl:seq of (DEFAULT`FlowId) \u0026 (forall i in set (inds fidl) \u0026 (i in set (inds fidl))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 568:16: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall m1, m2 in set {{stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid))} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 819:27: (forall dfdtopo:DEFAULT`DFDTopo \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or (is_(fid, MSId) or (fid \u003d nil))) and (is_(tid, DFDId) or (is_(tid, MSId) or (tid \u003d nil))))}, top2:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in let piset:set of ([DEFAULT`ProcId]) \u003d ((dunion {{pi_1, pi_2} | mk_(pi_1, pi_2) in set top}) \\ {nil}) in (forall piseq in set PossibleSeqs(piset) \u0026 (forall i, j in set (inds piseq) \u0026 ((j \u003c i) \u003d\u003e (j in set (inds piseq))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1783:47: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(nil, id) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(id, nil):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(id, nil) \u003d dfdtop(flowid)) \u003d\u003e let mk_(id, nil) \u003d dfdtop(flowid) in (is_(id, DEFAULT`DFDId) or is_(id, DEFAULT`MSId)))))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1164:26: (forall out:seq of (DEFAULT`FlowId), dst:DEFAULT`State, fids:set of (DEFAULT`FlowId), intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 ((forall mk_(s, -) in set (elems dst) \u0026 ((s in set (dom intm)) and (s in set (dom maxm)))) \u003d\u003e ((not (fids \u003c\u003e {})) \u003d\u003e (forall mk_(s, m) in set (elems dst) \u0026 ((m \u003d \u003cREADWRITE\u003e) \u003d\u003e (s in set (dom intm)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1785:47: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(nil, id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(id, nil):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, nil) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(fid, tid):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(fid, tid) \u003d dfdtop(flowid)) \u003d\u003e let mk_(fid, tid) \u003d dfdtop(flowid) in (is_(fid, DEFAULT`DFDId) or is_(fid, DEFAULT`MSId))))))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 785:27: (forall fs:set of (DEFAULT`FlowId), dst:DEFAULT`State, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, \u003cREADWRITE\u003e) in set (elems dst) \u0026 ((s in set (dom intm)) and (s in set (dom maxm)))) \u003d\u003e (forall i in set (inds dst) \u0026 (let mk_(-, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (m \u003d \u003cREADWRITE\u003e) \u003d\u003e (i in set (inds dst))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1780:46: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(nil, id) \u003d dfdtop(flowid)) \u003d\u003e let mk_(nil, id) \u003d dfdtop(flowid) in (id in set (dom dfdsig))))))))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1220:14: (forall top:set of ((DEFAULT`ProcId * DEFAULT`ProcId)), ids:set of ((DEFAULT`DFDId | DEFAULT`MSId)) \u0026 ((exists mk_(fid, tid) in set top \u0026 (((fid in set ids) and (tid not in set ids)) or ((tid in set ids) and (fid not in set ids)))) \u003d\u003e (exists mk_(fid, tid) in set top \u0026 (((fid in set ids) and (tid not in set ids)) or ((tid in set ids) and (fid not in set ids))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 747:28: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 ((not (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))) \u003d\u003e (stid in set (dom intm))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 756:28: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in let dpre:DEFAULT`Apply \u003d MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPOST\u003e, \u003cPRE\u003e), dpost:DEFAULT`Apply \u003d MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPOST\u003e, \u003cPOST\u003e) in ((not ((len piseq) \u003d 1)) \u003d\u003e let pred:DEFAULT`BinaryExpr \u003d mk_BinaryExpr(dpre, \u003cAND\u003e, dpost) in pre_MakePostForEO((tl piseq), dfdsig, intm\u0027, maxm))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 76:18: (forall dfdid:DEFAULT`DFDId, dss:DEFAULT`DSs, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, dfdmap:DEFAULT`DFDMap \u0026 ((dfdid in set (dom dfdsig)) \u003d\u003e pre_MakeDFDModImps((dom dfdmap), dfdsig)))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1812:29: (forall id:DEFAULT`DFDId, top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])), dfdmap:DEFAULT`DFDMap, dfdsig:DEFAULT`DFDSig \u0026 (forall dfdid in set (dom dfdmap) \u0026 (dfdid in set (dom dfdmap))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1328:23: (forall id:(DEFAULT`DSId | DEFAULT`FlowId) \u0026 ((not is_(id, DSId)) \u003d\u003e is_(id, seq of (char))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 602:8: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 ((dfdid in set (dom dfdsig)) \u003d\u003e let mk_(-, out, dst):DEFAULT`Signature \u003d dfdsig(dfdid) in let fids:set of (DEFAULT`FlowId) \u003d NeedsQuant(dfdtopo, dfdsig, {}, {}), pred:DEFAULT`Expr \u003d MakePrePred(dfdtopo, dfdsig, intm, maxm) in pre_QuantNec(out, dst, fids, intm, maxm)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 681:21: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let mk_(-, out, dst):DEFAULT`Signature \u003d dfdsig(dfdid), fids:set of (DEFAULT`FlowId) \u003d NeedsQuant(dfdtopo, dfdsig, (elems out), {}) in pre_MakeInExpr(out, dst, fids, dfdtopo, dfdsig, intm, maxm) \u003d\u003e let mk_(-, out, dst):DEFAULT`Signature \u003d dfdsig(dfdid), fids:set of (DEFAULT`FlowId) \u003d NeedsQuant(dfdtopo, dfdsig, (elems out), {}), body:DEFAULT`Expr \u003d MakeInExpr(out, dst, fids, dfdtopo, dfdsig, intm, maxm) in ((not ((len out) \u003c\u003d 1)) \u003d\u003e (is_(MakePattern(out), DEFAULT`PatternId) or is_(MakePattern(out), DEFAULT`TuplePattern)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1018:22: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e (dfdid in set (dom dfdsig))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 790:28: (forall fs:set of (DEFAULT`FlowId), dst:DEFAULT`State, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, \u003cREADWRITE\u003e) in set (elems dst) \u0026 ((s in set (dom intm)) and (s in set (dom maxm)))) \u003d\u003e (forall i in set (inds dst) \u0026 (i in set (inds dst)))))"] \ No newline at end of file +["legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 77:29: (forall dfdid:DEFAULT`DFDId, dss:DEFAULT`DSs, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, dfdmap:DEFAULT`DFDMap \u0026 ((dfdid in set (dom dfdsig)) \u003d\u003e (dfdid in set (dom dfdsig))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 241:34: (forall fidl:seq of (DEFAULT`FlowId) \u0026 ((not (0 \u003d (len fidl))) \u003d\u003e ((not (1 \u003d (len fidl))) \u003d\u003e is_([FlowIdTypeConf(fidl(i)) | i in set (inds fidl)], seq1 of (DEFAULT`Type)))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 649:14: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in pre_MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPRE\u003e, \u003cPRE\u003e))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1205:3: (forall -:DEFAULT`Id, n:nat, max:nat \u0026 ((max - n) \u003e\u003d 0))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 651:31: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId)))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1148:31: (forall dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, notneeded:set of (DEFAULT`FlowId), pids:set of (DEFAULT`ProcId) \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in ((not ((dom dfdsig) \u003d pids)) \u003d\u003e (forall pid in set ((dom dfdsig) \\ pids) \u0026 ((not ((TransClosure(pid, top, {}) \u003d {}) and (EquivClass(top, {pid}) \u003d (dom dfdsig)))) \u003d\u003e (pid in set (dom dfdsig))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 761:31: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) \u003d\u003e (nid in set (dom dfdsig))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1145:23: (forall dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, notneeded:set of (DEFAULT`FlowId), pids:set of (DEFAULT`ProcId) \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in ((not ((dom dfdsig) \u003d pids)) \u003d\u003e (forall pid in set ((dom dfdsig) \\ pids) \u0026 ((TransClosure(pid, top, {}) \u003d {}) \u003d\u003e is_(top, set of ((DEFAULT`ProcId * DEFAULT`ProcId)))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1440:16: (forall id:(DEFAULT`DFDId | DEFAULT`DSId | DEFAULT`EPId | DEFAULT`Id | DEFAULT`MSId) \u0026 let realid:(DEFAULT`DFDId | DEFAULT`DSId | DEFAULT`EPId | DEFAULT`Id | DEFAULT`MSId | seq of (char)) \u003d (cases id :\nmk_DSId(id\u0027) -\u003e id\u0027,\nmk_DFDId(id\u0027) -\u003e id\u0027,\nmk_EPId(id\u0027) -\u003e id\u0027,\nmk_MSId(id\u0027) -\u003e id\u0027\nothers id\n end) in (forall i in set (inds realid) \u0026 (i in set (inds realid))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 118:45: (forall fidl:seq of (DEFAULT`FlowId) \u0026 ((not (0 \u003d (len fidl))) \u003d\u003e ((not (1 \u003d (len fidl))) \u003d\u003e (forall i in set (inds fidl) \u0026 (i in set (inds fidl))))))","non-empty sequence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1096:27: (forall idl:seq of (DEFAULT`Id) \u0026 ((not (0 \u003d (len idl))) \u003d\u003e ((1 \u003d (len idl)) \u003d\u003e (idl \u003c\u003e []))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 40:11: (forall mk_(dfdid, dss, dfdtopo, dfdmap, dfdsig):DEFAULT`HDFD, mss:DEFAULT`MSs, style:(\u003cEXPL\u003e | \u003cIMPL\u003e) \u0026 pre_MakeInterface(dfdid, dss, dfdtopo, dfdsig, dfdmap))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 837:42: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 let mk_(s, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in ((not (m \u003d \u003cREAD\u003e)) \u003d\u003e (s in set (dom maxm))))))","cases exhaustive obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1773:4: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 (((((exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (dfdtop(flowid) \u003d mk_(id, mk_EPId(any1)))) or (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (dfdtop(flowid) \u003d mk_(mk_EPId(any2), id)))) or (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (dfdtop(flowid) \u003d mk_(nil, id)))) or (exists mk_(id, nil):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (dfdtop(flowid) \u003d mk_(id, nil)))) or (exists mk_(fid, tid):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (dfdtop(flowid) \u003d mk_(fid, tid))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 649:30: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId)))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 749:14: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in pre_MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPOST\u003e, \u003cPRE\u003e)))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 832:32: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 (i in set (inds dst)))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1105:43: (forall idl:seq1 of (DEFAULT`Id) \u0026 ((not ((len idl) \u003d 1)) \u003d\u003e (forall i in set (inds idl) \u0026 (i in set (inds idl)))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 820:40: (forall dfdtopo:DEFAULT`DFDTopo \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or (is_(fid, MSId) or (fid \u003d nil))) and (is_(tid, DFDId) or (is_(tid, MSId) or (tid \u003d nil))))}, top2:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in let piset:set of ([DEFAULT`ProcId]) \u003d ((dunion {{pi_1, pi_2} | mk_(pi_1, pi_2) in set top}) \\ {nil}) in (forall piseq in set PossibleSeqs(piset) \u0026 (forall i, j in set (inds piseq) \u0026 ((j \u003c i) \u003d\u003e (is_(piseq(i), DEFAULT`DFDId) or is_(piseq(i), DEFAULT`MSId))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 851:26: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 (forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (s in set (dom intm)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 746:28: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 ((mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)})) \u003d\u003e (stid in set (dom intm))))))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 204:12: (forall dfdsig:DEFAULT`DFDSig, mss:DEFAULT`MSs \u0026 ((not (forall id in set (dom dfdsig) \u0026 is_(id, DFDId))) \u003d\u003e (exists id in set (dom dfdsig) \u0026 is_(id, MSId))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 529:14: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and pre_MakeImplOpBody(dfdid, dfdtopo, dfdsig)) \u003d\u003e let mk_(din, out, dst):DEFAULT`Signature \u003d dfdsig(dfdid) in pre_MakeImplOpBody(dfdid, dfdtopo, dfdsig)))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1120:28: (forall op:DEFAULT`BinaryOp, es:set of (DEFAULT`Expr) \u0026 ((es \u003c\u003e {}) \u003d\u003e (forall e in set es \u0026 ((not ((card es) \u003d 1)) \u003d\u003e pre_DBinOp(op, (es \\ {e}))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 651:15: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in pre_MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPRE\u003e, \u003cPOST\u003e))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1172:11: (forall fids:set of (DEFAULT`FlowId) \u0026 ((not (fids \u003d {})) \u003d\u003e (exists fid in set fids \u0026 true)))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1767:18: (forall dss:DEFAULT`DSs, dfdsig:DEFAULT`DFDSig \u0026 (forall dsid in set dss \u0026 (forall mk_(-, -, dst) in set (rng dfdsig) \u0026 (forall i in set (inds dst) \u0026 (i in set (inds dst))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 724:18: (forall dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo) in (forall piseq in set eos \u0026 pre_MakePostForEO(piseq, dfdsig, intm, maxm)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 763:27: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) \u003d\u003e (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) \u003d\u003e (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId)))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1037:16: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 ((dfdid in set (dom dfdsig)) \u003d\u003e (forall m1, m2 in set {{stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid))} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4)))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 624:3: (forall dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo) in pre_DBinOp(\u003cOR\u003e, {MakePreForEO(piseq, dfdsig, intm, maxm) | piseq in set eos}))","recursive function obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1177:19: (forall fids:set of (DEFAULT`FlowId) \u0026 ((not (fids \u003d {})) \u003d\u003e (forall fid in set fids \u0026 let pat:seq1 of (DEFAULT`PatternId) \u003d [mk_PatternId(FlowIdVarConf(fid))], first:DEFAULT`TypeBind \u003d mk_TypeBind(pat, FlowIdTypeConf(fid)) in (CardFId(fids) \u003e CardFId((fids \\ {fid}))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1777:44: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)) \u003d\u003e let mk_(mk_EPId(-), id) \u003d dfdtop(flowid) in (id in set (dom dfdsig)))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 208:35: (forall dfdsig:DEFAULT`DFDSig, mss:DEFAULT`MSs \u0026 ((not (forall id in set (dom dfdsig) \u0026 is_(id, DFDId))) \u003d\u003e (forall id in set (dom dfdsig) \u0026 (is_(id, MSId) \u003d\u003e ((not (id in set (dom mss))) \u003d\u003e (id in set (dom dfdsig)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1266:1: (forall n:nat \u0026 ((if ((n \u003d 0) or (n \u003d 1))\nthen n\nelse (n - 1)) \u003e\u003d 0))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1143:13: (forall dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, notneeded:set of (DEFAULT`FlowId), pids:set of (DEFAULT`ProcId) \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in ((not ((dom dfdsig) \u003d pids)) \u003d\u003e (exists pid in set ((dom dfdsig) \\ pids) \u0026 true)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1322:22: (forall id:DEFAULT`StId \u0026 ((not is_(id, DSId)) \u003d\u003e is_(id, seq of (char))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1813:6: (forall id:DEFAULT`DFDId, top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])), dfdmap:DEFAULT`DFDMap, dfdsig:DEFAULT`DFDSig \u0026 (forall dfdid in set (dom dfdmap) \u0026 let mk_(-, -, -, -, dfdsig\u0027):DEFAULT`HDFD \u003d dfdmap(dfdid) in (dfdid in set (dom dfdsig\u0027))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 566:16: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall m1, m2 in set {{stid |-\u003e 0} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1070:33: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let mk_(call, pat):(DEFAULT`Call * [DEFAULT`Pattern]) \u003d MakeCallAndPat(nid, dfdsig(nid)), kind:(\u003cOPCALL\u003e | \u003cOPRES\u003e) \u003d FindKind(dfdsig(nid)) in ((not ((len piseq) \u003d 1)) \u003d\u003e is_((tl piseq), seq1 of (DEFAULT`ProcId)))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 224:42: (forall fidl:seq of (DEFAULT`FlowId) \u0026 (forall i in set (inds fidl) \u0026 (i in set (inds fidl))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 647:28: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 ((not (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))) \u003d\u003e (stid in set (dom intm)))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 142:1: (forall dfdid:DEFAULT`DFDId, dss:DEFAULT`DSs, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, mss:DEFAULT`MSs, style:(\u003cEXPL\u003e | \u003cIMPL\u003e) \u0026 is_(let dst:[DEFAULT`StateDef] \u003d MakeState(dfdid, dss, CollectExtDFs(dfdtopo)), msdescs:set of (DEFAULT`Definition) \u003d MakeMSDescs(dfdsig, mss), dfdop:DEFAULT`OpDef \u003d MakeDFDOp(dfdid, dfdtopo, dfdsig, style) in (if (dst \u003d nil)\nthen ({dfdop} union msdescs)\nelse ({dst, dfdop} union msdescs)), set of (DEFAULT`Definition)))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 674:22: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let mk_(-, out, dst):DEFAULT`Signature \u003d dfdsig(dfdid), fids:set of (DEFAULT`FlowId) \u003d NeedsQuant(dfdtopo, dfdsig, (elems out), {}) in pre_MakeInExpr(out, dst, fids, dfdtopo, dfdsig, intm, maxm) \u003d\u003e (dfdid in set (dom dfdsig))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 207:25: (forall dfdsig:DEFAULT`DFDSig, mss:DEFAULT`MSs \u0026 ((not (forall id in set (dom dfdsig) \u0026 is_(id, DFDId))) \u003d\u003e (forall id in set (dom dfdsig) \u0026 (is_(id, MSId) \u003d\u003e ((id in set (dom mss)) \u003d\u003e (id in set (dom mss)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 659:38: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in let dpre:DEFAULT`Apply \u003d MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPRE\u003e, \u003cPRE\u003e), dpost:DEFAULT`Apply \u003d MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPRE\u003e, \u003cPOST\u003e) in ((not ((len piseq) \u003d 1)) \u003d\u003e let pred:DEFAULT`BinaryExpr \u003d mk_BinaryExpr(dpre, \u003cAND\u003e, dpost) in is_((tl piseq), seq1 of (DEFAULT`ProcId))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 804:1: (forall dfdtopo:DEFAULT`DFDTopo \u0026 is_(let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or (is_(fid, MSId) or (fid \u003d nil))) and (is_(tid, DFDId) or (is_(tid, MSId) or (tid \u003d nil))))}, top2:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in let piset:set of ([DEFAULT`ProcId]) \u003d ((dunion {{pi_1, pi_2} | mk_(pi_1, pi_2) in set top}) \\ {nil}) in {piseq | piseq in set PossibleSeqs(piset) \u0026 (forall i, j in set (inds piseq) \u0026 ((j \u003c i) \u003d\u003e (piseq(j) not in set TransClosure(piseq(i), top2, {}))))}, set of (seq1 of (DEFAULT`ProcId))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 644:13: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall m1, m2 in set {{stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid))} | stid in set (dom intm)} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 682:24: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (dfdid in set (dom dfdsig)))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 147:15: (forall dfdid:DEFAULT`DFDId, dss:DEFAULT`DSs, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, mss:DEFAULT`MSs, style:(\u003cEXPL\u003e | \u003cIMPL\u003e) \u0026 pre_MakeDFDOp(dfdid, dfdtopo, dfdsig, style))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1029:16: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e let mk_(din, -, -):DEFAULT`Signature \u003d dfdsig(dfdid), eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo), intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (forall piseq in set eos \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig))))","recursive function obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1366:26: (forall pids:set of (DEFAULT`ProcId) \u0026 ((not (pids \u003d {})) \u003d\u003e ((not ((card pids) \u003d 1)) \u003d\u003e (forall pid in set pids \u0026 (CardPSet(pids) \u003e CardPSet((pids \\ {pid})))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1738:22: (forall mk_(sysid, -, dfdtop, -, dfdsig):DEFAULT`HDFD \u0026 ((sysid in set (dom dfdsig)) \u003d\u003e let mk_(din, out, dst):DEFAULT`Signature \u003d dfdsig(sysid) in ((din \u003d []) \u003d\u003e ((out \u003d []) \u003d\u003e (forall flowid in set (dom dfdtop) \u0026 (flowid in set (dom dfdtop)))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 831:30: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds din) \u0026 (i in set (inds din)))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1031:15: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e let mk_(din, -, -):DEFAULT`Signature \u003d dfdsig(dfdid), eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo), intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm)))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1201:8: (forall id:DEFAULT`Id, n:nat, max:nat \u0026 ((n \u003c\u003d max) \u003d\u003e ((not (n \u003d max)) \u003d\u003e pre_MakePatternSeq((id ^ \"\u0027\"), (n + 1), max))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 751:35: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (nid in set (dom dfdsig))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1063:23: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (nid in set (dom dfdsig))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1735:24: (forall mk_(sysid, -, dfdtop, -, dfdsig):DEFAULT`HDFD \u0026 ((sysid in set (dom dfdsig)) \u003d\u003e (sysid in set (dom dfdsig))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 724:5: (forall dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo) in pre_DBinOp(\u003cOR\u003e, {MakePostForEO(piseq, dfdsig, intm, maxm) | piseq in set eos}))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 645:40: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 (nid in set (dom dfdsig))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 91:36: (forall dfdids:set of (DEFAULT`DFDId), dfdsig:DEFAULT`DFDSig \u0026 ((dfdids subset (dom dfdsig)) \u003d\u003e (forall id in set dfdids \u0026 (id in set (dom dfdsig)))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 563:15: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and pre_MakePostExpr(dfdid, dfdtopo, dfdsig, intm, maxm)) \u003d\u003e pre_MakePostExpr(dfdid, dfdtopo, dfdsig, intm, maxm)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 836:52: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 let mk_(s, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in ((not (m \u003d \u003cREAD\u003e)) \u003d\u003e ((intm(s) - 1) \u003e\u003d 0)))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 840:29: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 (let mk_(-, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (m \u003d \u003cREADWRITE\u003e) \u003d\u003e (i in set (inds dst))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 701:8: (forall out:seq of (DEFAULT`FlowId), dst:DEFAULT`State, fids:set of (DEFAULT`FlowId), dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (pre_MakeExistsBind(fids, dst, intm, maxm, \u003cPOST\u003e) \u003d\u003e let pred:DEFAULT`Expr \u003d MakePostPred(dfdtopo, dfdsig, intm, maxm) in pre_QuantNec(out, dst, fids, intm, maxm)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 820:49: (forall dfdtopo:DEFAULT`DFDTopo \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or (is_(fid, MSId) or (fid \u003d nil))) and (is_(tid, DFDId) or (is_(tid, MSId) or (tid \u003d nil))))}, top2:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in let piset:set of ([DEFAULT`ProcId]) \u003d ((dunion {{pi_1, pi_2} | mk_(pi_1, pi_2) in set top}) \\ {nil}) in (forall piseq in set PossibleSeqs(piset) \u0026 (forall i, j in set (inds piseq) \u0026 ((j \u003c i) \u003d\u003e is_(top2, set of (((DEFAULT`DFDId | DEFAULT`MSId) * (DEFAULT`DFDId | DEFAULT`MSId))))))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1020:14: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e (forall m1, m2 in set {{stid |-\u003e 0} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 207:29: (forall dfdsig:DEFAULT`DFDSig, mss:DEFAULT`MSs \u0026 ((not (forall id in set (dom dfdsig) \u0026 is_(id, DFDId))) \u003d\u003e (forall id in set (dom dfdsig) \u0026 (is_(id, MSId) \u003d\u003e ((id in set (dom mss)) \u003d\u003e is_(id, DEFAULT`MSId))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 749:41: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 745:40: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 (nid in set (dom dfdsig)))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1288:1: (forall id:(DEFAULT`DFDId | DEFAULT`Id | DEFAULT`MSId) \u0026 is_((cases id :\nmk_MSId(id\u0027) -\u003e id\u0027,\nmk_DFDId(id\u0027) -\u003e id\u0027\nothers id\n end), seq of (char)))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 559:14: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and pre_MakePostExpr(dfdid, dfdtopo, dfdsig, intm, maxm)) \u003d\u003e (forall m1, m2 in set {{stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid))} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4)))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 651:35: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (nid in set (dom dfdsig)))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 839:31: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds out) \u0026 (i in set (inds out)))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 249:15: (forall dst:DEFAULT`State \u0026 (forall i in set (inds dst) \u0026 (i in set (inds dst))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 702:21: (forall out:seq of (DEFAULT`FlowId), dst:DEFAULT`State, fids:set of (DEFAULT`FlowId), dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (pre_MakeExistsBind(fids, dst, intm, maxm, \u003cPOST\u003e) \u003d\u003e let pred:DEFAULT`Expr \u003d MakePostPred(dfdtopo, dfdsig, intm, maxm) in (QuantNec(out, dst, fids, intm, maxm) \u003d\u003e pre_MakeExistsBind(fids, dst, intm, maxm, \u003cPOST\u003e))))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1364:17: (forall pids:set of (DEFAULT`ProcId) \u0026 ((not (pids \u003d {})) \u003d\u003e ((not ((card pids) \u003d 1)) \u003d\u003e (exists pid in set pids \u0026 true))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 761:27: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) \u003d\u003e (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1062:49: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1391:16: (forall id:(DEFAULT`DFDId | DEFAULT`DSId | DEFAULT`EPId | DEFAULT`Id | DEFAULT`MSId) \u0026 let realid:(DEFAULT`DFDId | DEFAULT`DSId | DEFAULT`EPId | DEFAULT`Id | DEFAULT`MSId | seq of (char)) \u003d (cases id :\nmk_DSId(id\u0027) -\u003e id\u0027,\nmk_DFDId(id\u0027) -\u003e id\u0027,\nmk_EPId(id\u0027) -\u003e id\u0027,\nmk_MSId(id\u0027) -\u003e id\u0027\nothers id\n end) in (forall i in set (inds realid) \u0026 (i in set (inds realid))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1774:51: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)) \u003d\u003e let mk_(id, mk_EPId(-)) \u003d dfdtop(flowid) in (is_(id, DEFAULT`DFDId) or is_(id, DEFAULT`MSId))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 562:15: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and pre_MakePostExpr(dfdid, dfdtopo, dfdsig, intm, maxm)) \u003d\u003e pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 817:42: (forall dfdtopo:DEFAULT`DFDTopo \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or (is_(fid, MSId) or (fid \u003d nil))) and (is_(tid, DFDId) or (is_(tid, MSId) or (tid \u003d nil))))}, top2:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in let piset:set of ([DEFAULT`ProcId]) \u003d ((dunion {{pi_1, pi_2} | mk_(pi_1, pi_2) in set top}) \\ {nil}) in is_(piset, set of (DEFAULT`ProcId)))","type invariant satisfiable obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1672:1: (exists mk_(-, out, sta):DEFAULT`Signature \u0026 ((sta \u003d []) \u003d\u003e (((out \u003c\u003e []) and (out \u003d [])) \u003d\u003e (exists mk_(-, m) in set (elems sta) \u0026 (m \u003d \u003cREADWRITE\u003e)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 841:42: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 (let mk_(-, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (m \u003d \u003cREADWRITE\u003e) \u003d\u003e let mk_(s, -):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (s in set (dom maxm))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1062:38: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1813:21: (forall id:DEFAULT`DFDId, top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])), dfdmap:DEFAULT`DFDMap, dfdsig:DEFAULT`DFDSig \u0026 (forall dfdid in set (dom dfdmap) \u0026 let mk_(-, -, -, -, dfdsig\u0027):DEFAULT`HDFD \u003d dfdmap(dfdid) in (dfdid in set (dom dfdsig))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 557:14: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and pre_MakePostExpr(dfdid, dfdtopo, dfdsig, intm, maxm)) \u003d\u003e (forall m1, m2 in set {{stid |-\u003e 0} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1780:53: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(nil, id) \u003d dfdtop(flowid)) \u003d\u003e let mk_(nil, id) \u003d dfdtop(flowid) in (is_(id, DEFAULT`DFDId) or is_(id, DEFAULT`MSId))))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 834:44: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 let mk_(s, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in ((m \u003d \u003cREAD\u003e) \u003d\u003e (s in set (dom intm))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1786:47: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(nil, id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(id, nil):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, nil) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(fid, tid):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(fid, tid) \u003d dfdtop(flowid)) \u003d\u003e let mk_(fid, tid) \u003d dfdtop(flowid) in (is_(tid, DEFAULT`DFDId) or is_(tid, DEFAULT`MSId))))))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1072:26: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let mk_(call, pat):(DEFAULT`Call * [DEFAULT`Pattern]) \u003d MakeCallAndPat(nid, dfdsig(nid)), kind:(\u003cOPCALL\u003e | \u003cOPRES\u003e) \u003d FindKind(dfdsig(nid)) in ((not ((len piseq) \u003d 1)) \u003d\u003e let rest:DEFAULT`Stmt \u003d MakeStmtForEO((tl piseq), dfdid, dfdsig) in ((kind \u003d \u003cOPRES\u003e) \u003d\u003e (is_(pat, DEFAULT`PatternId) or is_(pat, DEFAULT`TuplePattern))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1653:18: (forall dfdtopo:map (DEFAULT`FlowId) to (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in is_(top, set of (((DEFAULT`DFDId | DEFAULT`MSId) * (DEFAULT`DFDId | DEFAULT`MSId)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1785:40: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(nil, id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(id, nil):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, nil) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(fid, tid):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(fid, tid) \u003d dfdtop(flowid)) \u003d\u003e let mk_(fid, tid) \u003d dfdtop(flowid) in (fid in set (dom dfdsig))))))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 645:47: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 651:42: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1066:39: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let mk_(call, pat):(DEFAULT`Call * [DEFAULT`Pattern]) \u003d MakeCallAndPat(nid, dfdsig(nid)), kind:(\u003cOPCALL\u003e | \u003cOPRES\u003e) \u003d FindKind(dfdsig(nid)) in (((len piseq) \u003d 1) \u003d\u003e let mk_(-, out, -):DEFAULT`Signature \u003d dfdsig(dfdid) in is_(out, seq1 of (DEFAULT`Id)))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1063:30: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 518:8: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, style:(\u003cEXPL\u003e | \u003cIMPL\u003e) \u0026 ((if (style \u003d \u003cEXPL\u003e)\nthen pre_MakeDFDExplOp(dfdid, dfdtopo, dfdsig)\nelse pre_MakeDFDImplOp(dfdid, dfdtopo, dfdsig)) \u003d\u003e ((not (style \u003d \u003cEXPL\u003e)) \u003d\u003e pre_MakeDFDImplOp(dfdid, dfdtopo, dfdsig))))","type invariant satisfiable obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1647:1: (exists dfdtopo:DEFAULT`DFDTopo \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in (NotRecursive(top) and (forall flowid in set (dom dfdtopo) \u0026 FlowConnectOK(dfdtopo(flowid)))))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 172:12: (forall ids:set of (DEFAULT`StId) \u0026 ((not (ids \u003d {})) \u003d\u003e (exists id in set ids \u0026 true)))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 786:39: (forall fs:set of (DEFAULT`FlowId), dst:DEFAULT`State, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, \u003cREADWRITE\u003e) in set (elems dst) \u0026 ((s in set (dom intm)) and (s in set (dom maxm)))) \u003d\u003e (forall i in set (inds dst) \u0026 (let mk_(-, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (m \u003d \u003cREADWRITE\u003e) \u003d\u003e (s in set (dom intm))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 745:47: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId)))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 124:17: (forall mk_(-, -, sl):DEFAULT`Signature \u0026 (forall i in set (inds sl) \u0026 (i in set (inds sl))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 118:28: (forall fidl:seq of (DEFAULT`FlowId) \u0026 ((not (0 \u003d (len fidl))) \u003d\u003e ((not (1 \u003d (len fidl))) \u003d\u003e is_([FlowIdTypeConf(fidl(i)) | i in set (inds fidl)], seq1 of (DEFAULT`Type)))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 744:13: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall m1, m2 in set {{stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid))} | stid in set (dom intm)} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4)))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 649:34: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (nid in set (dom dfdsig)))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 836:44: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 let mk_(s, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in ((not (m \u003d \u003cREAD\u003e)) \u003d\u003e (s in set (dom intm))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 751:15: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in pre_MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPOST\u003e, \u003cPOST\u003e)))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1023:14: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e (forall m1, m2 in set {{stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid))} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1777:51: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)) \u003d\u003e let mk_(mk_EPId(-), id) \u003d dfdtop(flowid) in (is_(id, DEFAULT`DFDId) or is_(id, DEFAULT`MSId)))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1062:42: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (nid in set (dom dfdsig))))","non-empty sequence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 117:29: (forall fidl:seq of (DEFAULT`FlowId) \u0026 ((not (0 \u003d (len fidl))) \u003d\u003e ((1 \u003d (len fidl)) \u003d\u003e (fidl \u003c\u003e []))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1070:18: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let mk_(call, pat):(DEFAULT`Call * [DEFAULT`Pattern]) \u003d MakeCallAndPat(nid, dfdsig(nid)), kind:(\u003cOPCALL\u003e | \u003cOPRES\u003e) \u003d FindKind(dfdsig(nid)) in ((not ((len piseq) \u003d 1)) \u003d\u003e pre_MakeStmtForEO((tl piseq), dfdid, dfdsig))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 649:41: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId)))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 241:50: (forall fidl:seq of (DEFAULT`FlowId) \u0026 ((not (0 \u003d (len fidl))) \u003d\u003e ((not (1 \u003d (len fidl))) \u003d\u003e (forall i in set (inds fidl) \u0026 (i in set (inds fidl))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1144:29: (forall dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, notneeded:set of (DEFAULT`FlowId), pids:set of (DEFAULT`ProcId) \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in ((not ((dom dfdsig) \u003d pids)) \u003d\u003e (forall pid in set ((dom dfdsig) \\ pids) \u0026 is_(top, set of (((DEFAULT`DFDId | DEFAULT`MSId) * (DEFAULT`DFDId | DEFAULT`MSId)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1068:27: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let mk_(call, pat):(DEFAULT`Call * [DEFAULT`Pattern]) \u003d MakeCallAndPat(nid, dfdsig(nid)), kind:(\u003cOPCALL\u003e | \u003cOPRES\u003e) \u003d FindKind(dfdsig(nid)) in (((len piseq) \u003d 1) \u003d\u003e let mk_(-, out, -):DEFAULT`Signature \u003d dfdsig(dfdid) in let ret:DEFAULT`Return \u003d mk_Return(MakeResult(out)) in ((kind \u003d \u003cOPRES\u003e) \u003d\u003e (is_(pat, DEFAULT`PatternId) or is_(pat, DEFAULT`TuplePattern))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1786:40: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(nil, id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(id, nil):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, nil) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(fid, tid):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(fid, tid) \u003d dfdtop(flowid)) \u003d\u003e let mk_(fid, tid) \u003d dfdtop(flowid) in (tid in set (dom dfdsig))))))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1315:39: (forall id:(DEFAULT`DSId | DEFAULT`Id), n:nat, max:nat, c:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((not ((max \u003d n) and (c \u003d \u003cPOST\u003e))) \u003d\u003e ((not (0 \u003d n)) \u003d\u003e ((not (1 \u003d n)) \u003d\u003e ((n - 1) \u003e\u003d 0)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1774:44: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)) \u003d\u003e let mk_(id, mk_EPId(-)) \u003d dfdtop(flowid) in (id in set (dom dfdsig))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1783:40: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(nil, id) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(id, nil):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(id, nil) \u003d dfdtop(flowid)) \u003d\u003e let mk_(id, nil) \u003d dfdtop(flowid) in (id in set (dom dfdsig)))))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1081:30: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, -):DEFAULT`Signature \u0026 (forall i in set (inds din) \u0026 (i in set (inds din))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 756:42: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in let dpre:DEFAULT`Apply \u003d MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPOST\u003e, \u003cPRE\u003e), dpost:DEFAULT`Apply \u003d MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPOST\u003e, \u003cPOST\u003e) in ((not ((len piseq) \u003d 1)) \u003d\u003e let pred:DEFAULT`BinaryExpr \u003d mk_BinaryExpr(dpre, \u003cAND\u003e, dpost) in is_((tl piseq), seq1 of (DEFAULT`ProcId)))))","type invariant satisfiable obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1606:1: (exists mk_(hdfd, dd, -):DEFAULT`SA \u0026 (FlowTypeDefined(hdfd, dd) and TopLevelSigOK(hdfd)))","non-empty sequence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 240:39: (forall fidl:seq of (DEFAULT`FlowId) \u0026 ((not (0 \u003d (len fidl))) \u003d\u003e ((1 \u003d (len fidl)) \u003d\u003e (fidl \u003c\u003e []))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1026:27: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e let mk_(din, -, -):DEFAULT`Signature \u003d dfdsig(dfdid), eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo), intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (dfdid in set (dom dfdsig))))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1117:7: (forall op:DEFAULT`BinaryOp, es:set of (DEFAULT`Expr) \u0026 ((es \u003c\u003e {}) \u003d\u003e (exists e in set es \u0026 true)))","recursive function obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1201:8: (forall id:DEFAULT`Id, n:nat, max:nat \u0026 ((n \u003c\u003d max) \u003d\u003e ((not (n \u003d max)) \u003d\u003e (TowardsMax(id, n, max) \u003e TowardsMax((id ^ \"\u0027\"), (n + 1), max)))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 763:38: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) \u003d\u003e (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) \u003d\u003e (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId)))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 761:38: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) \u003d\u003e (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 841:34: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 (let mk_(-, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (m \u003d \u003cREADWRITE\u003e) \u003d\u003e let mk_(s, -):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (s in set (dom intm))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 843:29: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 (i in set (inds dst)))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 676:14: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let mk_(-, out, dst):DEFAULT`Signature \u003d dfdsig(dfdid), fids:set of (DEFAULT`FlowId) \u003d NeedsQuant(dfdtopo, dfdsig, (elems out), {}) in pre_MakeInExpr(out, dst, fids, dfdtopo, dfdsig, intm, maxm) \u003d\u003e pre_MakeInExpr(out, dst, fids, dfdtopo, dfdsig, intm, maxm)))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1842:13: (forall pid:(DEFAULT`DFDId | DEFAULT`MSId), top:set of (((DEFAULT`DFDId | DEFAULT`MSId) * (DEFAULT`DFDId | DEFAULT`MSId))), dset:set of ((DEFAULT`DFDId | DEFAULT`MSId)) \u0026 ((exists mk_(fromid, toid) in set top \u0026 (((fromid \u003d pid) or (fromid in set dset)) and (toid not in set dset))) \u003d\u003e (exists mk_(fromid, toid) in set top \u0026 (((fromid \u003d pid) or (fromid in set dset)) and (toid not in set dset)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 835:42: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, dst):DEFAULT`Signature, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e), c2:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, m) in set (elems dst) \u0026 (((s in set (dom intm)) and ((s in set (dom maxm)) and (m \u003d \u003cREADWRITE\u003e))) \u003d\u003e (intm(s) \u003e 0))) \u003d\u003e (forall i in set (inds dst) \u0026 let mk_(s, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in ((m \u003d \u003cREAD\u003e) \u003d\u003e (s in set (dom maxm))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 208:32: (forall dfdsig:DEFAULT`DFDSig, mss:DEFAULT`MSs \u0026 ((not (forall id in set (dom dfdsig) \u0026 is_(id, DFDId))) \u003d\u003e (forall id in set (dom dfdsig) \u0026 (is_(id, MSId) \u003d\u003e ((not (id in set (dom mss))) \u003d\u003e is_(id, DEFAULT`MSId))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1032:14: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e let mk_(din, -, -):DEFAULT`Signature \u003d dfdsig(dfdid), eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo), intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in let optype:DEFAULT`OpType \u003d MakeOpType(dfdsig(dfdid)), parms:seq of (DEFAULT`PatternId) \u003d [mk_PatternId(FlowIdVarConf(din(i))) | i in set (inds din)], bodys:set of (DEFAULT`Stmt) \u003d {MakeStmtForEO(piseq, dfdid, dfdsig) | piseq in set eos}, dpre:DEFAULT`Expr \u003d MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) in pre_MakeNonDetStmt(bodys)))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1655:20: (forall dfdtopo:map (DEFAULT`FlowId) to (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in (NotRecursive(top) \u003d\u003e (forall flowid in set (dom dfdtopo) \u0026 (flowid in set (dom dfdtopo)))))","recursive function obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 174:26: (forall ids:set of (DEFAULT`StId) \u0026 ((not (ids \u003d {})) \u003d\u003e (forall id in set ids \u0026 (Card(ids) \u003e Card((ids \\ {id}))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1097:29: (forall idl:seq of (DEFAULT`Id) \u0026 ((not (0 \u003d (len idl))) \u003d\u003e ((not (1 \u003d (len idl))) \u003d\u003e is_([mk_PatternId(idl(i)) | i in set (inds idl)], seq1 of (DEFAULT`Pattern)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 646:28: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 ((mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)})) \u003d\u003e (stid in set (dom intm)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 749:34: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (nid in set (dom dfdsig))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1224:29: (forall top:set of ((DEFAULT`ProcId * DEFAULT`ProcId)), ids:set of ((DEFAULT`DFDId | DEFAULT`MSId)) \u0026 ((exists mk_(fid, tid) in set top \u0026 (((fid in set ids) and (tid not in set ids)) or ((tid in set ids) and (fid not in set ids)))) \u003d\u003e (forall mk_(fid, tid) in set top \u0026 ((((fid in set ids) and (tid not in set ids)) or ((tid in set ids) and (fid not in set ids))) \u003d\u003e is_((ids union {fid, tid}), set of ((DEFAULT`DFDId | DEFAULT`MSId)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 792:25: (forall fs:set of (DEFAULT`FlowId), dst:DEFAULT`State, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, \u003cREADWRITE\u003e) in set (elems dst) \u0026 ((s in set (dom intm)) and (s in set (dom maxm)))) \u003d\u003e let outl:seq of (DEFAULT`TypeBind) \u003d MakeTypeBindList(fs), stl:seq of (DEFAULT`TypeBind) \u003d [let mk_(s, -):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i), p:seq of (DEFAULT`PatternId) \u003d MakePatternIds(s, (intm(s) + 1), maxm(s), c) in mk_TypeBind(p, StateTypeConf(s)) | i in set (inds dst) \u0026 let mk_(-, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (m \u003d \u003cREADWRITE\u003e)] in is_((outl ^ stl), seq1 of (DEFAULT`TypeBind))))","non-empty sequence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 239:38: (forall fidl:seq of (DEFAULT`FlowId) \u0026 ((not (0 \u003d (len fidl))) \u003d\u003e ((1 \u003d (len fidl)) \u003d\u003e (fidl \u003c\u003e []))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 820:40: (forall dfdtopo:DEFAULT`DFDTopo \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or (is_(fid, MSId) or (fid \u003d nil))) and (is_(tid, DFDId) or (is_(tid, MSId) or (tid \u003d nil))))}, top2:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in let piset:set of ([DEFAULT`ProcId]) \u003d ((dunion {{pi_1, pi_2} | mk_(pi_1, pi_2) in set top}) \\ {nil}) in (forall piseq in set PossibleSeqs(piset) \u0026 (forall i, j in set (inds piseq) \u0026 ((j \u003c i) \u003d\u003e (i in set (inds piseq))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1027:43: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e let mk_(din, -, -):DEFAULT`Signature \u003d dfdsig(dfdid), eos:set of (seq1 of (DEFAULT`ProcId)) \u003d ExecutionOrders(dfdtopo), intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (forall i in set (inds din) \u0026 (i in set (inds din)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 763:31: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) \u003d\u003e (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) \u003d\u003e (nid in set (dom dfdsig)))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 751:42: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 786:49: (forall fs:set of (DEFAULT`FlowId), dst:DEFAULT`State, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, \u003cREADWRITE\u003e) in set (elems dst) \u0026 ((s in set (dom intm)) and (s in set (dom maxm)))) \u003d\u003e (forall i in set (inds dst) \u0026 (let mk_(-, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (m \u003d \u003cREADWRITE\u003e) \u003d\u003e (s in set (dom maxm))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1097:43: (forall idl:seq of (DEFAULT`Id) \u0026 ((not (0 \u003d (len idl))) \u003d\u003e ((not (1 \u003d (len idl))) \u003d\u003e (forall i in set (inds idl) \u0026 (i in set (inds idl))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1164:34: (forall out:seq of (DEFAULT`FlowId), dst:DEFAULT`State, fids:set of (DEFAULT`FlowId), intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 ((forall mk_(s, -) in set (elems dst) \u0026 ((s in set (dom intm)) and (s in set (dom maxm)))) \u003d\u003e ((not (fids \u003c\u003e {})) \u003d\u003e (forall mk_(s, m) in set (elems dst) \u0026 ((m \u003d \u003cREADWRITE\u003e) \u003d\u003e (s in set (dom maxm)))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 603:21: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 ((dfdid in set (dom dfdsig)) \u003d\u003e let mk_(-, out, dst):DEFAULT`Signature \u003d dfdsig(dfdid) in let fids:set of (DEFAULT`FlowId) \u003d NeedsQuant(dfdtopo, dfdsig, {}, {}), pred:DEFAULT`Expr \u003d MakePrePred(dfdtopo, dfdsig, intm, maxm) in (QuantNec(out, dst, fids, intm, maxm) \u003d\u003e pre_MakeExistsBind(fids, dst, intm, maxm, \u003cPRE\u003e))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 599:22: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 ((dfdid in set (dom dfdsig)) \u003d\u003e (dfdid in set (dom dfdsig))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 517:8: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, style:(\u003cEXPL\u003e | \u003cIMPL\u003e) \u0026 ((if (style \u003d \u003cEXPL\u003e)\nthen pre_MakeDFDExplOp(dfdid, dfdtopo, dfdsig)\nelse pre_MakeDFDImplOp(dfdid, dfdtopo, dfdsig)) \u003d\u003e ((style \u003d \u003cEXPL\u003e) \u003d\u003e pre_MakeDFDExplOp(dfdid, dfdtopo, dfdsig))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 525:24: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and pre_MakeImplOpBody(dfdid, dfdtopo, dfdsig)) \u003d\u003e (dfdid in set (dom dfdsig))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 749:30: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1260:12: (forall sigs:set of (DEFAULT`Signature), stid:DEFAULT`StId \u0026 ((not (sigs \u003d {})) \u003d\u003e (exists sig in set sigs \u0026 true)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 751:31: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in (is_(nid, DEFAULT`DFDId) or is_(nid, DEFAULT`MSId))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1035:16: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 ((dfdid in set (dom dfdsig)) \u003d\u003e (forall m1, m2 in set {{stid |-\u003e 0} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4)))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1082:31: (forall id:(DEFAULT`DFDId | DEFAULT`MSId), mk_(din, out, -):DEFAULT`Signature \u0026 (forall i in set (inds out) \u0026 (i in set (inds out))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1193:18: (forall id:(DEFAULT`DSId | DEFAULT`Id), n:nat, max:nat, c:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((not ((n \u003d max) and (c \u003d \u003cPOST\u003e))) \u003d\u003e ((not (0 \u003d n)) \u003d\u003e pre_MakePatternSeq(StateVarConf(id), n, max))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1105:28: (forall idl:seq1 of (DEFAULT`Id) \u0026 ((not ((len idl) \u003d 1)) \u003d\u003e is_([FlowIdVarConf(idl(i)) | i in set (inds idl)], seq1 of (DEFAULT`Expr))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1131:30: (forall dfdtopo:DEFAULT`DFDTopo \u0026 (forall fid in set (dom dfdtopo) \u0026 (fid in set (dom dfdtopo))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1065:26: (forall piseq:seq1 of (DEFAULT`ProcId), dfdid:DEFAULT`DFDId, dfdsig:DEFAULT`DFDSig \u0026 (((hd piseq) in set (dom dfdsig)) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let mk_(call, pat):(DEFAULT`Call * [DEFAULT`Pattern]) \u003d MakeCallAndPat(nid, dfdsig(nid)), kind:(\u003cOPCALL\u003e | \u003cOPRES\u003e) \u003d FindKind(dfdsig(nid)) in (((len piseq) \u003d 1) \u003d\u003e (dfdid in set (dom dfdsig)))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 225:43: (forall fidl:seq of (DEFAULT`FlowId) \u0026 (forall i in set (inds fidl) \u0026 (i in set (inds fidl))))","comprehension map injectivity obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 568:16: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall m1, m2 in set {{stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid))} | mk_(stid, -) in set CollectStIds((rng dfdsig))} \u0026 (forall d3 in set (dom m1), d4 in set (dom m2) \u0026 ((d3 \u003d d4) \u003d\u003e (m1(d3) \u003d m2(d4))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 819:27: (forall dfdtopo:DEFAULT`DFDTopo \u0026 let top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or (is_(fid, MSId) or (fid \u003d nil))) and (is_(tid, DFDId) or (is_(tid, MSId) or (tid \u003d nil))))}, top2:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])) \u003d {mk_(fid, tid) | mk_(fid, tid) in set (rng dfdtopo) \u0026 ((is_(fid, DFDId) or is_(fid, MSId)) and (is_(tid, DFDId) or is_(tid, MSId)))} in let piset:set of ([DEFAULT`ProcId]) \u003d ((dunion {{pi_1, pi_2} | mk_(pi_1, pi_2) in set top}) \\ {nil}) in (forall piseq in set PossibleSeqs(piset) \u0026 (forall i, j in set (inds piseq) \u0026 ((j \u003c i) \u003d\u003e (j in set (inds piseq))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1783:47: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(nil, id) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(id, nil):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(id, nil) \u003d dfdtop(flowid)) \u003d\u003e let mk_(id, nil) \u003d dfdtop(flowid) in (is_(id, DEFAULT`DFDId) or is_(id, DEFAULT`MSId)))))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1164:26: (forall out:seq of (DEFAULT`FlowId), dst:DEFAULT`State, fids:set of (DEFAULT`FlowId), intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 ((forall mk_(s, -) in set (elems dst) \u0026 ((s in set (dom intm)) and (s in set (dom maxm)))) \u003d\u003e ((not (fids \u003c\u003e {})) \u003d\u003e (forall mk_(s, m) in set (elems dst) \u0026 ((m \u003d \u003cREADWRITE\u003e) \u003d\u003e (s in set (dom intm)))))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1785:47: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(nil, id) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(id, nil):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, nil) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(fid, tid):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(fid, tid) \u003d dfdtop(flowid)) \u003d\u003e let mk_(fid, tid) \u003d dfdtop(flowid) in (is_(fid, DEFAULT`DFDId) or is_(fid, DEFAULT`MSId))))))))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 785:27: (forall fs:set of (DEFAULT`FlowId), dst:DEFAULT`State, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, \u003cREADWRITE\u003e) in set (elems dst) \u0026 ((s in set (dom intm)) and (s in set (dom maxm)))) \u003d\u003e (forall i in set (inds dst) \u0026 (let mk_(-, m):(DEFAULT`StId * DEFAULT`Mode) \u003d dst(i) in (m \u003d \u003cREADWRITE\u003e) \u003d\u003e (i in set (inds dst))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1780:46: (forall dfdtop:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (forall flowid in set (dom dfdtop) \u0026 ((not (exists mk_(id, mk_EPId(-)):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(id, mk_EPId(any1)) \u003d dfdtop(flowid)))) \u003d\u003e ((not (exists mk_(mk_EPId(-), id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 (mk_(mk_EPId(any1), id) \u003d dfdtop(flowid)))) \u003d\u003e (exists mk_(nil, id):([DEFAULT`ProcId] * [DEFAULT`ProcId]) \u0026 ((mk_(nil, id) \u003d dfdtop(flowid)) \u003d\u003e let mk_(nil, id) \u003d dfdtop(flowid) in (id in set (dom dfdsig))))))))","let be st existence obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1220:14: (forall top:set of ((DEFAULT`ProcId * DEFAULT`ProcId)), ids:set of ((DEFAULT`DFDId | DEFAULT`MSId)) \u0026 ((exists mk_(fid, tid) in set top \u0026 (((fid in set ids) and (tid not in set ids)) or ((tid in set ids) and (fid not in set ids)))) \u003d\u003e (exists mk_(fid, tid) in set top \u0026 (((fid in set ids) and (tid not in set ids)) or ((tid in set ids) and (fid not in set ids))))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 747:28: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in (forall stid in set (dom intm) \u0026 ((not (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))) \u003d\u003e (stid in set (dom intm))))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 756:28: (forall piseq:seq1 of (DEFAULT`ProcId), dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let nid:DEFAULT`ProcId \u003d (hd piseq) in ((nid in set (dom dfdsig)) and (pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPRE\u003e) and pre_MakeQuotedApply(nid, dfdsig(nid), intm, maxm, \u003cPOST\u003e, \u003cPOST\u003e))) \u003d\u003e let nid:DEFAULT`ProcId \u003d (hd piseq) in let intm\u0027:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e (if (mk_(stid, \u003cREADWRITE\u003e) in set CollectStIds({dfdsig(nid)}))\nthen (intm(stid) + 1)\nelse intm(stid)) | stid in set (dom intm)} in let dpre:DEFAULT`Apply \u003d MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPOST\u003e, \u003cPRE\u003e), dpost:DEFAULT`Apply \u003d MakeQuotedApply(nid, dfdsig(nid), intm\u0027, maxm, \u003cPOST\u003e, \u003cPOST\u003e) in ((not ((len piseq) \u003d 1)) \u003d\u003e let pred:DEFAULT`BinaryExpr \u003d mk_BinaryExpr(dpre, \u003cAND\u003e, dpost) in pre_MakePostForEO((tl piseq), dfdsig, intm\u0027, maxm))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 76:18: (forall dfdid:DEFAULT`DFDId, dss:DEFAULT`DSs, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, dfdmap:DEFAULT`DFDMap \u0026 ((dfdid in set (dom dfdsig)) \u003d\u003e pre_MakeDFDModImps((dom dfdmap), dfdsig)))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1812:29: (forall id:DEFAULT`DFDId, top:set of (([DEFAULT`ProcId] * [DEFAULT`ProcId])), dfdmap:DEFAULT`DFDMap, dfdsig:DEFAULT`DFDSig \u0026 (forall dfdid in set (dom dfdmap) \u0026 (dfdid in set (dom dfdmap))))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1328:23: (forall id:(DEFAULT`DSId | DEFAULT`FlowId) \u0026 ((not is_(id, DSId)) \u003d\u003e is_(id, seq of (char))))","legal function application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 602:8: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 ((dfdid in set (dom dfdsig)) \u003d\u003e let mk_(-, out, dst):DEFAULT`Signature \u003d dfdsig(dfdid) in let fids:set of (DEFAULT`FlowId) \u003d NeedsQuant(dfdtopo, dfdsig, {}, {}), pred:DEFAULT`Expr \u003d MakePrePred(dfdtopo, dfdsig, intm, maxm) in pre_QuantNec(out, dst, fids, intm, maxm)))","type compatibility obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 681:21: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig, intm:DEFAULT`IntM, maxm:DEFAULT`IntM \u0026 (let mk_(-, out, dst):DEFAULT`Signature \u003d dfdsig(dfdid), fids:set of (DEFAULT`FlowId) \u003d NeedsQuant(dfdtopo, dfdsig, (elems out), {}) in pre_MakeInExpr(out, dst, fids, dfdtopo, dfdsig, intm, maxm) \u003d\u003e let mk_(-, out, dst):DEFAULT`Signature \u003d dfdsig(dfdid), fids:set of (DEFAULT`FlowId) \u003d NeedsQuant(dfdtopo, dfdsig, (elems out), {}), body:DEFAULT`Expr \u003d MakeInExpr(out, dst, fids, dfdtopo, dfdsig, intm, maxm) in ((not ((len out) \u003c\u003d 1)) \u003d\u003e (is_(MakePattern(out), DEFAULT`PatternId) or is_(MakePattern(out), DEFAULT`TuplePattern)))))","legal map application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 1018:22: (forall dfdid:DEFAULT`DFDId, dfdtopo:DEFAULT`DFDTopo, dfdsig:DEFAULT`DFDSig \u0026 (((dfdid in set (dom dfdsig)) and let intm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e 0 | mk_(stid, -) in set CollectStIds((rng dfdsig))}, maxm:map (DEFAULT`StId) to (nat) \u003d {stid |-\u003e Reduce(NoOfWr((rng dfdsig), stid)) | mk_(stid, -) in set CollectStIds((rng dfdsig))} in (pre_MakePreExpr(dfdid, dfdtopo, dfdsig, intm, maxm) and (forall piseq in set ExecutionOrders(dfdtopo) \u0026 pre_MakeStmtForEO(piseq, dfdid, dfdsig)))) \u003d\u003e (dfdid in set (dom dfdsig))))","legal sequence application obligation in \u0027DEFAULT\u0027 (DFDexampleSL.vdmsl) at line 790:28: (forall fs:set of (DEFAULT`FlowId), dst:DEFAULT`State, intm:DEFAULT`IntM, maxm:DEFAULT`IntM, c:(\u003cPOST\u003e | \u003cPRE\u003e) \u0026 ((forall mk_(s, \u003cREADWRITE\u003e) in set (elems dst) \u0026 ((s in set (dom intm)) and (s in set (dom maxm)))) \u003d\u003e (forall i in set (inds dst) \u0026 (i in set (inds dst)))))"] \ No newline at end of file diff --git a/core/typechecker/src/main/java/org/overture/typechecker/visitor/TypeCheckerExpVisitor.java b/core/typechecker/src/main/java/org/overture/typechecker/visitor/TypeCheckerExpVisitor.java index 87927555b5..0b7755dfb1 100644 --- a/core/typechecker/src/main/java/org/overture/typechecker/visitor/TypeCheckerExpVisitor.java +++ b/core/typechecker/src/main/java/org/overture/typechecker/visitor/TypeCheckerExpVisitor.java @@ -3341,6 +3341,11 @@ else if (question.assistantFactory.createPTypeAssistant().isType(node.getLeft(). node.setType(AstFactory.newASeqSeqType(node.getLocation(), AstFactory.newAUnknownType(node.getLocation()))); return node.getType(); } + else if (etype instanceof ASeq1SeqType) + { + ASeq1SeqType s = (ASeq1SeqType)etype; + etype = AstFactory.newASeqSeqType(node.getLocation(), s.getSeqof()); + } node.setType(etype); return etype;