LP (the Larch Prover), Release 3.1a (95/04/27) logging to `/pro/oodb/specs/KOLA98/SIGMOD98_Scripts.lplog' on 21 June 1998 18:15:57. LP0.1.2: LP0.1.3: % ****************************************************************************** LP0.1.4: % * * LP0.1.5: % * Script File: SIGMOD98_Scripts * LP0.1.6: % * -------------------------------------------------------------------------- * LP0.1.7: % * Scripts Author: Mitch Cherniack (mfc@cs.brandeis.edu) * LP0.1.8: % * Date: June, 1998 * LP0.1.9: % * * LP0.1.10: % * Present Address: Computer Science Department * LP0.1.11: % * Brandeis University * LP0.1.12: % * Waltham, MA 02254 * LP0.1.13: % * -------------------------------------------------------------------------- * LP0.1.14: % * * LP0.1.15: % * Proof Scripts Establishing Correctness of Rewrite Rules used in the paper, * LP0.1.16: % * [CZ98a]: * LP0.1.17: % * * LP0.1.18: % * [CZ98a] Changing the Rules: Transformations for Rule-Based Optimizers * LP0.1.19: % * Mitch Cherniack and Stan Zdonik, In Proceedings of the 1998 ACM * LP0.1.20: % * SIGMOD International Conference on Management of Data, Seattle, * LP0.1.21: % * WA, June, 1998. * LP0.1.22: % * * LP0.1.23: % * For an up-to-date version of [CZ98a], see: * LP0.1.24: % * ftp://wilma.cs.brown.edu/u/mfc/sigmod98.ps.Z * LP0.1.25: % * * LP0.1.26: % * * LP0.1.27: % * Instructions: * LP0.1.28: % * * LP0.1.29: % * Requires Version 3.1a of the LP Theorem Prover, available from * LP0.1.30: % * MIT, Laboratory of Computer Science. For software and documentation on * LP0.1.31: % * LP see: * LP0.1.32: % * * LP0.1.33: % * http://www.sds.lcs.mit.edu/spd/larch/LP/overview.html * LP0.1.34: % * * LP0.1.35: % * With LP installed in $path, run this theorem prover script by typing * LP0.1.36: % * * LP0.1.37: % * $path/lp -c SIGMOD98_Scripts * LP0.1.38: % * * LP0.1.39: % ****************************************************************************** LP0.1.40: LP0.1.41: % Section 1: CNF LP0.1.42: % LP0.1.43: % Proof Scripts for COKO Transformations, LP0.1.44: % LP0.1.45: % TRANSFORMATION CNFNE LP0.1.46: % USES LP0.1.47: % CNFAux LP0.1.48: % BEGIN LP0.1.49: % BU {CNFAux} LP0.1.50: % END LP0.1.51: % LP0.1.52: % TRANSFORMATION CNFAux LP0.1.53: % USES LP0.1.54: % dist1: p | (q & r) --> (p | q) & (p | r), LP0.1.55: % dist2: (p & q) | r --> (p | r) & (q | r) LP0.1.56: % BEGIN LP0.1.57: % {dist1 || dist2} -> LP0.1.58: % GIVEN p & q DO {CNFAux (p); CNFAux (q)} LP0.1.59: % END LP0.1.60: % LP0.1.61: % TRANSFORMATION CNF LP0.1.62: % USES LP0.1.63: % CNFNE, LP0.1.64: % involution: ~ (~ (p)) --> p, LP0.1.65: % deMorgan1: ~ (p & q) --> ~ (p) | ~ (q), LP0.1.66: % deMorgan2: ~ (p | q) --> ~ (p) & ~ (q) LP0.1.67: % BEGIN LP0.1.68: % TD {involution || deMorgan1 || deMorgan2}; LP0.1.69: % BU {involution}; LP0.1.70: % CNFNE LP0.1.71: % END LP0.1.72: % LP0.1.73: % In [CZ98a], CNFNE is called CNF, and CNF (above) is not LP0.1.74: % described. LP0.1.75: LP0.1.76: clear LP0.1.77: set order manual The ordering-method is now `manual'. LP0.1.78: exec-silently CNF_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/CNF_Aux_Axioms.lp'. LP0.1.79: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.80: order formulas The system now contains 5 rewrite rules. The rewriting system is guaranteed to terminate. All equations have been oriented into rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.81: make immune formulas LP0.1.82: LP0.1.83: declare variables p, q, r: pred [T] .. LP0.1.84: LP0.1.85: LP0.1.86: % L1: Rules Used in CNFAux LP0.1.87: % ------------------------ LP0.1.88: LP0.1.89: set name dist1 The name-prefix is now `dist1'. LP0.1.90: prove (p & q) | r = (p | r) & (q | r) Attempting to prove conjecture dist1.1: (p & q) | r = (p | r) & (q | r) Suspending proof of conjecture dist1.1 LP0.1.91: LP0.1.92: resume by <=> Creating subgoals for proof of <=> New constants: pc, xc, rc, qc => hypothesis: dist1ImpliesHyp.1: (pc ? xc \/ rc ? xc) /\ (qc ? xc \/ rc ? xc) => subgoal: (pc ? xc /\ qc ? xc) \/ rc ? xc <= hypothesis: dist1ImpliesHyp.2: (pc ? xc /\ qc ? xc) \/ rc ? xc <= subgoal: (pc ? xc \/ rc ? xc) /\ (qc ? xc \/ rc ? xc) Attempting to prove level 2 subgoal 1 for proof of <=> Added hypothesis dist1ImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula dist1ImpliesHyp.1 to yield the following formulas, which imply dist1ImpliesHyp.1. dist1ImpliesHyp.1.1: pc ? xc \/ rc ? xc dist1ImpliesHyp.1.2: qc ? xc \/ rc ? xc The system now contains 7 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 2 subgoal 1 for proof of <=> LP0.1.93: LP0.1.94: % => LP0.1.95: resume by cases (rc ? xc) Creating subgoals for proof by cases Case hypotheses: dist1CaseHyp.1.1: rc ? xc dist1CaseHyp.1.2: ~(rc ? xc) Same subgoal for all cases: (pc ? xc /\ qc ? xc) \/ rc ? xc Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis dist1CaseHyp.1.1 to the system. Level 3 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis dist1CaseHyp.1.2 to the system. Level 3 subgoal for case 2 (out of 2) [] Proved by normalization. Level 2 subgoal 1 for proof of <=> [] Proved by cases rc ? xc. Attempting to prove level 2 subgoal 2 for proof of <=> Added hypothesis dist1ImpliesHyp.2 to the system. The system now contains 6 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 2 subgoal 2 for proof of <=>: (pc ? xc \/ rc ? xc) /\ (qc ? xc \/ rc ? xc) LP0.1.96: LP0.1.97: % <= LP0.1.98: resume by cases (rc ? xc) Creating subgoals for proof by cases Case hypotheses: dist1CaseHyp.1.1: rc ? xc dist1CaseHyp.1.2: ~(rc ? xc) Same subgoal for all cases: (pc ? xc \/ rc ? xc) /\ (qc ? xc \/ rc ? xc) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis dist1CaseHyp.1.1 to the system. Level 3 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis dist1CaseHyp.1.2 to the system. Deduction rule lp_and_is_true has been applied to formula dist1ImpliesHyp.2 to yield the following formulas, which imply dist1ImpliesHyp.2. dist1ImpliesHyp.2.1: pc ? xc dist1ImpliesHyp.2.2: qc ? xc Level 3 subgoal for case 2 (out of 2) [] Proved by normalization. Level 2 subgoal 2 for proof of <=> [] Proved by cases rc ? xc. Conjecture dist1.1: (p & q) | r = (p | r) & (q | r) [] Proved <=>. LP0.1.99: LP0.1.100: qed All conjectures have been proved. LP0.1.101: LP0.1.102: set name dist2 The name-prefix is now `dist2'. LP0.1.103: prove r | (p & q) = (p | r) & (q | r) Attempting to prove conjecture dist2.1: r | (p & q) = (p | r) & (q | r) Conjecture dist2.1 [] Proved by normalization. Deleted formula dist2.1, which reduced to `true'. LP0.1.104: qed All conjectures have been proved. LP0.1.105: LP0.1.106: LP0.1.107: % L1: Rules Used in CNF LP0.1.108: % --------------------- LP0.1.109: LP0.1.110: set name involution The name-prefix is now `involution'. LP0.1.111: prove ~ (~ (p)) = p Attempting to prove conjecture involution.1: ~ ~p = p Conjecture involution.1 [] Proved by normalization. Deleted formula involution.1, which reduced to `true'. LP0.1.112: qed All conjectures have been proved. LP0.1.113: LP0.1.114: set name deMorgan1 The name-prefix is now `deMorgan1'. LP0.1.115: prove ~ (p & q) = (~ (p)) | (~ (q)) Attempting to prove conjecture deMorgan1.1: ~(p & q) = (~p) | (~q) Suspending proof of conjecture deMorgan1.1 LP0.1.116: LP0.1.117: resume by <=> Creating subgoals for proof of <=> New constants: pc, xc, qc => hypothesis: deMorgan1ImpliesHyp.1: ~(pc ? xc) \/ ~(qc ? xc) => subgoal: ~(pc ? xc /\ qc ? xc) <= hypothesis: deMorgan1ImpliesHyp.2: ~(pc ? xc /\ qc ? xc) <= subgoal: ~(pc ? xc) \/ ~(qc ? xc) Attempting to prove level 2 subgoal 1 for proof of <=> Added hypothesis deMorgan1ImpliesHyp.1 to the system. The system now contains 7 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 2 subgoal 1 for proof of <=> LP0.1.118: LP0.1.119: % => LP0.1.120: resume by cases ~ (pc ? xc) Creating subgoals for proof by cases Case hypotheses: deMorgan1CaseHyp.1.1: ~(pc ? xc) deMorgan1CaseHyp.1.2: ~(~(pc ? xc)) Same subgoal for all cases: ~(pc ? xc /\ qc ? xc) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis deMorgan1CaseHyp.1.1 to the system. Level 3 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis deMorgan1CaseHyp.1.2 to the system. Level 3 subgoal for case 2 (out of 2) [] Proved by normalization. Level 2 subgoal 1 for proof of <=> [] Proved by cases ~(pc ? xc). Attempting to prove level 2 subgoal 2 for proof of <=> Added hypothesis deMorgan1ImpliesHyp.2 to the system. Suspending proof of level 2 subgoal 2 for proof of <=> LP0.1.121: LP0.1.122: % <= LP0.1.123: resume by contradiction Creating subgoals for proof by contradiction Hypothesis: deMorgan1ContraHyp.1: ~(~(pc ? xc) \/ ~(qc ? xc)) Only subgoal: false Attempting to prove level 3 subgoal for proof by contradiction Added hypothesis deMorgan1ContraHyp.1 to the system. Deduction rule lp_or_is_false has been applied to formula deMorgan1ContraHyp.1 to yield the following formulas, which imply deMorgan1ContraHyp.1. deMorgan1ContraHyp.1.1: ~(~(pc ? xc)) deMorgan1ContraHyp.1.2: ~(~(qc ? xc)) Formula deMorgan1ImpliesHyp.2, false, is inconsistent. Level 3 subgoal for proof by contradiction [] Proved by detecting an inconsistency. Level 2 subgoal 2 for proof of <=>: ~(pc ? xc) \/ ~(qc ? xc) [] Proved by contradiction. Conjecture deMorgan1.1: ~(p & q) = (~p) | (~q) [] Proved <=>. LP0.1.124: LP0.1.125: qed All conjectures have been proved. LP0.1.126: LP0.1.127: set name deMorgan2 The name-prefix is now `deMorgan2'. LP0.1.128: prove ~ (p | q) = (~ (p)) & (~ (q)) Attempting to prove conjecture deMorgan2.1: ~(p | q) = (~p) & (~q) Suspending proof of conjecture deMorgan2.1 LP0.1.129: resume by <=> Creating subgoals for proof of <=> New constants: pc, xc, qc => hypothesis: deMorgan2ImpliesHyp.1: ~(pc ? xc) /\ ~(qc ? xc) => subgoal: ~(pc ? xc \/ qc ? xc) <= hypothesis: deMorgan2ImpliesHyp.2: ~(pc ? xc \/ qc ? xc) <= subgoal: ~(pc ? xc) /\ ~(qc ? xc) Attempting to prove level 2 subgoal 1 for proof of <=> Added hypothesis deMorgan2ImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula deMorgan2ImpliesHyp.1 to yield the following formulas, which imply deMorgan2ImpliesHyp.1. deMorgan2ImpliesHyp.1.1: ~(pc ? xc) deMorgan2ImpliesHyp.1.2: ~(qc ? xc) Level 2 subgoal 1 for proof of <=> [] Proved by normalization. Attempting to prove level 2 subgoal 2 for proof of <=> Added hypothesis deMorgan2ImpliesHyp.2 to the system. Deduction rule lp_or_is_false has been applied to formula deMorgan2ImpliesHyp.2 to yield the following formulas, which imply deMorgan2ImpliesHyp.2. deMorgan2ImpliesHyp.2.1: ~(pc ? xc) deMorgan2ImpliesHyp.2.2: ~(qc ? xc) Level 2 subgoal 2 for proof of <=> [] Proved by normalization. Conjecture deMorgan2.1 [] Proved <=>. The system now contains 8 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.130: qed All conjectures have been proved. LP0.1.131: LP0.1.132: LP0.1.133: LP0.1.134: % Section 2: SNF LP0.1.135: % LP0.1.136: % Proof Scripts for COKO Transformations, LP0.1.137: % LP0.1.138: % TRANSFORMATION SNF LP0.1.139: % USES LP0.1.140: % SimpLits, LP0.1.141: % CNF, LP0.1.142: % OrderConjs, LP0.1.143: % pushneg: ~ (p OPLUS f) --> (~ (p)) OPLUS f, LP0.1.144: % init: p --> (K (true) OPLUS #1) & (K (true) OPLUS #2) & K (true) & p, LP0.1.145: % pull: (p OPLUS f) | (q OPLUS f) --> (p | q) OPLUS f, LP0.1.146: % shift: p & (q & r) --> (p & r) & q, LP0.1.147: % simplify: K (true) & p --> p LP0.1.148: % BEGIN LP0.1.149: % SimpLits; LP0.1.150: % CNF; LP0.1.151: % TD {pushneg}; LP0.1.152: % init; LP0.1.153: % BU {pull || {REPEAT shift}}; LP0.1.154: % OrderConjs; LP0.1.155: % BU {simplify} LP0.1.156: % END LP0.1.157: % LP0.1.158: % TRANSFORMATION SimpLits LP0.1.159: % USES LP0.1.160: % SL1: --> o h, LP0.1.161: % SL2: --> K ([x, y]), LP0.1.162: % SL3: --> o f, LP0.1.163: % SL4: --> o f, LP0.1.164: % SL5: f o (g o h) --> (f o g) o h, LP0.1.165: % SL6: f o K (x) --> K (f ! x), LP0.1.166: % SL7: p OPLUS (f o g) --> p OPLUS f OPLUS g, LP0.1.167: % SL8: p OPLUS K (x) --> K (p ? x) LP0.1.168: % BEGIN LP0.1.169: % BU {{{SL1 || SL2 || SL3 || SL4} -> LP0.1.170: % {REPEAT {SL5 -> {print "SL5 fired on"; LP0.1.171: % GIVEN f DO print f; print "\n"}}}} || LP0.1.172: % SL6 || SL7 || SL8} LP0.1.173: % END LP0.1.174: % LP0.1.175: % TRANSFORMATION OrderConjs LP0.1.176: % USES LP0.1.177: % OC1: (p OPLUS #1) & q & r & (r' OPLUS #1) --> ((p & r') OPLUS #1) & q & r, LP0.1.178: % OC2: p & (q OPLUS #2) & r & (r' OPLUS #2) --> p & ((q & r') OPLUS #2) & r, LP0.1.179: % OC3: p & q & r & r' --> p & q & (r & r') LP0.1.180: % BEGIN LP0.1.181: % BU {OC1 || OC2 || OC3} LP0.1.182: % END LP0.1.183: % LP0.1.184: % In [CZ98a], transformation SNF does not contain the rewrite rule, LP0.1.185: % pushneg, nor the firing algorithm statement, LP0.1.186: % LP0.1.187: % TD {pushneg} LP0.1.188: % LP0.1.189: LP0.1.190: LP0.1.191: clear LP0.1.192: set order manual The ordering-method is now `manual'. LP0.1.193: exec-silently SNF_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/SNF_Aux_Axioms.lp'. LP0.1.194: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.195: order formulas The system now contains 66 rewrite rules. The rewriting system is guaranteed to terminate. All equations have been oriented into rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.196: make immune formulas LP0.1.197: LP0.1.198: % L1: Rules Used in Transformation, SNF LP0.1.199: % ------------------------------------- LP0.1.200: LP0.1.201: set name pushneg The name-prefix is now `pushneg'. LP0.1.202: declare variables p: pred [S], f: fun [R, S] LP0.1.203: prove ~ (p \oplus f) = (~ (p) \oplus f) Attempting to prove conjecture pushneg.1: ~(p \oplus f) = (~p) \oplus f Conjecture pushneg.1 [] Proved by normalization. Deleted formula pushneg.1, which reduced to `true'. LP0.1.204: qed All conjectures have been proved. LP0.1.205: LP0.1.206: set name init The name-prefix is now `init'. LP0.1.207: declare variables p: pred [pair [T, U]] LP0.1.208: prove p = (K (true) \oplus fst) & (K (true) \oplus snd) & K (true) & p Attempting to prove conjecture init.1: p = (K(true) \oplus fst) & (K(true) \oplus snd) & K(true) & p Conjecture init.1 [] Proved by normalization. Deleted formula init.1, which reduced to `true'. LP0.1.209: qed All conjectures have been proved. LP0.1.210: LP0.1.211: set name pull The name-prefix is now `pull'. LP0.1.212: declare variables p: pred [S], f: fun [R, S] LP0.1.213: prove (p \oplus f) | (q \oplus f) = (p | q) \oplus f Attempting to prove conjecture pull.1: (p \oplus f) | (q \oplus f) = (p | q) \oplus f Conjecture pull.1 [] Proved by normalization. Deleted formula pull.1, which reduced to `true'. LP0.1.214: qed All conjectures have been proved. LP0.1.215: LP0.1.216: set name shift The name-prefix is now `shift'. LP0.1.217: declare variables p, q, r: pred [S] LP0.1.218: prove p & (q & r) = (p & r) & q Attempting to prove conjecture shift.1: p & (q & r) = p & r & q Conjecture shift.1 [] Proved by normalization. Deleted formula shift.1, which reduced to `true'. LP0.1.219: qed All conjectures have been proved. LP0.1.220: LP0.1.221: set name simplify The name-prefix is now `simplify'. LP0.1.222: declare variables p: pred [S] LP0.1.223: prove K (true) & p: pred [S] = p Attempting to prove conjecture simplify.1: (K(true) & p):pred[S] = p Conjecture simplify.1 [] Proved by normalization. Deleted formula simplify.1, which reduced to `true'. LP0.1.224: qed All conjectures have been proved. LP0.1.225: LP0.1.226: % L1: Rules Used in Transformation, SimpLits LP0.1.227: % ------------------------------------------ LP0.1.228: LP0.1.229: set name SL1 The name-prefix is now `SL1'. LP0.1.230: declare variables h: fun [T, U], f: fun [U, V], g: fun [U, W] LP0.1.231: prove \< f \circ h, g \circ h \> = \< f, g \> \circ h Attempting to prove conjecture SL1.1: \ = \ \circ h Conjecture SL1.1 [] Proved by normalization. Deleted formula SL1.1, which reduced to `true'. LP0.1.232: qed All conjectures have been proved. LP0.1.233: LP0.1.234: set name SL2 The name-prefix is now `SL2'. LP0.1.235: declare variables x: U, y: V LP0.1.236: prove \< K (x), K (y) \> = K ([x, y]) Attempting to prove conjecture SL2.1: \ = K([x, y]) Conjecture SL2.1 [] Proved by normalization. Deleted formula SL2.1, which reduced to `true'. LP0.1.237: qed All conjectures have been proved. LP0.1.238: LP0.1.239: set name SL3 The name-prefix is now `SL3'. LP0.1.240: declare variables x: V, f: fun [T, U] LP0.1.241: prove \< f, K (x) \> = \< id, K (x) \> \circ f Attempting to prove conjecture SL3.1: \ = \ \circ f Conjecture SL3.1 [] Proved by normalization. Deleted formula SL3.1, which reduced to `true'. LP0.1.242: qed All conjectures have been proved. LP0.1.243: LP0.1.244: set name SL4 The name-prefix is now `SL4'. LP0.1.245: declare variables x: V, f: fun [T, U] LP0.1.246: prove \< K (x), f \> = \< K (x), id \> \circ f Attempting to prove conjecture SL4.1: \ = \ \circ f Conjecture SL4.1 [] Proved by normalization. Deleted formula SL4.1, which reduced to `true'. LP0.1.247: qed All conjectures have been proved. LP0.1.248: LP0.1.249: set name SL5 The name-prefix is now `SL5'. LP0.1.250: declare variables h: fun [T, U], g: fun [U, V], f: fun [V, W] LP0.1.251: prove f \circ (g \circ h) = (f \circ g) \circ h Attempting to prove conjecture SL5.1: f \circ (g \circ h) = f \circ g \circ h Conjecture SL5.1 [] Proved by normalization. Deleted formula SL5.1, which reduced to `true'. LP0.1.252: qed All conjectures have been proved. LP0.1.253: LP0.1.254: set name SL6 The name-prefix is now `SL6'. LP0.1.255: declare variables x: U, f: fun [U, V] LP0.1.256: prove f:fun [U, V] \circ K (x) = K (f:fun [U, V] ! x) Attempting to prove conjecture SL6.1: (f \circ K(x)):fun[T, V] = K(f:fun[U, V] ! x) Conjecture SL6.1 [] Proved by normalization. Deleted formula SL6.1, which reduced to `true'. LP0.1.257: qed All conjectures have been proved. LP0.1.258: LP0.1.259: set name SL7 The name-prefix is now `SL7'. LP0.1.260: declare variables g: fun [T, U], f: fun [U, V], p: pred [V] LP0.1.261: prove p \oplus (f \circ g) = (p \oplus f) \oplus g Attempting to prove conjecture SL7.1: p \oplus (f \circ g) = p \oplus f \oplus g Conjecture SL7.1 [] Proved by normalization. Deleted formula SL7.1, which reduced to `true'. LP0.1.262: qed All conjectures have been proved. LP0.1.263: LP0.1.264: set name SL8 The name-prefix is now `SL8'. LP0.1.265: declare variables x: U, p: pred [U] LP0.1.266: prove p: pred [U] \oplus K (x) = K (p: pred [U] ? x) Attempting to prove conjecture SL8.1: (p:pred[U] \oplus K(x)):pred[T] = K(p:pred[U] ? x) Conjecture SL8.1 [] Proved by normalization. Deleted formula SL8.1, which reduced to `true'. LP0.1.267: qed All conjectures have been proved. LP0.1.268: LP0.1.269: % L1: Rules Used in Transformation, OrderConjs LP0.1.270: % -------------------------------------------- LP0.1.271: LP0.1.272: set name OC1 The name-prefix is now `OC1'. LP0.1.273: declare variables p: pred [T], q: pred [U], r: pred [pair [T, U]], s: pred [T] .. LP0.1.274: prove (p \oplus fst) & (q \oplus snd) & r & (s \oplus fst) = ((p & s) \oplus fst) & (q \oplus snd) & r .. Attempting to prove conjecture OC1.1: (p \oplus fst) & (q \oplus snd) & r & (s \oplus fst) = ((p & s) \oplus fst) & (q \oplus snd) & r Conjecture OC1.1 [] Proved by normalization. Deleted formula OC1.1, which reduced to `true'. LP0.1.275: qed All conjectures have been proved. LP0.1.276: LP0.1.277: set name OC2 The name-prefix is now `OC2'. LP0.1.278: declare variables p: pred [T], q: pred [U], r: pred [pair [T, U]], s: pred [U] LP0.1.279: prove (p \oplus fst) & (q \oplus snd) & r & (s \oplus snd) = (p \oplus fst) & ((q & s) \oplus snd) & r .. Attempting to prove conjecture OC2.1: (p \oplus fst) & (q \oplus snd) & r & (s \oplus snd) = (p \oplus fst) & ((q & s) \oplus snd) & r Conjecture OC2.1 [] Proved by normalization. Deleted formula OC2.1, which reduced to `true'. LP0.1.280: qed All conjectures have been proved. LP0.1.281: LP0.1.282: set name OC3 The name-prefix is now `OC3'. LP0.1.283: declare variables p: pred [T], q: pred [U], r, s: pred [pair [T, U]] LP0.1.284: prove (p \oplus fst) & (q \oplus snd) & r & s = (p \oplus fst) & (q \oplus snd) & (r & s) .. Attempting to prove conjecture OC3.1: (p \oplus fst) & (q \oplus snd) & r & s = (p \oplus fst) & (q \oplus snd) & (r & s) Conjecture OC3.1 [] Proved by normalization. Deleted formula OC3.1, which reduced to `true'. LP0.1.285: qed All conjectures have been proved. LP0.1.286: LP0.1.287: LP0.1.288: LP0.1.289: % Section 3: Predicate Pushdown LP0.1.290: % LP0.1.291: % Proof Scripts for COKO Transformation, LP0.1.292: % LP0.1.293: % TRANSFORMATION Pushdown LP0.1.294: % USES LP0.1.295: % SNF, LP0.1.296: % push: join ((p OPLUS #1) & (q OPLUS #2) & r, f) ! [A, B] --> LP0.1.297: % join (r, f) ! [iterate (p, id) ! A, iterate (q, id) ! B], LP0.1.298: % simp: iterate (K (true), id) ! A --> A LP0.1.299: % LP0.1.300: % BEGIN LP0.1.301: % GIVEN join (p, _F) ! _O DO { LP0.1.302: % SNF (p); LP0.1.303: % push; LP0.1.304: % GIVEN join (_P, _F) ! [A, B] DO { LP0.1.305: % simp (A); LP0.1.306: % simp (B) LP0.1.307: % } LP0.1.308: % } LP0.1.309: % END LP0.1.310: % LP0.1.311: % In [CZ98a], only rules push and simp are described. LP0.1.312: % LP0.1.313: LP0.1.314: clear LP0.1.315: forget Critical pair list cleared. LP0.1.316: unregister registry LP0.1.317: set order manual The ordering-method is now `manual'. LP0.1.318: exec-silently Pushdown_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/Pushdown_Aux_Axioms.lp'. LP0.1.319: declare variables p: pred [T1], p: pred [T2], q: pred [T2], x: T1, y: T2, r: pred [pair [T1, T2]], f: fun [pair [T1, T2], U], f, g: fun [T2, T2], A: bag [T1], B: bag [T2] .. LP0.1.320: LP0.1.321: LP0.1.322: register height [__,__]:T2,T1->pair[T2, T1] = [__,__]:T1,T2->pair[T1, T2] Registry extended. LP0.1.323: register height ?:pred[pair[T2, T1]],pair[T2, T1]->Bool = ?:pred[pair[T1, T2]],pair[T1, T2]->Bool .. Registry extended. LP0.1.324: register height ?:pred[T1],T1->Bool = ?:pred[pair[T2, T1]],pair[T2, T1]->Bool Registry extended. LP0.1.325: register height ?:pred[T1],T1->Bool > [__,__]:T2,T1->pair[T2, T1] Registry extended. LP0.1.326: register height ?:pred[T2],T2->Bool = ?:pred[pair[T1, T2]],pair[T1, T2]->Bool Registry extended. LP0.1.327: register height ?:pred[T2],T2->Bool > [__,__]:T1,T2->pair[T1, T2] Registry extended. LP0.1.328: register height !:fun[bag[T2], bag[T2]],bag[T2]->bag[T2] = !:fun[bag[T2], bag[U]],bag[T2]->bag[U] .. Registry extended. LP0.1.329: register height C:pred[pair[T1, T2]],T1->pred[T2] > (&:pred[T2],pred[T2]->pred[T2], \circ:fun[bag[T2], bag[U]],fun[bag[T2], bag[T2]]->fun[bag[T2], bag[U]], iterate:pred[T2],fun[T2, U]->fun[bag[T2], bag[U]], iterate:pred[T2],fun[T2, T2]->fun[bag[T2], bag[T2]]) .. Registry extended. LP0.1.330: register height &:pred[T2],pred[T2]->pred[T2] = \circ:fun[bag[T2], bag[U]],fun[bag[T2], bag[T2]]->fun[bag[T2], bag[U]] = iterate:pred[T2],fun[T2, U]->fun[bag[T2], bag[U]] .. Registry extended. LP0.1.331: register height &:pred[T2],pred[T2]->pred[T2] >= iterate:pred[T2],fun[T2, T2]->fun[bag[T2], bag[T2]] .. Registry extended. LP0.1.332: register stat L =>, !:fun[bag[T2], bag[U]],bag[T2]->bag[U], !:fun[bag[T2], bag[T2]],bag[T2]->bag[T2], &:pred[T2],pred[T2]->pred[T2], \circ:fun[bag[T2], bag[U]],fun[bag[T2], bag[T2]]->fun[bag[T2], bag[U]] .. LP0.1.333: register stat R iterate:pred[T2],fun[T2, U]->fun[bag[T2], bag[U]] .. LP0.1.334: register stat multiset /\, \/, <=> LP0.1.335: register stat L =>, ?:pred[pair[T1, T2]],pair[T1, T2]->Bool, ?:pred[pair[T2, T1]],pair[T2, T1]->Bool .. LP0.1.336: register stat multiset /\, \/, <=>, [__,__]:T2,T1->pair[T2, T1] LP0.1.337: LP0.1.338: LP0.1.339: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.340: order * The formulas cannot be ordered using the current ordering. LP0.1.341: make immune formulas LP0.1.342: LP0.1.343: % L1: Lemmas for Transformation, Pushdown LP0.1.344: % --------------------------------------- LP0.1.345: LP0.1.346: declare variables p: pred [T1], p: pred [T2], q: pred [T2], x: T1, y: T2, r: pred [pair [T1, T2]], f: fun [pair [T1, T2], U], f, g: fun [T2, T2], A: bag [T1], B: bag [T2] .. LP0.1.347: LP0.1.348: % ---------------------------------------------------------- LP0.1.349: set immunity on The immunity is now `on'. LP0.1.350: set name pdLemma1 The name-prefix is now `pdLemma1'. LP0.1.351: prove C (p & q, x) = (C (p, x) & C (q, x)) Attempting to prove conjecture pdLemma1.1: C(p & q, x) = C(p, x) & C(q, x) Conjecture pdLemma1.1 [] Proved by normalization. The formulas cannot be ordered using the current ordering. LP0.1.352: qed All conjectures have been proved. LP0.1.353: % ---------------------------------------------------------- LP0.1.354: LP0.1.355: % ---------------------------------------------------------- LP0.1.356: set name pdLemma2 The name-prefix is now `pdLemma2'. LP0.1.357: prove C (p \oplus fst, x) = K (p:pred[T1] ? x) Attempting to prove conjecture pdLemma2.1: C(p \oplus fst, x) = K(p:pred[T1] ? x) Conjecture pdLemma2.1 [] Proved by normalization. The formulas cannot be ordered using the current ordering. LP0.1.358: qed All conjectures have been proved. LP0.1.359: % ---------------------------------------------------------- LP0.1.360: LP0.1.361: % ---------------------------------------------------------- LP0.1.362: set name pdLemma3 The name-prefix is now `pdLemma3'. LP0.1.363: prove C (p \oplus snd, x) = p Attempting to prove conjecture pdLemma3.1: C(p \oplus snd, x) = p Conjecture pdLemma3.1 [] Proved by normalization. The formulas cannot be ordered using the current ordering. LP0.1.364: qed All conjectures have been proved. LP0.1.365: % ---------------------------------------------------------- LP0.1.366: LP0.1.367: % ---------------------------------------------------------- LP0.1.368: set name pdLemma4 The name-prefix is now `pdLemma4'. LP0.1.369: prove iterate (p & q, f) = iterate (p, f) \circ iterate (q, id) Attempting to prove conjecture pdLemma4.1: iterate(p & q, f) = iterate(p, f) \circ iterate(q, id) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture pdLemma4.1 LP0.1.370: resume by induction on x:bag[T2] Creating subgoals for proof by structural induction on `x:bag[T2]' Basis subgoal: Subgoal 1: (iterate(p & q, f) ! {}):bag[U] = iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! {}) Induction constant: xc Induction hypothesis: pdLemma4InductHyp.1: (iterate(p & q, f) ! xc):bag[U] = iterate(p, f) ! (iterate(q, id) ! xc) Induction subgoal: Subgoal 2: (iterate(p & q, f) ! insert(t, xc)):bag[U] = iterate(p, f) ! (iterate(q, id) ! insert(t, xc)) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on x Level 2 subgoal 1 (basis step) for proof by induction on x [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on x Added hypothesis pdLemma4InductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on x LP0.1.371: resume by cases q ? t Creating subgoals for proof by cases New constants: qc, tc Case hypotheses: pdLemma4CaseHyp.1.1: qc ? tc pdLemma4CaseHyp.1.2: ~(qc ? tc) Same subgoal for all cases: (iterate(p & qc, f) ! insert(tc, xc)):bag[U] = iterate(p, f) ! (iterate(qc, id) ! insert(tc, xc)) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis pdLemma4CaseHyp.1.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for case 1 (out of 2) LP0.1.372: resume by cases p ? tc Creating subgoals for proof by cases New constant: pc Case hypotheses: pdLemma4CaseHyp.2.1: pc ? tc pdLemma4CaseHyp.2.2: ~(pc ? tc) Same subgoal for all cases: (iterate(pc & qc, f) ! insert(tc, xc)):bag[U] = iterate(pc, f) ! insert(tc, iterate(qc, id) ! xc) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis pdLemma4CaseHyp.2.1 to the system. Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis pdLemma4CaseHyp.2.2 to the system. Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for case 1 (out of 2) [] Proved by cases p ? tc. Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis pdLemma4CaseHyp.1.2 to the system. Level 3 subgoal for case 2 (out of 2): (iterate(p & qc, f) ! insert(tc, xc)):bag[U] = iterate(p, f) ! (iterate(qc, id) ! insert(tc, xc)) [] Proved by normalization. Level 2 subgoal 2 (induction step) for proof by induction on x: (iterate(p & q, f) ! insert(t, xc)):bag[U] = iterate(p, f) ! (iterate(q, id) ! insert(t, xc)) [] Proved by cases q ? t. Conjecture pdLemma4.1: iterate(p & q, f) = iterate(p, f) \circ iterate(q, id) [] Proved by structural induction on `x:bag[T2]'. The formulas cannot be ordered using the current ordering. LP0.1.373: qed All conjectures have been proved. LP0.1.374: % ---------------------------------------------------------- LP0.1.375: LP0.1.376: LP0.1.377: % ---------------------------------------------------------- LP0.1.378: set name pdLemma5 The name-prefix is now `pdLemma5'. LP0.1.379: prove iterate (q & (p:pred[T2] \oplus g:fun[T2,T2]), f \circ g) ! B = iterate (p, f:fun[T2,T2]) ! (iterate (q:pred[T2], g) ! B) .. Attempting to prove conjecture pdLemma5.1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! B):bag[T2] = iterate(p, f) ! (iterate(q, g) ! B) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture pdLemma5.1 LP0.1.380: resume by induction on B:bag[T2] Creating subgoals for proof by structural induction on `B:bag[T2]' Basis subgoal: Subgoal 1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! {}):bag[T2] = iterate(p, f) ! (iterate(q, g) ! {}) Induction constant: Bc Induction hypothesis: pdLemma5InductHyp.1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! Bc):bag[T2] = iterate(p, f) ! (iterate(q, g) ! Bc) Induction subgoal: Subgoal 2: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! insert(t, Bc)): bag[T2] = iterate(p, f) ! (iterate(q, g) ! insert(t, Bc)) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on B Level 2 subgoal 1 (basis step) for proof by induction on B [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on B Added hypothesis pdLemma5InductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on B LP0.1.381: resume by cases q ? t Creating subgoals for proof by cases New constants: qc, tc Case hypotheses: pdLemma5CaseHyp.1.1: qc ? tc pdLemma5CaseHyp.1.2: ~(qc ? tc) Same subgoal for all cases: (iterate(qc & (p:pred[T2] \oplus g), f \circ g) ! insert(tc, Bc)):bag[T2] = iterate(p, f) ! (iterate(qc, g) ! insert(tc, Bc)) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis pdLemma5CaseHyp.1.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for case 1 (out of 2) LP0.1.382: resume by cases p:pred[T2] ? (g ! tc) Creating subgoals for proof by cases New constants: pc, gc Case hypotheses: pdLemma5CaseHyp.2.1: pc ? (gc ! tc) pdLemma5CaseHyp.2.2: ~(pc ? (gc ! tc)) Same subgoal for all cases: (iterate(qc & (pc \oplus gc), f \circ gc) ! insert(tc, Bc)):bag[T2] = iterate(pc, f) ! insert(gc ! tc, iterate(qc, gc) ! Bc) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis pdLemma5CaseHyp.2.1 to the system. Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis pdLemma5CaseHyp.2.2 to the system. Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for case 1 (out of 2) [] Proved by cases p:pred[T2] ? (g ! tc). Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis pdLemma5CaseHyp.1.2 to the system. Level 3 subgoal for case 2 (out of 2): (iterate(qc & (p:pred[T2] \oplus g), f \circ g) ! insert(tc, Bc)):bag[T2] = iterate(p, f) ! (iterate(qc, g) ! insert(tc, Bc)) [] Proved by normalization. Level 2 subgoal 2 (induction step) for proof by induction on B: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! insert(t, Bc)):bag[T2] = iterate(p, f) ! (iterate(q, g) ! insert(t, Bc)) [] Proved by cases q ? t. Conjecture pdLemma5.1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! B):bag[T2] = iterate(p, f) ! (iterate(q, g) ! B) [] Proved by structural induction on `B:bag[T2]'. The formulas cannot be ordered using the current ordering. LP0.1.383: qed All conjectures have been proved. LP0.1.384: % ---------------------------------------------------------- LP0.1.385: LP0.1.386: LP0.1.387: % ---------------------------------------------------------- LP0.1.388: set name pdLemma6 The name-prefix is now `pdLemma6'. LP0.1.389: prove iterate (q & (p:pred[T2] \oplus g:fun[T2,T2]), f \circ g) ! B = iterate (p, f:fun[T2,U]) ! (iterate (q:pred[T2], g) ! B) .. Attempting to prove conjecture pdLemma6.1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! B):bag[U] = iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, g) ! B) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture pdLemma6.1 LP0.1.390: resume by induction on B:bag[T2] Creating subgoals for proof by structural induction on `B:bag[T2]' Basis subgoal: Subgoal 1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! {}):bag[U] = iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, g) ! {}) Induction constant: Bc Induction hypothesis: pdLemma6InductHyp.1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! Bc):bag[U] = iterate(p, f) ! (iterate(q, g) ! Bc) Induction subgoal: Subgoal 2: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! insert(t, Bc)): bag[U] = iterate(p, f) ! (iterate(q, g) ! insert(t, Bc)) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on B Level 2 subgoal 1 (basis step) for proof by induction on B [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on B Added hypothesis pdLemma6InductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on B LP0.1.391: resume by cases q ? t Creating subgoals for proof by cases New constants: qc, tc Case hypotheses: pdLemma6CaseHyp.1.1: qc ? tc pdLemma6CaseHyp.1.2: ~(qc ? tc) Same subgoal for all cases: (iterate(qc & (p:pred[T2] \oplus g), f \circ g) ! insert(tc, Bc)):bag[U] = iterate(p, f) ! (iterate(qc, g) ! insert(tc, Bc)) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis pdLemma6CaseHyp.1.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for case 1 (out of 2) LP0.1.392: resume by cases p:pred[T2] ? (g ! tc) Creating subgoals for proof by cases New constants: pc, gc Case hypotheses: pdLemma6CaseHyp.2.1: pc ? (gc ! tc) pdLemma6CaseHyp.2.2: ~(pc ? (gc ! tc)) Same subgoal for all cases: (iterate(qc & (pc \oplus gc), f \circ gc) ! insert(tc, Bc)):bag[U] = iterate(pc, f) ! insert(gc ! tc, iterate(qc, gc) ! Bc) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis pdLemma6CaseHyp.2.1 to the system. Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis pdLemma6CaseHyp.2.2 to the system. Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for case 1 (out of 2) [] Proved by cases p:pred[T2] ? (g ! tc). Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis pdLemma6CaseHyp.1.2 to the system. Level 3 subgoal for case 2 (out of 2): (iterate(qc & (p:pred[T2] \oplus g), f \circ g) ! insert(tc, Bc)):bag[U] = iterate(p, f) ! (iterate(qc, g) ! insert(tc, Bc)) [] Proved by normalization. Level 2 subgoal 2 (induction step) for proof by induction on B: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! insert(t, Bc)):bag[U] = iterate(p, f) ! (iterate(q, g) ! insert(t, Bc)) [] Proved by cases q ? t. Conjecture pdLemma6.1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! B):bag[U] = iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, g) ! B) [] Proved by structural induction on `B:bag[T2]'. The formulas cannot be ordered using the current ordering. LP0.1.393: qed All conjectures have been proved. LP0.1.394: % ---------------------------------------------------------- LP0.1.395: LP0.1.396: % ---------------------------------------------------------- LP0.1.397: set name pdLemma7 The name-prefix is now `pdLemma7'. LP0.1.398: prove iterate (p:pred[T2], f:fun[T2,U]) ! (iterate (q:pred[T2],id) ! B) = iterate (q, f:fun[T2,U]) ! (iterate (p, id) ! B) by induction on B:bag[T2] .. Attempting to prove conjecture pdLemma7.1: (iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! B)):bag[U] = iterate(q, f):fun[bag[T2], bag[U]] ! (iterate(p, id) ! B) Creating subgoals for proof by structural induction on `B:bag[T2]' Basis subgoal: Subgoal 1: (iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! {})): bag[U] = iterate(q, f):fun[bag[T2], bag[U]] ! (iterate(p, id) ! {}) Induction constant: Bc Induction hypothesis: pdLemma7InductHyp.1: (iterate(p, f) ! (iterate(q, id) ! Bc)):bag[U] = iterate(q, f) ! (iterate(p, id) ! Bc) Induction subgoal: Subgoal 2: (iterate(p, f) ! (iterate(q, id) ! insert(t, Bc))):bag[U] = iterate(q, f) ! (iterate(p, id) ! insert(t, Bc)) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on B Level 2 subgoal 1 (basis step) for proof by induction on B [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on B Added hypothesis pdLemma7InductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on B LP0.1.399: resume by cases q ? t Creating subgoals for proof by cases New constants: qc, tc Case hypotheses: pdLemma7CaseHyp.1.1: qc ? tc pdLemma7CaseHyp.1.2: ~(qc ? tc) Same subgoal for all cases: (iterate(p, f) ! (iterate(qc, id) ! insert(tc, Bc))):bag[U] = iterate(qc, f) ! (iterate(p, id) ! insert(tc, Bc)) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis pdLemma7CaseHyp.1.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for case 1 (out of 2) LP0.1.400: resume by cases p ? tc Creating subgoals for proof by cases New constant: pc Case hypotheses: pdLemma7CaseHyp.2.1: pc ? tc pdLemma7CaseHyp.2.2: ~(pc ? tc) Same subgoal for all cases: (iterate(pc, f) ! insert(tc, iterate(qc, id) ! Bc)):bag[U] = iterate(qc, f) ! (iterate(pc, id) ! insert(tc, Bc)) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis pdLemma7CaseHyp.2.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 4 subgoal for case 1 (out of 2) LP0.1.401: instan p by pc, q by qc, B by Bc in *Induct* Formula pdLemma7InductHyp.1 has been instantiated to formula pdLemma7InductHyp.1.1, (iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U] = iterate(qc, f) ! (iterate(pc, id) ! Bc) Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis pdLemma7CaseHyp.2.2 to the system. The formulas cannot be ordered using the current ordering. LP0.1.402: instan p by pc, q by qc, B by Bc in *Induct* Formula pdLemma7InductHyp.1 has been instantiated to formula pdLemma7InductHyp.1.1, (iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U] = iterate(qc, f) ! (iterate(pc, id) ! Bc) Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for case 1 (out of 2): (iterate(p, f) ! (iterate(qc, id) ! insert(tc, Bc))):bag[U] = iterate(qc, f) ! (iterate(p, id) ! insert(tc, Bc)) [] Proved by cases p ? tc. Attempting to prove level 3 subgoal for case 2 (out of 2): (iterate(p, f) ! (iterate(qc, id) ! insert(tc, Bc))):bag[U] = iterate(qc, f) ! (iterate(p, id) ! insert(tc, Bc)) Added hypothesis pdLemma7CaseHyp.1.2 to the system. The formulas cannot be ordered using the current ordering. LP0.1.403: resume by cases p ? tc Creating subgoals for proof by cases New constant: pc Case hypotheses: pdLemma7CaseHyp.2.1: pc ? tc pdLemma7CaseHyp.2.2: ~(pc ? tc) Same subgoal for all cases: (iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U] = iterate(qc, f) ! (iterate(pc, id) ! insert(tc, Bc)) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis pdLemma7CaseHyp.2.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 4 subgoal for case 1 (out of 2) LP0.1.404: instan p by pc, q by qc, B by Bc in *Induct* Formula pdLemma7InductHyp.1 has been instantiated to formula pdLemma7InductHyp.1.1, (iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U] = iterate(qc, f) ! (iterate(pc, id) ! Bc) Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis pdLemma7CaseHyp.2.2 to the system. The formulas cannot be ordered using the current ordering. LP0.1.405: instan p by pc, q by qc, B by Bc in *Induct* Formula pdLemma7InductHyp.1 has been instantiated to formula pdLemma7InductHyp.1.1, (iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U] = iterate(qc, f) ! (iterate(pc, id) ! Bc) Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for case 2 (out of 2): (iterate(p, f) ! (iterate(qc, id) ! insert(tc, Bc))):bag[U] = iterate(qc, f) ! (iterate(p, id) ! insert(tc, Bc)) [] Proved by cases p ? tc. Level 2 subgoal 2 (induction step) for proof by induction on B: (iterate(p, f) ! (iterate(q, id) ! insert(t, Bc))):bag[U] = iterate(q, f) ! (iterate(p, id) ! insert(t, Bc)) [] Proved by cases q ? t. Conjecture pdLemma7.1: (iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! B)):bag[U] = iterate(q, f):fun[bag[T2], bag[U]] ! (iterate(p, id) ! B) [] Proved by structural induction on `B:bag[T2]'. The formulas cannot be ordered using the current ordering. LP0.1.406: qed All conjectures have been proved. LP0.1.407: make immune formulas LP0.1.408: % ---------------------------------------------------------- LP0.1.409: LP0.1.410: % ---------------------------------------------------------- LP0.1.411: set name pdLemma8 The name-prefix is now `pdLemma8'. LP0.1.412: prove K (true) & p:pred[T2] = p Attempting to prove conjecture pdLemma8.1: K(true) & p = p Conjecture pdLemma8.1 [] Proved by normalization. The formulas cannot be ordered using the current ordering. LP0.1.413: qed All conjectures have been proved. LP0.1.414: % ---------------------------------------------------------- LP0.1.415: LP0.1.416: % ---------------------------------------------------------- LP0.1.417: set name pdLemma9 The name-prefix is now `pdLemma9'. LP0.1.418: prove K (false) & p:pred[T2] = K (false) Attempting to prove conjecture pdLemma9.1: K(false) & p = K(false) Conjecture pdLemma9.1 [] Proved by normalization. The formulas cannot be ordered using the current ordering. LP0.1.419: qed All conjectures have been proved. LP0.1.420: % ---------------------------------------------------------- LP0.1.421: LP0.1.422: % ---------------------------------------------------------- LP0.1.423: set name pdLemma10 The name-prefix is now `pdLemma10'. LP0.1.424: prove iterate (K (false), f:fun[T2,U]) ! B = {} by induction on B:bag[T2] Attempting to prove conjecture pdLemma10.1: (iterate(K(false), f) ! B):bag[U] = {} Creating subgoals for proof by structural induction on `B:bag[T2]' Basis subgoal: Subgoal 1: (iterate(K(false), f) ! {}):bag[U] = {} Induction constant: Bc Induction hypothesis: pdLemma10InductHyp.1: (iterate(K(false), f) ! Bc):bag[U] = {} Induction subgoal: Subgoal 2: (iterate(K(false), f) ! insert(t, Bc)):bag[U] = {} Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on B Level 2 subgoal 1 (basis step) for proof by induction on B [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on B Added hypothesis pdLemma10InductHyp.1 to the system. Level 2 subgoal 2 (induction step) for proof by induction on B [] Proved by normalization. Conjecture pdLemma10.1 [] Proved by structural induction on `B:bag[T2]'. The formulas cannot be ordered using the current ordering. LP0.1.425: qed All conjectures have been proved. LP0.1.426: set immunity off The immunity is now `off'. LP0.1.427: LP0.1.428: LP0.1.429: % L1: Rules Used in Transformation, Pushdown LP0.1.430: % ------------------------------------------ LP0.1.431: LP0.1.432: set name push The name-prefix is now `push'. LP0.1.433: LP0.1.434: make passive formulas LP0.1.435: set order left Warning: the rewriting system is known to terminate, but its termination cannot be verified with the `left-to-right' ordering. When another rewrite rule is added, the rewriting system will be treated as nonterminating. The ordering-method is now `left-to-right'. LP0.1.436: LP0.1.437: prove join ((p \oplus fst) & (q \oplus snd) & r, f) ! [A, B] = join (r, f) ! [iterate (p, id) ! A, iterate (q, id) ! B] .. Attempting to prove conjecture push.1: join((p \oplus fst) & (q \oplus snd) & r, f) ! [A, B] = join(r, f) ! [iterate(p, id) ! A, iterate(q, id) ! B] The system now contains 173 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of conjecture push.1 LP0.1.438: LP0.1.439: resume by induction on A:bag[T1] Creating subgoals for proof by structural induction on `A:bag[T1]' Basis subgoal: Subgoal 1: join((p \oplus fst) & (q \oplus snd) & r, f) ! [{}, B] = join(r, f) ! [iterate(p, id) ! {}, iterate(q, id) ! B] Induction constant: Ac Induction hypothesis: pushInductHyp.1: join((p \oplus fst) & (q \oplus snd) & r, f) ! [Ac, B] = join(r, f) ! [iterate(p, id) ! Ac, iterate(q, id) ! B] Induction subgoal: Subgoal 2: join((p \oplus fst) & (q \oplus snd) & r, f) ! [insert(t, Ac), B] = join(r, f) ! [iterate(p, id) ! insert(t, Ac), iterate(q, id) ! B] Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A Level 2 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on A Added hypothesis pushInductHyp.1 to the system. The system now contains 174 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on A LP0.1.440: LP0.1.441: % Base Case: Trivial LP0.1.442: % Inductive Case: LP0.1.443: LP0.1.444: resume by cases p ? t Creating subgoals for proof by cases New constants: pc, tc Case hypotheses: pushCaseHyp.1.1: pc ? tc pushCaseHyp.1.2: ~(pc ? tc) Same subgoal for all cases: (iterate(K(pc ? tc) & q & C(r, tc), C(f, tc)) ! B) \U (join(r, f) ! [iterate(pc, id) ! Ac, iterate(q, id) ! B]) = join(r, f) ! [iterate(pc, id) ! insert(tc, Ac), iterate(q, id) ! B] Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis pushCaseHyp.1.1 to the system. The system now contains 175 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 3 subgoal for case 1 (out of 2) LP0.1.445: LP0.1.446: % Case 1: p ? t LP0.1.447: LP0.1.448: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.449: LP0.1.450: crit-pairs *Lemma* with Composition The following equations are critical pairs between rewrite rules pdLemma4.1 and Composition.2. push.2: (iterate(p & q, f) ! x):bag[U] = iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! x) The system now contains 1 formula and 175 rewrite rules. The rewriting system is NOT guaranteed to terminate. The system now contains 176 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.451: norm conjecture Level 3 subgoal for case 1 (out of 2): (iterate(K(pc ? tc) & q & C(r, tc), C(f, tc)) ! B) \U (join(r, f) ! [iterate(pc, id) ! Ac, iterate(q, id) ! B]) = join(r, f) ! [iterate(pc, id) ! insert(tc, Ac), iterate(q, id) ! B] [] Proved by normalization. Attempting to prove level 3 subgoal for case 2 (out of 2): (iterate(K(pc ? tc) & q & C(r, tc), C(f, tc)) ! B) \U (join(r, f) ! [iterate(pc, id) ! Ac, iterate(q, id) ! B]) = join(r, f) ! [iterate(pc, id) ! insert(tc, Ac), iterate(q, id) ! B] Added hypothesis pushCaseHyp.1.2 to the system. Level 3 subgoal for case 2 (out of 2) [] Proved by normalization. Level 2 subgoal 2 (induction step) for proof by induction on A: join((p \oplus fst) & (q \oplus snd) & r, f) ! [insert(t, Ac), B] = join(r, f) ! [iterate(p, id) ! insert(t, Ac), iterate(q, id) ! B] [] Proved by cases p ? t. Conjecture push.1: join((p \oplus fst) & (q \oplus snd) & r, f) ! [A, B] = join(r, f) ! [iterate(p, id) ! A, iterate(q, id) ! B] [] Proved by structural induction on `A:bag[T1]'. The system now contains 174 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.452: LP0.1.453: % Case 2: ~ (p ? t) LP0.1.454: LP0.1.455: qed All conjectures have been proved. LP0.1.456: make immune formulas LP0.1.457: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.458: LP0.1.459: set name simp The name-prefix is now `simp'. LP0.1.460: prove iterate (K (true), id) ! A = A Attempting to prove conjecture simp.1: iterate(K(true), id) ! A = A Suspending proof of conjecture simp.1 LP0.1.461: resume by induction on A:bag[T2] Creating subgoals for proof by structural induction on `A:bag[T2]' Basis subgoal: Subgoal 1: iterate(K(true), id) ! {} = {} Induction constant: Ac Induction hypothesis: simpInductHyp.1: iterate(K(true), id) ! Ac = Ac Induction subgoal: Subgoal 2: iterate(K(true), id) ! insert(t, Ac) = insert(t, Ac) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A Level 2 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on A Added hypothesis simpInductHyp.1 to the system. Level 2 subgoal 2 (induction step) for proof by induction on A [] Proved by normalization. Conjecture simp.1 [] Proved by structural induction on `A:bag[T2]'. The system now contains 175 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.462: qed All conjectures have been proved. LP0.1.463: LP0.1.464: LP0.1.465: % Section 4: SNF2 LP0.1.466: % LP0.1.467: % Proof Scripts for COKO Transformations: LP0.1.468: % LP0.1.469: % TRANSFORMATION SNF2 LP0.1.470: % USES LP0.1.471: % SimpLits2, LP0.1.472: % CNF, LP0.1.473: % OrderConjs2, LP0.1.474: % pushneg: ~ (p OPLUS f) --> (~ (p)) OPLUS f, LP0.1.475: % init: p --> (K (true) OPLUS (id X #1)) & LP0.1.476: % (K (true) OPLUS (id X #2)) & LP0.1.477: % K (true) & p, LP0.1.478: % pull: (p OPLUS f) | (q OPLUS f) --> (p | q) OPLUS f, LP0.1.479: % shift: p & (q & r) --> (p & r) & q, LP0.1.480: % simplify: K (true) & p --> p LP0.1.481: % BEGIN LP0.1.482: % SimpLits2; LP0.1.483: % CNF; LP0.1.484: % TD {pushneg}; LP0.1.485: % init; LP0.1.486: % BU {pull || {REPEAT shift}}; LP0.1.487: % OrderConjs2; LP0.1.488: % BU {simplify} LP0.1.489: % END LP0.1.490: % LP0.1.491: % TRANSFORMATION SimpLits2 LP0.1.492: % USES LP0.1.493: % SL11: --> K ([x, y]), LP0.1.494: % SL12: f o K (x) --> K (f ! x), LP0.1.495: % SL13: --> o f, LP0.1.496: % SL14: --> o f, LP0.1.497: % SL21: --> o h, LP0.1.498: % SL22: --> o (id X h), LP0.1.499: % SL23: --> o (id X h), LP0.1.500: % SL24: --> o (id X h), LP0.1.501: % SL25: --> o (id X h), LP0.1.502: % SL26: --> o #2, LP0.1.503: % SL27: --> o #2 LP0.1.504: % Shft, LP0.1.505: % Pr2Times, LP0.1.506: % PR1: p OPLUS (f o g) --> p OPLUS f OPLUS g, LP0.1.507: % PR2: p OPLUS K (x) --> K (p ? x) LP0.1.508: % BEGIN LP0.1.509: % BU {Pr2Times || LP0.1.510: % SL11 || SL12 || {{SL13 || SL14} -> Shft} || LP0.1.511: % SL21 || SL22 || SL23 || SL24 || SL25 || SL26 || SL27 || LP0.1.512: % Shft}; LP0.1.513: % BU {PR1 || PR2} LP0.1.514: % END LP0.1.515: % LP0.1.516: % TRANSFORMATION Pr2Times LP0.1.517: % USES LP0.1.518: % CO1: --> (f X g) o (id X h), LP0.1.519: % CO2: --> <#2, #1> o (g X f) o (id X h), LP0.1.520: % CO3: --> (f X g) o #2, LP0.1.521: % CO4: --> <#2, #1> o (g X f) o #2, LP0.1.522: % CO5: --> (f X id) o (id X g), LP0.1.523: % CO6: --> <#2, #1> o (g X id) o (id X f), LP0.1.524: % CO7: <#1, #2> --> id, LP0.1.525: % CO8: f o id --> f, LP0.1.526: % CO9: id o f --> f LP0.1.527: % BEGIN LP0.1.528: % CO1 || CO2 || CO3 || CO4 || CO5 || CO6 || CO7 || CO8 || CO9 LP0.1.529: % END LP0.1.530: % LP0.1.531: % TRANSFORMATION Shft LP0.1.532: % USES LP0.1.533: % SL1: f o #1 o #2 --> f o (#1 o #2), LP0.1.534: % SL2: f o #2 o #2 --> f o (#2 o #2), LP0.1.535: % SL3: f o (g o h) --> (f o g) o h LP0.1.536: % BEGIN LP0.1.537: % REPEAT SL3; LP0.1.538: % {SL1 || SL2} LP0.1.539: % END LP0.1.540: % LP0.1.541: % TRANSFORMATION OrderConjs2 LP0.1.542: % USES LP0.1.543: % OC1: (p OPLUS (id X #1)) & q & r & (r' OPLUS (id X #1)) --> LP0.1.544: % ((p & r') OPLUS (id X #1)) & q & r, LP0.1.545: % OC2: p & (q OPLUS (id X #2)) & r & (r' OPLUS (id X #2)) --> LP0.1.546: % p & ((q & r') OPLUS (id X #2)) & r, LP0.1.547: % OC3: p & q & r & r' --> p & q & (r & r') LP0.1.548: % BEGIN LP0.1.549: % BU {OC1 || OC2 || OC3} LP0.1.550: % END LP0.1.551: % LP0.1.552: % In [CZ98a], the effects of SNF2 are described but the transformations LP0.1.553: % themselves are not presented. The effect of SNF2 on any predicate, p is LP0.1.554: % to rewrite p to the form, LP0.1.555: % LP0.1.556: % (\rho OPLUS (id \times fst)) & (\sigma OPLUS (id \times snd)) & \tau LP0.1.557: % LP0.1.558: % See Section 2 for proofs of rewrite rules: LP0.1.559: % LP0.1.560: % pushneg, pull, shift, simplify (from SNF2), LP0.1.561: % SL11 (SL2 in Section 2), SL12 (SL6 in Section 2), SL13 (SL3 in Section 2), LP0.1.562: % SL14 (SL4 in Section 2), SL21 (SL1 in Section 2), PR1 (SL7 in Section 2), LP0.1.563: % and PR2 (SL8 in Section 2) (from SimpLits2), and LP0.1.564: % OC3 (from OrderConjs2) LP0.1.565: % LP0.1.566: LP0.1.567: clear LP0.1.568: forget Critical pair list cleared. LP0.1.569: unregister registry LP0.1.570: set order manual The ordering-method is now `manual'. LP0.1.571: exec-silently SNF2_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/SNF2_Aux_Axioms.lp'. LP0.1.572: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.573: order * The system now contains 170 rewrite rules. The rewriting system is guaranteed to terminate. All equations have been oriented into rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.574: LP0.1.575: % L1: Rules Used in Transformation, SNF2 LP0.1.576: % -------------------------------------- LP0.1.577: LP0.1.578: set name init The name-prefix is now `init'. LP0.1.579: declare variables p: pred [pair [T1, pair [T2, T3]]] LP0.1.580: prove p = (K (true) \oplus (id \times fst)) & (K (true) \oplus (id \times snd)) & K (true) & p .. Attempting to prove conjecture init.1: p = (K(true) \oplus (id \times fst)) & (K(true) \oplus (id \times snd)) & K(true) & p Conjecture init.1 [] Proved by normalization. Deleted formula init.1, which reduced to `true'. LP0.1.581: qed All conjectures have been proved. LP0.1.582: LP0.1.583: LP0.1.584: % L1: Rules Used in Transformation, SimpLits2 LP0.1.585: % ------------------------------------------- LP0.1.586: LP0.1.587: set name SL22 The name-prefix is now `SL22'. LP0.1.588: declare variables f: fun [T1, U], h: fun [T2, V], g: fun [pair [T1, V], W] .. LP0.1.589: prove \ = \ \circ (id \times h) .. Attempting to prove conjecture SL22.1: \ = \ \circ (id \times h) Suspending proof of conjecture SL22.1 LP0.1.590: declare operator one: pair [T1, T2] -> T1, two: pair [T1, T2] -> T2 .. LP0.1.591: set immunity on The immunity is now `on'. LP0.1.592: instan pr:pair[T1,T2] by x in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y]) Deleted rewrite rule Pairs.1, which reduced to `true'. LP0.1.593: set immunity off The immunity is now `off'. LP0.1.594: LP0.1.595: fix x:T1 as one (x:pair[T1,T2]) in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula SL22.2, \E y:T2 (x:pair[T1, T2] = [one(x), y]) The system now contains 171 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.596: LP0.1.597: fix y:T2 as two (x:pair[T1,T2]) in SL22 / contains-operator (one: pair [T1, T2] -> T1) .. A prenex-existential quantifier in formula SL22.2 has been eliminated to produce formula SL22.3, x = [one(x), two(x)] The system now contains 172 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.598: LP0.1.599: crit-pairs SL22 with ProductsF The following equations are critical pairs between rewrite rules SL22.3 and ProductsF.1. SL22.4: ((f \times g) ! x):pair[T1, V] = [f ! one(x), g ! two(x)] The system now contains 1 formula and 172 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.600: crit-pairs SL22 with Projection The following equations are critical pairs between rewrite rules SL22.3 and Projection.4. SL22.5: snd ! x = two(x) The system now contains 2 formulas and 172 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules SL22.3 and Projection.3. SL22.6: fst:fun[pair[T1, T2], T1] ! x = one(x) The system now contains 1 formula and 174 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Conjecture SL22.1: \ = \ \circ (id \times h) [] Proved by normalization. The system now contains 171 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.601: qed All conjectures have been proved. LP0.1.602: LP0.1.603: set name SL23 The name-prefix is now `SL23'. LP0.1.604: declare variables f: fun [pair [T1, V], W], h: fun [T2, V], g: fun [T1, U] .. LP0.1.605: prove \ = \ \circ (id \times h) .. Attempting to prove conjecture SL23.1: \ = \ \circ (id \times h) Conjecture SL23.1 [] Proved by normalization. Deleted formula SL23.1, which reduced to `true'. LP0.1.606: qed All conjectures have been proved. LP0.1.607: LP0.1.608: set name SL24 The name-prefix is now `SL24'. LP0.1.609: declare variables f: fun [V, W], h: fun [T2, V], g: fun [pair [T1, V], U] .. LP0.1.610: prove \ = \ \circ (id \times h) .. Attempting to prove conjecture SL24.1: \ = \ \circ (id \times h) Suspending proof of conjecture SL24.1 LP0.1.611: declare operator one: pair [T1, T2] -> T1, two: pair [T1, T2] -> T2 .. LP0.1.612: set immunity on The immunity is now `on'. LP0.1.613: instan pr:pair[T1,T2] by x in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y]) Deleted rewrite rule Pairs.1, which reduced to `true'. LP0.1.614: set immunity off The immunity is now `off'. LP0.1.615: LP0.1.616: fix x:T1 as one (x:pair[T1,T2]) in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula SL24.2, \E y:T2 (x:pair[T1, T2] = [one(x), y]) The system now contains 172 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.617: LP0.1.618: fix y:T2 as two (x:pair[T1,T2]) in SL24 / contains-operator (one: pair [T1, T2] -> T1) .. A prenex-existential quantifier in formula SL24.2 has been eliminated to produce formula SL24.3, x = [one(x), two(x)] The system now contains 173 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.619: LP0.1.620: crit-pairs SL24 with ProductsF The following equations are critical pairs between rewrite rules SL24.3 and ProductsF.1. SL24.4: ((f \times g) ! x):pair[T1, V] = [f ! one(x), g ! two(x)] The system now contains 1 formula and 173 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.621: crit-pairs SL24 with Projection The following equations are critical pairs between rewrite rules SL24.3 and Projection.4. SL24.5: snd ! x = two(x) The system now contains 2 formulas and 173 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Conjecture SL24.1: \ = \ \circ (id \times h) [] Proved by normalization. The system now contains 172 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.622: qed All conjectures have been proved. LP0.1.623: LP0.1.624: set name SL25 The name-prefix is now `SL25'. LP0.1.625: declare variables f: fun [pair [T1, V], W], h: fun [T2, V], g: fun [pair [T1, V], U] .. LP0.1.626: prove \ = \ \circ (id \times h) .. Attempting to prove conjecture SL25.1: \ = \ \circ (id \times h) Conjecture SL25.1 [] Proved by normalization. Deleted formula SL25.1, which reduced to `true'. LP0.1.627: qed All conjectures have been proved. LP0.1.628: LP0.1.629: set name SL26 The name-prefix is now `SL26'. LP0.1.630: declare variables f: fun [U, W], h: fun [T2, V], g: fun [T2, U] .. LP0.1.631: prove \ = \ \circ snd .. Attempting to prove conjecture SL26.1: \ = \ \circ snd Conjecture SL26.1 [] Proved by normalization. Deleted formula SL26.1, which reduced to `true'. LP0.1.632: qed All conjectures have been proved. LP0.1.633: LP0.1.634: set name SL27 The name-prefix is now `SL27'. LP0.1.635: declare variables f: fun [T2, W], h: fun [U, V], g: fun [T2, U] .. LP0.1.636: prove \ = \ \circ snd .. Attempting to prove conjecture SL27.1: \ = \ \circ snd Conjecture SL27.1 [] Proved by normalization. Deleted formula SL27.1, which reduced to `true'. LP0.1.637: qed All conjectures have been proved. LP0.1.638: LP0.1.639: LP0.1.640: LP0.1.641: % L1: Rules Used in Transformation, Pr2Times LP0.1.642: % ------------------------------------------ LP0.1.643: LP0.1.644: set name CO1 The name-prefix is now `CO1'. LP0.1.645: declare variables f: fun [T1, U], h: fun [T2, V], g: fun [V, W] .. LP0.1.646: prove \ = (f \times g) \circ (id \times h) .. Attempting to prove conjecture CO1.1: \ = (f \times g) \circ (id \times h) Suspending proof of conjecture CO1.1 LP0.1.647: declare operator one: pair [T1, T2] -> T1, two: pair [T1, T2] -> T2 .. LP0.1.648: set immunity on The immunity is now `on'. LP0.1.649: instan pr:pair[T1,T2] by x in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y]) Deleted rewrite rule Pairs.1, which reduced to `true'. LP0.1.650: set immunity off The immunity is now `off'. LP0.1.651: LP0.1.652: fix x:T1 as one (x:pair[T1,T2]) in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula CO1.2, \E y:T2 (x:pair[T1, T2] = [one(x), y]) The system now contains 173 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.653: LP0.1.654: fix y:T2 as two (x:pair[T1,T2]) in CO1 / contains-operator (one: pair [T1, T2] -> T1) .. A prenex-existential quantifier in formula CO1.2 has been eliminated to produce formula CO1.3, x = [one(x), two(x)] The system now contains 174 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.655: LP0.1.656: crit-pairs CO1 with ProductsF The following equations are critical pairs between rewrite rules CO1.3 and ProductsF.1. CO1.4: ((f \times g) ! x):pair[T1, V] = [f ! one(x), g ! two(x)] The system now contains 1 formula and 174 rewrite rules. The rewriting system is guaranteed to terminate. Deduction rule lp_and_is_true has been applied to formula ProductsF.1 to yield the following formulas, which imply ProductsF.1. ProductsF.1.1: (f:fun[T1, T1] ! x):T1 = f ! one([x, y]) ProductsF.1.2: (g:fun[T2, V] ! y):V = g ! two([x, y]) Critical pair computation abandoned because a theorem has been proved. Conjecture CO1.1: \ = (f \times g) \circ (id \times h) [] Proved by normalization. The system now contains 173 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.657: qed All conjectures have been proved. LP0.1.658: LP0.1.659: set name CO2 The name-prefix is now `CO2'. LP0.1.660: declare variables f: fun [V, W], h: fun [T2, V], g: fun [T1, U] .. LP0.1.661: prove \ = \ \circ (g \times f) \circ (id \times h) .. Attempting to prove conjecture CO2.1: \ = \ \circ (g \times f) \circ (id \times h) Conjecture CO2.1 [] Proved by normalization. Deleted formula CO2.1, which reduced to `true'. LP0.1.662: qed All conjectures have been proved. LP0.1.663: LP0.1.664: set name CO3 The name-prefix is now `CO3'. LP0.1.665: declare variables f: fun [T2, V], g: fun [T4, U] .. LP0.1.666: prove \ = (f:fun [T2, V] \times g:fun [T4, U]) \circ snd .. Attempting to prove conjecture CO3.1: \ = (f \times g) \circ snd Suspending proof of conjecture CO3.1 LP0.1.667: declare operator one: pair [pair [T1, T3], pair[T2, T4]] -> pair[T1, T3], two: pair [pair [T1, T3], pair[T2, T4]] -> pair[T2, T4], one: pair [T1, T3] -> T1, two: pair [T1, T3] -> T3, one: pair [T2, T4] -> T2, two: pair [T2, T4] -> T4 .. LP0.1.668: set immunity on The immunity is now `on'. LP0.1.669: instan pr:pair [pair [T1, T3], pair[T2, T4]] by x in Pairs / contains-oper (=:pair [pair [T1,T3], pair[T2,T4]], pair [pair [T1,T3], pair[T2,T4]] -> Bool) .. Formula Pairs.13 has been instantiated to formula Pairs.13.1, \E x:pair[T1, T3] \E y:pair[T2, T4] (x:pair[pair[T1, T3], pair[T2, T4]] = [x, y]) Deleted rewrite rule Pairs.13, which reduced to `true'. LP0.1.670: set immunity off The immunity is now `off'. LP0.1.671: fix x as one (x:pair [pair [T1, T3], pair[T2, T4]]) in Pairs / contains-oper (=:pair [pair [T1,T3], pair[T2,T4]], pair [pair [T1,T3], pair[T2,T4]] -> Bool) .. A prenex-existential quantifier in formula Pairs.13.1 has been eliminated to produce formula CO3.2, \E y:pair[T2, T4] (x:pair[pair[T1, T3], pair[T2, T4]] = [one(x), y]) The system now contains 174 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.672: fix y as two (x:pair [pair [T1, T3], pair[T2, T4]]) in CO3 / contains-oper (one: pair [pair [T1,T3], pair[T2,T4]] -> pair [T1,T3]) .. A prenex-existential quantifier in formula CO3.2 has been eliminated to produce formula CO3.3, x:pair[pair[T1, T3], pair[T2, T4]] = [one(x), two(x)] The system now contains 175 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.673: LP0.1.674: set immunity on The immunity is now `on'. LP0.1.675: instan pr:pair[T1,T3] by x in Pairs / contains-operator (=:pair[T1,T3],pair[T1,T3]->Bool) .. Formula Pairs.5 has been instantiated to formula Pairs.5.1, \E x:T1 \E y:T3 (x:pair[T1, T3] = [x, y]) Deleted rewrite rule Pairs.5, which reduced to `true'. LP0.1.676: set immunity off The immunity is now `off'. LP0.1.677: LP0.1.678: fix x:T1 as one (x:pair[T1,T3]) in Pairs / contains-operator (=:pair[T1, T3],pair[T1, T3]->Bool) .. A prenex-existential quantifier in formula Pairs.5.1 has been eliminated to produce formula CO3.4, \E y:T3 (x:pair[T1, T3] = [one(x), y]) The system now contains 176 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.679: LP0.1.680: fix y as two (x:pair[T1,T3]) in CO3 / contains-operator (one: pair [T1, T3] -> T1) .. A prenex-existential quantifier in formula CO3.4 has been eliminated to produce formula CO3.5, x:pair[T1, T3] = [one(x), two(x)] The system now contains 177 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.681: LP0.1.682: set immunity on The immunity is now `on'. LP0.1.683: instan pr:pair[T2,T4] by x in Pairs / contains-operator (=:pair[T2,T4],pair[T2,T4]->Bool) .. Formula Pairs.7 has been instantiated to formula Pairs.7.1, \E x:T2 \E y:T4 (x:pair[T2, T4] = [x, y]) Deleted rewrite rule Pairs.7, which reduced to `true'. LP0.1.684: set immunity off The immunity is now `off'. LP0.1.685: LP0.1.686: fix x:T2 as one (x:pair[T2,T4]) in Pairs / contains-operator (=:pair[T2, T4],pair[T2, T4]->Bool) .. A prenex-existential quantifier in formula Pairs.7.1 has been eliminated to produce formula CO3.6, \E y:T4 (x:pair[T2, T4] = [one(x), y]) The system now contains 178 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.687: LP0.1.688: fix y:T4 as two (x:pair[T2,T4]) in CO3 / contains-operator (one: pair [T2, T4] -> T2) .. A prenex-existential quantifier in formula CO3.6 has been eliminated to produce formula CO3.7, x:pair[T2, T4] = [one(x), two(x)] The system now contains 179 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.689: LP0.1.690: crit-pairs CO3 with Projection The following equations are critical pairs between rewrite rules CO3.3 and Projection.16. CO3.8: (snd ! x):pair[T2, T4] = two(x) The system now contains 1 formula and 179 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules CO3.3 and Projection.15. CO3.9: (fst ! x):pair[T1, T3] = one(x) The system now contains 1 formula and 180 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules CO3.7 and Projection.8. CO3.10: (snd ! x):T4 = two(x) The system now contains 1 formula and 181 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules CO3.7 and Projection.7. CO3.11: (fst:fun[pair[T2, T4], T2] ! x):T2 = one(x) The system now contains 1 formula and 182 rewrite rules. The rewriting system is guaranteed to terminate. The system now contains 183 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.691: crit-pairs CO3 with ProductsF The following equations are critical pairs between rewrite rules CO3.7 and ProductsF.2. CO3.12: ((f \times g) ! x):pair[V, U] = [f ! one(x), g ! two(x)] The system now contains 1 formula and 183 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Conjecture CO3.1: \ = (f \times g) \circ snd [] Proved by normalization. The system now contains 174 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.692: qed All conjectures have been proved. LP0.1.693: LP0.1.694: LP0.1.695: set name CO4 The name-prefix is now `CO4'. LP0.1.696: declare variables g: fun [T2, V], f: fun [T4, U] .. LP0.1.697: prove \ = \ \circ (g:fun [T2, V] \times f:fun [T4, U]) \circ snd .. Attempting to prove conjecture CO4.1: \ = \ \circ (g \times f) \circ snd Conjecture CO4.1 [] Proved by normalization. Deleted formula CO4.1, which reduced to `true'. LP0.1.698: qed All conjectures have been proved. LP0.1.699: LP0.1.700: set name CO5 The name-prefix is now `CO5'. LP0.1.701: declare variables g: fun [T2, V], f: fun [T1, U] .. LP0.1.702: prove \ = (f \times id) \circ (id \times g) Attempting to prove conjecture CO5.1: \ = (f \times id) \circ (id \times g) Suspending proof of conjecture CO5.1 LP0.1.703: declare operator one: pair [T1, T2] -> T1, two: pair [T1, T2] -> T2 .. LP0.1.704: set immunity on The immunity is now `on'. LP0.1.705: instan pr:pair[T1,T2] by x in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y]) Deleted rewrite rule Pairs.1, which reduced to `true'. LP0.1.706: set immunity off The immunity is now `off'. LP0.1.707: LP0.1.708: fix x:T1 as one (x:pair[T1,T2]) in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula CO5.2, \E y:T2 (x:pair[T1, T2] = [one(x), y]) The system now contains 175 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.709: LP0.1.710: fix y:T2 as two (x:pair[T1,T2]) in CO5 / contains-operator (one: pair [T1, T2] -> T1) .. A prenex-existential quantifier in formula CO5.2 has been eliminated to produce formula CO5.3, x = [one(x), two(x)] The system now contains 176 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.711: LP0.1.712: crit-pairs CO5 with ProductsF The following equations are critical pairs between rewrite rules CO5.3 and ProductsF.1. CO5.4: ((f \times g) ! x):pair[T1, V] = [f ! one(x), g ! two(x)] The system now contains 1 formula and 176 rewrite rules. The rewriting system is guaranteed to terminate. Deduction rule lp_and_is_true has been applied to formula ProductsF.1 to yield the following formulas, which imply ProductsF.1. ProductsF.1.1: (f:fun[T1, T1] ! x):T1 = f ! one([x, y]) ProductsF.1.2: (g:fun[T2, V] ! y):V = g ! two([x, y]) Deleted formula CO1.1, which reduced to `true'. The system now contains 177 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.713: crit-pairs CO5 with Projection The following equations are critical pairs between rewrite rules CO5.3 and Projection.4. CO5.5: snd ! x = two(x) The system now contains 1 formula and 177 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Conjecture CO5.1: \ = (f \times id) \circ (id \times g) [] Proved by normalization. The system now contains 175 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.714: qed All conjectures have been proved. LP0.1.715: LP0.1.716: set name CO6 The name-prefix is now `CO6'. LP0.1.717: declare variables f: fun [T2, V], g: fun [T1, U] .. LP0.1.718: prove \ = \ \circ (g \times id) \circ (id \times f) .. Attempting to prove conjecture CO6.1: \ = \ \circ (g \times id) \circ (id \times f) Conjecture CO6.1 [] Proved by normalization. Deleted formula CO6.1, which reduced to `true'. LP0.1.719: qed All conjectures have been proved. LP0.1.720: LP0.1.721: set name CO7 The name-prefix is now `CO7'. LP0.1.722: prove \ = id Attempting to prove conjecture CO7.1: \ = id Suspending proof of conjecture CO7.1 LP0.1.723: declare operator one: pair [T1, T2] -> T1, two: pair [T1, T2] -> T2 .. LP0.1.724: set immunity on The immunity is now `on'. LP0.1.725: instan pr:pair[T1,T2] by x in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y]) Deleted rewrite rule Pairs.1, which reduced to `true'. LP0.1.726: set immunity off The immunity is now `off'. LP0.1.727: fix x:T1 as one (x:pair[T1,T2]) in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula CO7.2, \E y:T2 (x:pair[T1, T2] = [one(x), y]) The system now contains 176 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.728: fix y:T2 as two (x:pair[T1,T2]) in CO7 / contains-operator (one: pair [T1, T2] -> T1) .. A prenex-existential quantifier in formula CO7.2 has been eliminated to produce formula CO7.3, x = [one(x), two(x)] The system now contains 177 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.729: crit-pairs CO7 with Projection The following equations are critical pairs between rewrite rules CO7.3 and Projection.4. CO7.4: snd ! x = two(x) The system now contains 1 formula and 177 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules CO7.3 and Projection.3. CO7.5: fst:fun[pair[T1, T2], T1] ! x = one(x) The system now contains 1 formula and 178 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Conjecture CO7.1: \ = id [] Proved by normalization. The system now contains 176 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.730: qed All conjectures have been proved. LP0.1.731: LP0.1.732: set name CO8 The name-prefix is now `CO8'. LP0.1.733: declare variables f: fun [T2, V] LP0.1.734: prove f \circ id = f Attempting to prove conjecture CO8.1: f \circ id = f Conjecture CO8.1 [] Proved by normalization. Deleted formula CO8.1, which reduced to `true'. LP0.1.735: qed All conjectures have been proved. LP0.1.736: LP0.1.737: set name CO9 The name-prefix is now `CO9'. LP0.1.738: declare variables f: fun [T2, V] LP0.1.739: prove id \circ f = f Attempting to prove conjecture CO9.1: id \circ f = f Conjecture CO9.1 [] Proved by normalization. Deleted formula CO9.1, which reduced to `true'. LP0.1.740: qed All conjectures have been proved. LP0.1.741: LP0.1.742: LP0.1.743: % L1: Rules Used in Transformation, Shft LP0.1.744: % -------------------------------------- LP0.1.745: LP0.1.746: set name SL1 The name-prefix is now `SL1'. LP0.1.747: declare variables f: fun [T2, V] .. LP0.1.748: prove f \circ fst \circ snd = f \circ (fst \circ snd) Attempting to prove conjecture SL1.1: f \circ fst \circ snd = f \circ (fst \circ snd) Conjecture SL1.1 [] Proved by normalization. Deleted formula SL1.1, which reduced to `true'. LP0.1.749: qed All conjectures have been proved. LP0.1.750: LP0.1.751: set name SL2 The name-prefix is now `SL2'. LP0.1.752: declare variables f: fun [T4, V] .. LP0.1.753: prove f \circ snd \circ snd = f \circ (snd \circ snd) Attempting to prove conjecture SL2.1: f \circ snd \circ snd = f \circ (snd \circ snd) Conjecture SL2.1 [] Proved by normalization. Deleted formula SL2.1, which reduced to `true'. LP0.1.754: qed All conjectures have been proved. LP0.1.755: LP0.1.756: set name SL3 The name-prefix is now `SL3'. LP0.1.757: declare variables h: fun [T2, U], g: fun [U, V], f: fun [V, W] .. LP0.1.758: prove f \circ (g:fun [U, V] \circ h) = (f \circ g) \circ h Attempting to prove conjecture SL3.1: f \circ (g:fun[U, V] \circ h) = f \circ g \circ h Conjecture SL3.1 [] Proved by normalization. Deleted formula SL3.1, which reduced to `true'. LP0.1.759: qed All conjectures have been proved. LP0.1.760: LP0.1.761: LP0.1.762: % L1: Rules Used in Transformation, OrderConjs2 LP0.1.763: % --------------------------------------------- LP0.1.764: LP0.1.765: set name OC1 The name-prefix is now `OC1'. LP0.1.766: declare variables p, r': pred [pair [T1, T2]], q, r: pred [pair [T1, pair [T2, T3]]] .. LP0.1.767: prove (p \oplus (id \times fst)) & q & r & (r' \oplus (id \times fst)) = ((p & r') \oplus (id \times fst)) & q & r .. Attempting to prove conjecture OC1.1: (p \oplus (id \times fst)) & q & r & (r' \oplus (id \times fst)) = ((p & r') \oplus (id \times fst)) & q & r Conjecture OC1.1 [] Proved by normalization. Deleted formula OC1.1, which reduced to `true'. LP0.1.768: qed All conjectures have been proved. LP0.1.769: LP0.1.770: set name OC2 The name-prefix is now `OC2'. LP0.1.771: declare variables q, r': pred [pair [T1, T3]], p, r: pred [pair [T1, pair [T2, T3]]] .. LP0.1.772: prove p & (q \oplus (id \times snd)) & r & (r' \oplus (id \times snd)) = p & ((q & r') \oplus (id \times snd)) & r .. Attempting to prove conjecture OC2.1: p & (q \oplus (id \times snd)) & r & (r' \oplus (id \times snd)) = p & ((q & r') \oplus (id \times snd)) & r Conjecture OC2.1 [] Proved by normalization. Deleted formula OC2.1, which reduced to `true'. LP0.1.773: qed All conjectures have been proved. LP0.1.774: LP0.1.775: LP0.1.776: % Section 5: Magic LP0.1.777: % LP0.1.778: % Proof Scripts for COKO Transformation, LP0.1.779: % LP0.1.780: % TRANSFORMATION Magic LP0.1.781: % USES LP0.1.782: % SNF2, LP0.1.783: % Pushdown, LP0.1.784: % SimplifyJoin, LP0.1.785: % shift: p & q & r --> p & (q & r), LP0.1.786: % nod: njoin (p, f, g) ! [set ! A, B] --> njoin (p, f, g) ! [A, B], LP0.1.787: % LP0.1.788: % magic: join (q OPLUS (id X #1) & r, f) ! LP0.1.789: % [A, njoin (p, g, h) ! [A', B]] --> LP0.1.790: % join (q OPLUS (id X #1) & r, f) ! LP0.1.791: % [A, njoin (p, g, h) ! [set ! (join (q, #2) ! [A, A']), B]] LP0.1.792: % LP0.1.793: % BEGIN LP0.1.794: % Pushdown; LP0.1.795: % LP0.1.796: % GIVEN join (p, _F) ! _O DO { LP0.1.797: % SNF2 (p); LP0.1.798: % shift (p); LP0.1.799: % magic LP0.1.800: % }; LP0.1.801: % LP0.1.802: % GIVEN _F ! [_O, A], A = _F ! [B, _O] DO { LP0.1.803: % SimplifyJoin (B); LP0.1.804: % nod (A) LP0.1.805: % } LP0.1.806: % LP0.1.807: % END LP0.1.808: % LP0.1.809: % In [CZ98a], only rule magic is described. LP0.1.810: % LP0.1.811: LP0.1.812: clear LP0.1.813: forget Critical pair list cleared. LP0.1.814: unregister registry LP0.1.815: set order manual The ordering-method is now `manual'. LP0.1.816: exec-silently Magic_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/Magic_Aux_Axioms.lp'. LP0.1.817: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.818: order * The formulas cannot be ordered using the current ordering. LP0.1.819: LP0.1.820: % L1: Lemmas for Transformation, Magic LP0.1.821: % ------------------------------------ LP0.1.822: LP0.1.823: set name magicLemma1 The name-prefix is now `magicLemma1'. LP0.1.824: LP0.1.825: declare variables q: pred [pair [W, pair [T1, V]]], f: fun [pair [W, pair [T1, V]], X], A, B: bag [pair [W, pair [T1, V]]] .. LP0.1.826: prove iterate (p, f:fun [pair [W, pair [T1, V]], X]) ! (A \U B) = (iterate (p, f:fun [pair [W, pair [T1, V]], X]) ! A) \U (iterate (p, f:fun [pair [W, pair [T1, V]], X]) ! B) .. Attempting to prove conjecture magicLemma1.1: (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (A \U B)):bag[X] = (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! A) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture magicLemma1.1 LP0.1.827: LP0.1.828: resume by induction on A: bag [pair [W, pair [T1, V]]] Creating subgoals for proof by structural induction on `A:bag[pair[W, pair[T1, V]]]' Basis subgoal: Subgoal 1: (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! ({} \U B)): bag[X] = (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! {}) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) Induction constant: Ac Induction hypothesis: magicLemma1InductHyp.1: iterate(p, f) ! (Ac \U B) = (iterate(p, f) ! Ac) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) Induction subgoal: Subgoal 2: iterate(p, f) ! (insert(p1, Ac) \U B) = (iterate(p, f) ! insert(p1, Ac)) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A Level 2 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on A Added hypothesis magicLemma1InductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on A LP0.1.829: LP0.1.830: % Base Case: Trivial LP0.1.831: % Inductive Case LP0.1.832: resume by cases p ? p1 Creating subgoals for proof by cases New constants: pc, p1c Case hypotheses: magicLemma1CaseHyp.1.1: pc ? p1c magicLemma1CaseHyp.1.2: ~(pc ? p1c) Same subgoal for all cases: iterate(pc, f) ! insert(p1c, Ac \U B) = (iterate(pc, f) ! insert(p1c, Ac)) \U (iterate(pc, f) ! B) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis magicLemma1CaseHyp.1.1 to the system. Level 3 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis magicLemma1CaseHyp.1.2 to the system. Level 3 subgoal for case 2 (out of 2) [] Proved by normalization. Level 2 subgoal 2 (induction step) for proof by induction on A: iterate(p, f) ! (insert(p1, Ac) \U B) = (iterate(p, f) ! insert(p1, Ac)) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) [] Proved by cases p ? p1. Conjecture magicLemma1.1: (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (A \U B)):bag[X] = (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! A) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) [] Proved by structural induction on `A:bag[pair[W, pair[T1, V]]]'. The formulas cannot be ordered using the current ordering. LP0.1.833: LP0.1.834: qed All conjectures have been proved. LP0.1.835: % ---------------------------------------------------------- LP0.1.836: LP0.1.837: % ---------------------------------------------------------- LP0.1.838: set name magicLemma2 The name-prefix is now `magicLemma2'. LP0.1.839: set immunity on The immunity is now `on'. LP0.1.840: declare variables p, q: pred [pair [W, pair [T1, V]]], x: W .. LP0.1.841: prove C (p & q, x) = (C (p, x:W) & C (q, x:W)) Attempting to prove conjecture magicLemma2.1: C(p & q, x) = C(p, x) & C(q, x) Conjecture magicLemma2.1 [] Proved by normalization. The formulas cannot be ordered using the current ordering. LP0.1.842: set immunity off The immunity is now `off'. LP0.1.843: qed All conjectures have been proved. LP0.1.844: % ---------------------------------------------------------- LP0.1.845: LP0.1.846: % ---------------------------------------------------------- LP0.1.847: set name magicLemma3 The name-prefix is now `magicLemma3'. LP0.1.848: LP0.1.849: declare variables q: pred [pair [T1, V]], g: fun [pair [T1, V], pair [W, pair [T1, V]]], p: pred [pair [W, pair [T1, V]]], f: fun [pair [W, pair [T1, V]], X], A: bag [pair [T1, V]] .. LP0.1.850: prove iterate (p, f:fun [pair [W, pair [T1, V]], X]) ! (iterate (q, g:fun [pair [T1, V], pair [W, pair [T1, V]]]) ! A) = iterate (q & (p:pred [pair [W, pair [T1, V]]] \oplus g), f \circ g) ! A .. Attempting to prove conjecture magicLemma3.1: iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (iterate(q, g):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]] ! A) = iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! A The formulas cannot be ordered using the current ordering. Suspending proof of conjecture magicLemma3.1 LP0.1.851: LP0.1.852: resume by induction on A:bag [pair [T1, V]] Creating subgoals for proof by structural induction on `A:bag[pair[T1, V]]' Basis subgoal: Subgoal 1: iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (iterate(q, g):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]] ! {}) = iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! {} Induction constant: Ac Induction hypothesis: magicLemma3InductHyp.1: iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (iterate(q, g) ! Ac) = iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! Ac Induction subgoal: Subgoal 2: iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (iterate(q, g) ! insert(p1, Ac)) = iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! insert(p1, Ac) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A Level 2 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on A Added hypothesis magicLemma3InductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on A LP0.1.853: LP0.1.854: % Base Case: Trivial LP0.1.855: % Inductive Case LP0.1.856: LP0.1.857: resume by cases (q & (p \oplus g:fun [pair [T1, V], pair [W, pair [T1, V]]])) ? p1 .. Creating subgoals for proof by cases New constants: qc, pc, gc, p1c Case hypotheses: magicLemma3CaseHyp.1.1: (qc & (pc \oplus gc)) ? p1c magicLemma3CaseHyp.1.2: ~((qc & (pc \oplus gc)) ? p1c) Same subgoal for all cases: iterate(pc, f) ! (iterate(qc, gc) ! insert(p1c, Ac)) = iterate(qc & (pc \oplus gc), f \circ gc) ! insert(p1c, Ac) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis magicLemma3CaseHyp.1.1 to the system. Deduction rule lp_and_is_true has been applied to formula magicLemma3CaseHyp.1.1 to yield the following formulas, which imply magicLemma3CaseHyp.1.1. magicLemma3CaseHyp.1.1.1: qc ? p1c magicLemma3CaseHyp.1.1.2: pc ? (gc ! p1c) Level 3 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis magicLemma3CaseHyp.1.2 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for case 2 (out of 2) LP0.1.858: LP0.1.859: % Case 1: Trivial LP0.1.860: % Case 2: LP0.1.861: resume by cases qc ? p1c Creating subgoals for proof by cases Case hypotheses: magicLemma3CaseHyp.2.1: qc ? p1c magicLemma3CaseHyp.2.2: ~(qc ? p1c) Same subgoal for all cases: iterate(pc, f) ! (iterate(qc, gc) ! insert(p1c, Ac)) = iterate(qc & (pc \oplus gc), f \circ gc) ! Ac Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis magicLemma3CaseHyp.2.1 to the system. Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis magicLemma3CaseHyp.2.2 to the system. Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for case 2 (out of 2): iterate(pc, f) ! (iterate(qc, gc) ! insert(p1c, Ac)) = iterate(qc & (pc \oplus gc), f \circ gc) ! insert(p1c, Ac) [] Proved by cases qc ? p1c. Level 2 subgoal 2 (induction step) for proof by induction on A: iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (iterate(q, g) ! insert(p1, Ac)) = iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! insert(p1, Ac) [] Proved by cases (q & (p:pred[pair[W, pair[T1, V]]] \oplus g)) ? p1. Conjecture magicLemma3.1: iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (iterate(q, g):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]] ! A) = iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! A [] Proved by structural induction on `A:bag[pair[T1, V]]'. The formulas cannot be ordered using the current ordering. LP0.1.862: qed All conjectures have been proved. LP0.1.863: % ---------------------------------------------------------- LP0.1.864: LP0.1.865: LP0.1.866: % ---------------------------------------------------------- LP0.1.867: set name magicLemma4 The name-prefix is now `magicLemma4'. LP0.1.868: LP0.1.869: declare variables p, q: pred [pair [W, pair [T1, V]]], A: bag [W], B: bag [pair [T1, V]], f: fun [pair [W, pair [T1, V]], X], w: W .. LP0.1.870: LP0.1.871: set order left-to-right Warning: the rewriting system is known to terminate, but its termination cannot be verified with the `left-to-right' ordering. When another rewrite rule is added, the rewriting system will be treated as nonterminating. The ordering-method is now `left-to-right'. LP0.1.872: prove (join (p & q, f) ! [A, B]):bag[X] = iterate (q, f) ! (join (p, id) ! [A, B]) .. Attempting to prove conjecture magicLemma4.1: join(p & q, f) ! [A, B] = iterate(q, f) ! (join(p, id) ! [A, B]) The system now contains 480 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of conjecture magicLemma4.1 LP0.1.873: resume by induction on A: bag [W] Creating subgoals for proof by structural induction on `A:bag[W]' Basis subgoal: Subgoal 1: join(p & q, f) ! [{}, B] = iterate(q, f) ! (join(p, id) ! [{}, B]) Induction constant: Ac Induction hypothesis: magicLemma4InductHyp.1: join(p & q, f) ! [Ac, B] = iterate(q, f) ! (join(p, id) ! [Ac, B]) Induction subgoal: Subgoal 2: join(p & q, f) ! [insert(w, Ac), B] = iterate(q, f) ! (join(p, id) ! [insert(w, Ac), B]) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A Level 2 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on A Added hypothesis magicLemma4InductHyp.1 to the system. The system now contains 481 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on A LP0.1.874: LP0.1.875: % Base Case: Trivial LP0.1.876: % Inductive Case LP0.1.877: LP0.1.878: resume by induction on B:bag [pair [T1, V]] Creating subgoals for proof by structural induction on `B:bag[pair[T1, V]]' Basis subgoal: Subgoal 1: (iterate(C(p, w) & C(q, w), C(f, w)) ! {}) \U (iterate(q, f) ! (join(p, id) ! [Ac, {}])) = (iterate(C(p, w) & (q \oplus C(id, w)), f \circ C(id, w)) ! {}) \U (iterate(q, f) ! (join(p, id) ! [Ac, {}])) Induction constant: Bc Induction hypothesis: magicLemma4InductHyp.2: (iterate(C(p, w) & C(q, w), C(f, w)) ! Bc) \U (iterate(q, f) ! (join(p, id) ! [Ac, Bc])) = (iterate(C(p, w) & (q \oplus C(id, w)), f \circ C(id, w)) ! Bc) \U (iterate(q, f) ! (join(p, id) ! [Ac, Bc])) Induction subgoal: Subgoal 2: (iterate(C(p, w) & C(q, w), C(f, w)) ! insert(p1, Bc)) \U (iterate(q, f) ! (join(p, id) ! [Ac, insert(p1, Bc)])) = (iterate(C(p, w) & (q \oplus C(id, w)), f \circ C(id, w)) ! insert(p1, Bc)) \U (iterate(q, f) ! (join(p, id) ! [Ac, insert(p1, Bc)])) Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on B Level 3 subgoal 1 (basis step) for proof by induction on B [] Proved by normalization. Attempting to prove level 3 subgoal 2 (induction step) for proof by induction on B Added hypothesis magicLemma4InductHyp.2 to the system. The system now contains 482 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 3 subgoal 2 (induction step) for proof by induction on B LP0.1.879: LP0.1.880: % Base Case: Trivial LP0.1.881: % Inductive Case LP0.1.882: LP0.1.883: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.884: resume by cases (p & q) ? [w, p1] Creating subgoals for proof by cases New constants: pc, qc, wc, p1c Case hypotheses: magicLemma4CaseHyp.1.1: (pc & qc) ? [wc, p1c] magicLemma4CaseHyp.1.2: ~((pc & qc) ? [wc, p1c]) Same subgoal for all cases: (iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) = (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis magicLemma4CaseHyp.1.1 to the system. Deduction rule lp_and_is_true has been applied to formula magicLemma4CaseHyp.1.1 to yield the following formulas, which imply magicLemma4CaseHyp.1.1. magicLemma4CaseHyp.1.1.1: pc ? [wc, p1c] magicLemma4CaseHyp.1.1.2: qc ? [wc, p1c] The system now contains 484 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 4 subgoal for case 1 (out of 2) LP0.1.885: LP0.1.886: % Case 1 LP0.1.887: LP0.1.888: set immunity on The immunity is now `on'. LP0.1.889: prove C (qc, wc) = qc \oplus C (id, wc) Attempting to prove level 5 lemma magicLemma4.2: C(qc, wc) = qc \oplus C(id, wc) Level 5 lemma magicLemma4.2 [] Proved by normalization. Attempting to prove level 4 subgoal for case 1 (out of 2): (iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) = (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) Current subgoal: insert(f ! [wc, p1c], (iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! Bc) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc])))) = insert(f ! [wc, p1c], (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc)) ! Bc) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc])))) The system now contains 485 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 4 subgoal for case 1 (out of 2) LP0.1.890: set immunity off The immunity is now `off'. LP0.1.891: LP0.1.892: set immunity on The immunity is now `on'. LP0.1.893: prove C (f, wc) = f \circ C (id, wc) Attempting to prove level 5 lemma magicLemma4.3: C(f, wc) = f \circ C(id, wc) Level 5 lemma magicLemma4.3 [] Proved by normalization. Attempting to prove level 4 subgoal for case 1 (out of 2) Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2): (iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) = (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) Added hypothesis magicLemma4CaseHyp.1.2 to the system. The system now contains 483 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 4 subgoal for case 2 (out of 2) LP0.1.894: set immunity off The immunity is now `off'. LP0.1.895: LP0.1.896: % Case 2 LP0.1.897: LP0.1.898: set immunity on The immunity is now `on'. LP0.1.899: prove C (qc, wc) = qc \oplus C (id, wc) Attempting to prove level 5 lemma magicLemma4.2: C(qc, wc) = qc \oplus C(id, wc) Level 5 lemma magicLemma4.2 [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) The system now contains 484 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 4 subgoal for case 2 (out of 2) LP0.1.900: set immunity off The immunity is now `off'. LP0.1.901: LP0.1.902: set immunity on The immunity is now `on'. LP0.1.903: prove C (f, wc) = f \circ C (id, wc) Attempting to prove level 5 lemma magicLemma4.3: C(f, wc) = f \circ C(id, wc) Level 5 lemma magicLemma4.3 [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2): (iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) = (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) Current subgoal: (iterate(C(pc, wc) & (qc \oplus C(id, wc)), C(f, wc)) ! Bc) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) = (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc)) ! Bc) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal 2 (induction step) for proof by induction on B: (iterate(C(p, w) & C(q, w), C(f, w)) ! insert(p1, Bc)) \U (iterate(q, f) ! (join(p, id) ! [Ac, insert(p1, Bc)])) = (iterate(C(p, w) & (q \oplus C(id, w)), f \circ C(id, w)) ! insert(p1, Bc)) \U (iterate(q, f) ! (join(p, id) ! [Ac, insert(p1, Bc)])) [] Proved by cases (p & q) ? [w, p1]. Level 2 subgoal 2 (induction step) for proof by induction on A: join(p & q, f) ! [insert(w, Ac), B] = iterate(q, f) ! (join(p, id) ! [insert(w, Ac), B]) [] Proved by structural induction on `B:bag[pair[T1, V]]'. Conjecture magicLemma4.1: join(p & q, f) ! [A, B] = iterate(q, f) ! (join(p, id) ! [A, B]) [] Proved by structural induction on `A:bag[W]'. The system now contains 481 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.904: set immunity off The immunity is now `off'. LP0.1.905: LP0.1.906: qed All conjectures have been proved. LP0.1.907: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.908: % ---------------------------------------------------------- LP0.1.909: LP0.1.910: % ---------------------------------------------------------- LP0.1.911: set name magicLemma5a The name-prefix is now `magicLemma5a'. LP0.1.912: declare variables p: pred [pair [W, pair [T1, V]]], A: bag [W], B: bag [pair [T1, V]], f: fun [pair [W, pair [T1, V]], pair [W, pair [T1, V]]], X, Y, Z: bag [pair [W, pair [T1, V]]] .. LP0.1.913: LP0.1.914: prove X \U Y = Y \U X by induction on X Attempting to prove conjecture magicLemma5a.1: X \U Y = Y \U X Creating subgoals for proof by structural induction on `X' Basis subgoal: Subgoal 1: {} \U Y = Y \U {} Induction constant: Xc Induction hypothesis: magicLemma5aInductHyp.1: Xc \U Y = Y \U Xc Induction subgoal: Subgoal 2: insert(p1, Xc) \U Y = Y \U insert(p1, Xc) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on X Level 2 subgoal 1 (basis step) for proof by induction on X [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on X Added hypothesis magicLemma5aInductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on X LP0.1.915: resume by induction on Y Creating subgoals for proof by structural induction on `Y' Basis subgoal: Subgoal 1: insert(p1, Xc \U {}) = insert(p1, {} \U Xc) Induction constant: Yc Induction hypothesis: magicLemma5aInductHyp.2: insert(p1, Xc \U Yc) = insert(p1, Yc \U Xc) Induction subgoal: Subgoal 2: insert(p1, Xc \U insert(p2, Yc)) = insert(p1, insert(p2, Yc) \U Xc) Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on Y Level 3 subgoal 1 (basis step) for proof by induction on Y [] Proved by normalization. Attempting to prove level 3 subgoal 2 (induction step) for proof by induction on Y Added hypothesis magicLemma5aInductHyp.2 to the system. Normalization of the term insert(p1, Xc \U insert(p2, Yc)) = insert(p1, insert(p2, Yc) \U Xc) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to insert(p1, insert(p2, Xc \U Yc)) = insert(p2, insert(p1, Yc \U Xc)) Normalization of the term insert(p1, insert(p2, Xc \U Yc)) = insert(p2, insert(p1, Yc \U Xc)) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to insert(p2, insert(p1, Xc \U Yc)) = insert(p2, insert(p1, Yc \U Xc)) The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal 2 (induction step) for proof by induction on Y LP0.1.916: resume by contradiction Creating subgoals for proof by contradiction New constants: p2c, p1c Hypothesis: magicLemma5aContraHyp.1: ~(insert(p2c, insert(p1c, Xc \U Yc)) = insert(p2c, insert(p1c, Yc \U Xc))) Only subgoal: false Attempting to prove level 4 subgoal for proof by contradiction Added hypothesis magicLemma5aContraHyp.1 to the system. Normalization of the term ~(insert(p2c, insert(p1c, Xc \U Yc)) = insert(p2c, insert(p1c, Yc \U Xc))) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to ~(insert(p1c, insert(p2c, Xc \U Yc)) = insert(p2c, insert(p1c, Yc \U Xc))) The formulas cannot be ordered using the current ordering. Suspending proof of level 4 subgoal for proof by contradiction LP0.1.917: crit-pairs *Contra* with *Induct* The following equations are critical pairs between rewrite rules magicLemma5aContraHyp.1 and magicLemma5aInductHyp.2. magicLemma5a.2: false The system now contains 2 formulas and 483 rewrite rules. The rewriting system is NOT guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Formula magicLemma5a.2, false, is inconsistent. Level 4 subgoal for proof by contradiction [] Proved by detecting an inconsistency. Level 3 subgoal 2 (induction step) for proof by induction on Y: insert(p1, Xc \U insert(p2, Yc)) = insert(p1, insert(p2, Yc) \U Xc) [] Proved by contradiction. Level 2 subgoal 2 (induction step) for proof by induction on X: insert(p1, Xc) \U Y = Y \U insert(p1, Xc) [] Proved by structural induction on `Y'. Conjecture magicLemma5a.1: X \U Y = Y \U X [] Proved by structural induction on `X'. The formulas cannot be ordered using the current ordering. LP0.1.918: qed All conjectures have been proved. LP0.1.919: % ---------------------------------------------------------- LP0.1.920: LP0.1.921: % ---------------------------------------------------------- LP0.1.922: set name magicLemma5b The name-prefix is now `magicLemma5b'. LP0.1.923: prove X \U (Y \U Z) = (X \U Z) \U Y Attempting to prove conjecture magicLemma5b.1: X \U (Y \U Z) = X \U Z \U Y The formulas cannot be ordered using the current ordering. Suspending proof of conjecture magicLemma5b.1 LP0.1.924: resume by induction on X Creating subgoals for proof by structural induction on `X' Basis subgoal: Subgoal 1: {} \U (Y \U Z) = {} \U Z \U Y Induction constant: Xc Induction hypothesis: magicLemma5bInductHyp.1: Xc \U (Y \U Z) = Xc \U Z \U Y Induction subgoal: Subgoal 2: insert(p1, Xc) \U (Y \U Z) = insert(p1, Xc) \U Z \U Y Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on X The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 1 (basis step) for proof by induction on X LP0.1.925: resume by induction on Y Creating subgoals for proof by structural induction on `Y' Basis subgoal: Subgoal 1: {} \U Z = Z \U {} Induction constant: Yc Induction hypothesis: magicLemma5bInductHyp.1: Yc \U Z = Z \U Yc Induction subgoal: Subgoal 2: insert(p1, Yc) \U Z = Z \U insert(p1, Yc) Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on Y Level 3 subgoal 1 (basis step) for proof by induction on Y [] Proved by normalization. Attempting to prove level 3 subgoal 2 (induction step) for proof by induction on Y Added hypothesis magicLemma5bInductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal 2 (induction step) for proof by induction on Y LP0.1.926: resume by induction on Z Creating subgoals for proof by structural induction on `Z' Basis subgoal: Subgoal 1: insert(p1, Yc \U {}) = insert(p1, {} \U Yc) Induction constant: Zc Induction hypothesis: magicLemma5bInductHyp.2: insert(p1, Yc \U Zc) = insert(p1, Zc \U Yc) Induction subgoal: Subgoal 2: insert(p1, Yc \U insert(p2, Zc)) = insert(p1, insert(p2, Zc) \U Yc) Attempting to prove level 4 subgoal 1 (basis step) for proof by induction on Z Level 4 subgoal 1 (basis step) for proof by induction on Z [] Proved by normalization. Attempting to prove level 4 subgoal 2 (induction step) for proof by induction on Z Added hypothesis magicLemma5bInductHyp.2 to the system. Normalization of the term insert(p1, Yc \U insert(p2, Zc)) = insert(p1, insert(p2, Zc) \U Yc) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to insert(p1, insert(p2, Yc \U Zc)) = insert(p2, insert(p1, Zc \U Yc)) Normalization of the term insert(p1, insert(p2, Yc \U Zc)) = insert(p2, insert(p1, Zc \U Yc)) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to insert(p2, insert(p1, Yc \U Zc)) = insert(p2, insert(p1, Zc \U Yc)) The formulas cannot be ordered using the current ordering. Suspending proof of level 4 subgoal 2 (induction step) for proof by induction on Z LP0.1.927: resume by contradiction Creating subgoals for proof by contradiction New constants: p2c, p1c Hypothesis: magicLemma5bContraHyp.1: ~(insert(p2c, insert(p1c, Yc \U Zc)) = insert(p2c, insert(p1c, Zc \U Yc))) Only subgoal: false Attempting to prove level 5 subgoal for proof by contradiction Added hypothesis magicLemma5bContraHyp.1 to the system. Normalization of the term ~(insert(p2c, insert(p1c, Yc \U Zc)) = insert(p2c, insert(p1c, Zc \U Yc))) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to ~(insert(p1c, insert(p2c, Yc \U Zc)) = insert(p2c, insert(p1c, Zc \U Yc))) The formulas cannot be ordered using the current ordering. Suspending proof of level 5 subgoal for proof by contradiction LP0.1.928: crit-pairs *Contra* with *Induct* The following equations are critical pairs between rewrite rules magicLemma5bContraHyp.1 and magicLemma5bInductHyp.2. magicLemma5b.2: false The system now contains 3 formulas and 483 rewrite rules. The rewriting system is NOT guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Formula magicLemma5b.2, false, is inconsistent. Level 5 subgoal for proof by contradiction [] Proved by detecting an inconsistency. Level 4 subgoal 2 (induction step) for proof by induction on Z: insert(p1, Yc \U insert(p2, Zc)) = insert(p1, insert(p2, Zc) \U Yc) [] Proved by contradiction. Level 3 subgoal 2 (induction step) for proof by induction on Y: insert(p1, Yc) \U Z = Z \U insert(p1, Yc) [] Proved by structural induction on `Z'. Level 2 subgoal 1 (basis step) for proof by induction on X: {} \U (Y \U Z) = {} \U Z \U Y [] Proved by structural induction on `Y'. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on X: insert(p1, Xc) \U (Y \U Z) = insert(p1, Xc) \U Z \U Y Added hypothesis magicLemma5bInductHyp.1 to the system. Level 2 subgoal 2 (induction step) for proof by induction on X [] Proved by normalization. Conjecture magicLemma5b.1: X \U (Y \U Z) = X \U Z \U Y [] Proved by structural induction on `X'. The formulas cannot be ordered using the current ordering. LP0.1.929: qed All conjectures have been proved. LP0.1.930: % ---------------------------------------------------------- LP0.1.931: LP0.1.932: % ---------------------------------------------------------- LP0.1.933: set name magicLemma5c The name-prefix is now `magicLemma5c'. LP0.1.934: prove join (p, f:fun [pair [W, pair [T1, V]], pair [W, pair [T1, V]]]) ! [A, B] = join (p, f) ! [A, iterate (ex (p\inv) \oplus \, id) ! B] .. Attempting to prove conjecture magicLemma5c.1: (join(p, f) ! [A, B]):bag[pair[W, pair[T1, V]]] = join(p, f) ! [A, iterate(ex(p\inv) \oplus \, id) ! B] The formulas cannot be ordered using the current ordering. Suspending proof of conjecture magicLemma5c.1 LP0.1.935: resume by induction on A:bag [W] Creating subgoals for proof by structural induction on `A:bag[W]' Basis subgoal: Subgoal 1: (join(p, f) ! [{}, B]):bag[pair[W, pair[T1, V]]] = join(p, f) ! [{}, iterate(ex(p\inv) \oplus \, id) ! B] Induction constant: Ac Induction hypothesis: magicLemma5cInductHyp.1: (join(p, f) ! [Ac, B]):bag[pair[W, pair[T1, V]]] = join(p, f) ! [Ac, iterate(ex(p\inv) \oplus \, id) ! B] Induction subgoal: Subgoal 2: (join(p, f) ! [insert(w, Ac), B]):bag[pair[W, pair[T1, V]]] = join(p, f) ! [insert(w, Ac), iterate(ex(p\inv) \oplus \, id) ! B] Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A Level 2 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on A Added hypothesis magicLemma5cInductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on A LP0.1.936: LP0.1.937: % Base Case LP0.1.938: % Inductive Case LP0.1.939: LP0.1.940: resume by induction on B:bag[pair [T1, V]] Creating subgoals for proof by structural induction on `B:bag[pair[T1, V]]' Basis subgoal: Subgoal 1: ((iterate(C(p, w), C(f, w)) ! {}) \U (join(p, f) ! [Ac, {}])): bag[pair[W, pair[T1, V]]] = (iterate(C(p, w), C(f, w)) ! (iterate(ex(p\inv) \oplus \, id) ! {})) \U (join(p, f) ! [Ac, iterate(ex(p\inv) \oplus \, id) ! {}]) Induction constant: Bc Induction hypothesis: magicLemma5cInductHyp.2: ((iterate(C(p, w), C(f, w)) ! Bc) \U (join(p, f) ! [Ac, Bc])): bag[pair[W, pair[T1, V]]] = (iterate(C(p, w), C(f, w)) ! (iterate(ex(p\inv) \oplus \, id) ! Bc)) \U (join(p, f) ! [Ac, iterate(ex(p\inv) \oplus \, id) ! Bc]) Induction subgoal: Subgoal 2: ((iterate(C(p, w), C(f, w)) ! insert(p1, Bc)) \U (join(p, f) ! [Ac, insert(p1, Bc)])): bag[pair[W, pair[T1, V]]] = (iterate(C(p, w), C(f, w)) ! (iterate(ex(p\inv) \oplus \, id) ! insert(p1, Bc))) \U (join(p, f) ! [Ac, iterate(ex(p\inv) \oplus \, id) ! insert(p1, Bc)]) Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on B Level 3 subgoal 1 (basis step) for proof by induction on B [] Proved by normalization. Attempting to prove level 3 subgoal 2 (induction step) for proof by induction on B Added hypothesis magicLemma5cInductHyp.2 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal 2 (induction step) for proof by induction on B LP0.1.941: LP0.1.942: % Base Case LP0.1.943: % Inductive Case LP0.1.944: LP0.1.945: resume by cases (ex(p\inv) \oplus \) ? p1 Creating subgoals for proof by cases New constants: pc, wc, p1c Case hypotheses: magicLemma5cCaseHyp.1.1: (ex(pc\inv) \oplus \) ? p1c magicLemma5cCaseHyp.1.2: ~((ex(pc\inv) \oplus \) ? p1c) Same subgoal for all cases: ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! (iterate(ex(pc\inv) \oplus \, id) ! insert(p1c, Bc))) \U (join(pc, f) ! [Ac, iterate(ex(pc\inv) \oplus \, id) ! insert(p1c, Bc)]) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis magicLemma5cCaseHyp.1.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 4 subgoal for case 1 (out of 2) LP0.1.946: LP0.1.947: % Case 1 LP0.1.948: LP0.1.949: resume by cases pc ? [wc, p1c] Creating subgoals for proof by cases Case hypotheses: magicLemma5cCaseHyp.2.1: pc ? [wc, p1c] magicLemma5cCaseHyp.2.2: ~(pc ? [wc, p1c]) Same subgoal for all cases: ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! insert(p1c, iterate(ex(pc\inv) \oplus \, id) ! Bc)) \U (join(pc, f) ! [Ac, iterate(ex(pc\inv) \oplus \, id) ! Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac) Attempting to prove level 5 subgoal for case 1 (out of 2) Added hypothesis magicLemma5cCaseHyp.2.1 to the system. Level 5 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 5 subgoal for case 2 (out of 2) Added hypothesis magicLemma5cCaseHyp.2.2 to the system. Level 5 subgoal for case 2 (out of 2) [] Proved by normalization. Level 4 subgoal for case 1 (out of 2): ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! (iterate(ex(pc\inv) \oplus \, id) ! insert(p1c, Bc))) \U (join(pc, f) ! [Ac, iterate(ex(pc\inv) \oplus \, id) ! insert(p1c, Bc)]) [] Proved by cases pc ? [wc, p1c]. Attempting to prove level 4 subgoal for case 2 (out of 2): ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! (iterate(ex(pc\inv) \oplus \, id) ! insert(p1c, Bc))) \U (join(pc, f) ! [Ac, iterate(ex(pc\inv) \oplus \, id) ! insert(p1c, Bc)]) Added hypothesis magicLemma5cCaseHyp.1.2 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 4 subgoal for case 2 (out of 2) LP0.1.950: LP0.1.951: % Case 2 LP0.1.952: LP0.1.953: resume by cases pc ? [wc, p1c] Creating subgoals for proof by cases Case hypotheses: magicLemma5cCaseHyp.2.1: pc ? [wc, p1c] magicLemma5cCaseHyp.2.2: ~(pc ? [wc, p1c]) Same subgoal for all cases: ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! Bc) \U (join(pc, f) ! [Ac, Bc]) Attempting to prove level 5 subgoal for case 1 (out of 2) Added hypothesis magicLemma5cCaseHyp.2.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 5 subgoal for case 1 (out of 2) LP0.1.954: % Case 1 LP0.1.955: prove \E y:W (y:W \in insert(wc, Ac) /\ (pc\inv) ? [p1c, y]) by specializing y to wc .. Attempting to prove level 6 lemma magicLemma5c.2: \E y:W (y \in insert(wc, Ac) /\ (pc\inv) ? [p1c, y]) Creating subgoals for proof by specialization Subgoal: wc \in insert(wc, Ac) /\ (pc\inv) ? [p1c, wc] Attempting to prove level 7 subgoal for proof by specialization Level 7 subgoal for proof by specialization [] Proved by normalization. Level 6 lemma magicLemma5c.2 [] Proved by specialization. Attempting to prove level 5 subgoal for case 1 (out of 2) Formula magicLemma5c.2, false, is inconsistent. Level 5 subgoal for case 1 (out of 2): ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! Bc) \U (join(pc, f) ! [Ac, Bc]) [] Proved by impossible case. Attempting to prove level 5 subgoal for case 2 (out of 2): ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! Bc) \U (join(pc, f) ! [Ac, Bc]) Added hypothesis magicLemma5cCaseHyp.2.2 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 5 subgoal for case 2 (out of 2) LP0.1.956: LP0.1.957: % Case 2 LP0.1.958: LP0.1.959: prove (iterate(C(pc\inv, p1c), C(f:fun [pair [W, pair [T1, V]], pair [W, pair [T1, V]]] \circ \, p1c)) ! Ac) = {} by contradiction .. Attempting to prove level 6 lemma magicLemma5c.2: (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac): bag[pair[W, pair[T1, V]]] = {}