Page 21 - 《软件学报》2025年第9期

3932 软件学报 2025 年第 36 卷第 9 期

(1) 反证法. 假设 co(d,c) 成立.
(2) 由 rf(d,b)、co(d,c) 以及 fr 的定义可得: fr(b,c).
(3) 由 (2)、rf(c,a) 以及定理 5 可得: ¬perloc(b,a). 与 poloc(a,b) 推出矛盾.

R R R W R R R W W R R R

R W W
W R R W R W R R R
R R W
W W R W W W R R W
W R W

W W W R W R W R W R R W
(a) 相关定理 (b) 推论
图 11 序列模式转换的相关定理和推论示意

引理 14. ∀a,b∈E, coi(a,b)→poloc(a,b).
证明: 由 coi 的定义, 将目标替换为: 已知 co(a,b), int(a,b), 求证 po(a,b)∧loc(a,b). 显然, loc(a,b) 是成立的. 由
int(a,b) 以及 po 的定义可得: po(a,b)∨po(b,a). 最终证明¬po(b,a) 即可.
(1) 反证法. 假设 po(b,a) 成立.
(2) 由 po(b,a)、loc(a,b)、ppo1 的定义以及公理 2 可得: gmo(b,a).
(3) 由 co(a,b) 以及 co 的定义可得: gmo(a,b). 由 gmo 的非对称性与 (2) 推出矛盾.
定理 11 (RwW 转换). ∀a∈R, ∀b,c∈W, perloc(a,b,c)→perloc(a,c).
证明: 由表 3 和引理 11, 将目标替换为: 已知 poloc(a,b)∨fr(a,b), co(b,c), 求证 perloc(a,c). 分两种情况证明.
(1) 若 poloc(a,b) 成立:
(1.1) 由 int 和 ext 的定义可得: int(b,c)∨ext(b,c). 分开讨论.
(1.2) 若 int(b,c) 成立:
(1.2.1) 由 int(b,c)、co(b,c) 以及引理 14 可得: poloc(b,c).
(1.2.2) 由 poloc(a,b)、poloc(b,c) 以及 poloc 的传递性可得: poloc(a,c). perloc(a,c) 得证.
(1.3) 若 ext(b,c) 成立:
(1.3.1) 由 poloc(a,b)、ppo1 的定义以及公理 2 可得: gmo(a,b).
(1.3.2) 由假设中 co(b,c) 以及 co 定义可得: gmo(b,c).
(1.3.3) 由公理 1 可知: ∃x∈W, rf(x,a).
(1.3.4) 证明 x≠c.
(1.3.4.1) 反证法. 假设 x=c. 由 (1.3.2) 可得: rf(c,a).
(1.3.4.2) 由 poloc(a,b) 可知 int(a,b), 又因 ext(b,c) 可得: ext(a,c), 进而得到 rfe(c,a).
(1.3.4.3) 由 (1.3.4.2) 以及引理 8 可得: gmo(c,a).
(1.3.4.4) 由 (1.3.1)、(1.3.2) 以及 gmo 的定义可得: gmo(a,c).
(1.3.4.5) 由 (1.3.4.3)、(1.3.4.4) 以及 gmo 的非对称性推出矛盾.
(1.3.5) 证明 gmo(x,c). 由 (1.3.4) 以及 gmo 的定义可得: gmo(x,c)∨gmo(c,x). 只需证¬gmo(c,x).
(1.3.5.1) 反证法. 假设 gmo(c,x) 成立.
(1.3.5.2) 由 (1.3.3) 中 rf(x,a) 以及定义 14 可得: rfi(x,a)∨rfe(x,a). 分开讨论.
(1.3.5.3) 若 rfi(x,a) 成立:
(1.3.5.3.1) 由引理 7 可得: poloc(x,a), 又因 poloc(a,b) 以及 poloc 传递性可得: poloc(x,b).