因此,让引理建立BM、AMAN和PMM之间的相互作用以及列表上的上述关系是有用的。二十: 6金融市场交易的正式验证ABFB(a)子列表(b)包括(c)Perml1l1l2l1l2abcdfabcdefgabbcdcaebcdaeabccbabedbffigure 2列表条目之间的虚线证实了这些条目在两个列表中的存在。(a) 如果Lis子列表中的每个Lis条目也出现在土地上,则它们会以相同的顺序出现。(b) 包含在Lif中的列表Lis,Lis中的每个条目也存在于L。(c)如果两个条目在两个L.I引理5中的发生次数相同,则两个列表彼此的Lare排列。included\\u M\\u imp\\u included\\u投标:included M M->included BMBM。I引理6。included\\M\\u imp\\u included\\u asks:included M M->included amam上述引理中包含的概念类似于多集上的子集关系。我们有以下引理来说明包含关系的确切行为。I引理7。included\\u简介:( a、 计数a l≤ 计数a,s)->包括l,s,I引理8。included\\u elim:包含l s->( a、 计数a l≤ 计数a s)。在这项工作中,我们遇到了输入和输出都是列表的各种流程。我们需要类似于子序列关系的子列表关系来正确地指定这些过程的行为。I引理9。sublist\\u intro1(a:T):sublist l s->sublist l(a::s)。I引理10。sublist\\u elim3a(a e:T):sublist(a::l)(e::s)->sublist l s。请注意,如引理10所示,sublist的递归性质。它使得在先行词中包含子列表的语句更容易归纳。但是,对于其他关系(即included和perm),情况并非如此。3双边拍卖分析在这项工作中,我们不考虑对拍卖商的利益进行分析。因此,匹配的买卖双方的买方支付的金额与卖方收到的金额相同。
|