LP (the Larch Prover), Release 3.1a (95/04/27) logging to `/pro/oodb/specs/KOLA98/VLDB98_Scripts.lplog' on 21 June 1998 18:34:43. LP0.1.2: LP0.1.3: % ****************************************************************************** LP0.1.4: % * * LP0.1.5: % * Script File: VLDB98_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: % * [CZ98b]: * LP0.1.17: % * * LP0.1.18: % * [CZ98b] Inferring Function Semantics to Optimize Queries, * LP0.1.19: % * Mitch Cherniack and Stan Zdonik, In Proceedings of the 24th * LP0.1.20: % * International Conference on Very Large Data Bases, New York, * LP0.1.21: % * NY, August, 1998 * LP0.1.22: % * * LP0.1.23: % * For an up-to-date version of [CZ98b], see: * LP0.1.24: % * ftp://wilma.cs.brown.edu/u/mfc/vldb98.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 VLDB98_Scripts * LP0.1.38: % * * LP0.1.39: % ****************************************************************************** LP0.1.40: LP0.1.41: % Section 1: Injectivity Inference Rules LP0.1.42: % LP0.1.43: % Proof Scripts for the Inference Rules of Figure 4a LP0.1.44: % LP0.1.45: % is_inj (id) LP0.1.46: % is_key (f) => is_inj (f) LP0.1.47: % is_inj (f) /\ is_inj (g) => is_inj (f \circ g) LP0.1.48: % is_inj (f) \/ is_inj (g) => is_inj (\) LP0.1.49: % is_inj (f) => is_inj (iterate (K (true), f) LP0.1.50: % LP0.1.51: % Note that the 2nd rule relies on a correct identification by DB managers LP0.1.52: % as to what is a key. The formal specification of a key is identical to LP0.1.53: % that of an injective function and therefore the proof of this rule LP0.1.54: % is trivial. LP0.1.55: % LP0.1.56: LP0.1.57: LP0.1.58: clear LP0.1.59: set order manual The ordering-method is now `manual'. LP0.1.60: exec-silently Inj_Inf_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/Inj_Inf_Aux_Axioms.lp'. LP0.1.61: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.62: order formulas The formulas cannot be ordered using the current ordering. LP0.1.63: make immune formulas LP0.1.64: LP0.1.65: declare variables f, g: fun [T, U], g: fun [T, V], f: fun [U, V] .. LP0.1.66: LP0.1.67: LP0.1.68: % L1: Rules for Inference of Injectivity LP0.1.69: % -------------------------------------- LP0.1.70: LP0.1.71: set name inj_inf1 The name-prefix is now `inj_inf1'. LP0.1.72: prove is_inj (id) Attempting to prove conjecture inj_inf1.1: is_inj(id) Conjecture inj_inf1.1 [] Proved by normalization. Deleted formula inj_inf1.1, which reduced to `true'. The formulas cannot be ordered using the current ordering. LP0.1.73: qed All conjectures have been proved. LP0.1.74: LP0.1.75: set name inj_inf2 The name-prefix is now `inj_inf2'. LP0.1.76: prove is_key (f:fun[T,U]) => is_inj (f:fun[T,U]) Attempting to prove conjecture inj_inf2.1: is_key(f:fun[T, U]) => is_inj(f:fun[T, U]) Conjecture inj_inf2.1 [] Proved by normalization. Deleted formula inj_inf2.1, which reduced to `true'. The formulas cannot be ordered using the current ordering. LP0.1.77: qed All conjectures have been proved. LP0.1.78: LP0.1.79: set name inj_inf3 The name-prefix is now `inj_inf3'. LP0.1.80: 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.81: prove is_inj (f:fun[U,V]) /\ is_inj (g:fun[T,U]) => is_inj (f \circ g) Attempting to prove conjecture inj_inf3.1: is_inj(f:fun[U, V]) /\ is_inj(g:fun[T, U]) => is_inj(f \circ g) The system now contains 93 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of conjecture inj_inf3.1 LP0.1.82: resume by => Creating subgoals for proof of => New constants: gc, fc Hypothesis: inj_inf3ImpliesHyp.1: \A x:U \A y:U (fc ! x = fc ! y => x:U = y) /\ \A x:T \A y:T (gc ! x = gc ! y => x:T = y) Subgoal: \A x:T \A y:T (fc ! (gc ! x) = fc ! (gc ! y) => x:T = y) Attempting to prove level 2 subgoal for proof of => Added hypothesis inj_inf3ImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula inj_inf3ImpliesHyp.1 to yield the following formulas, which imply inj_inf3ImpliesHyp.1. inj_inf3ImpliesHyp.1.1: \A x:T \A y:T (gc ! x = gc ! y => x:T = y) inj_inf3ImpliesHyp.1.2: \A x:U \A y:U (fc ! x = fc ! y => x:U = y) The system now contains 95 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 2 subgoal for proof of => LP0.1.83: resume by => Creating subgoals for proof of => New constants: xc, yc Hypothesis: inj_inf3ImpliesHyp.2: fc ! (gc ! xc) = fc ! (gc ! yc) Subgoal: xc = yc Attempting to prove level 3 subgoal for proof of => Added hypothesis inj_inf3ImpliesHyp.2 to the system. The system now contains 96 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 3 subgoal for proof of => LP0.1.84: resume by contradiction Creating subgoals for proof by contradiction Hypothesis: inj_inf3ContraHyp.1: ~(xc = yc) Only subgoal: false Attempting to prove level 4 subgoal for proof by contradiction Added hypothesis inj_inf3ContraHyp.1 to the system. The system now contains 97 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 4 subgoal for proof by contradiction LP0.1.85: crit-pairs *Contra* with *Implies* The following equations are critical pairs between rewrite rules inj_inf3ContraHyp.1 and inj_inf3ImpliesHyp.1.1. inj_inf3.2: ~(gc ! xc = gc ! yc) inj_inf3.3: ~(gc ! yc = gc ! xc) The system now contains 2 formulas and 97 rewrite rules. The rewriting system is NOT guaranteed to terminate. Deleted formula inj_inf3.3, which reduced to `true'. The system now contains 98 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.86: crit-pairs inj_inf3 with *Implies* The following equations are critical pairs between rewrite rules inj_inf3.2 and inj_inf3ImpliesHyp.1.2. inj_inf3.4: false inj_inf3.5: false The system now contains 2 formulas and 98 rewrite rules. The rewriting system is NOT guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Formula inj_inf3.4, false, is inconsistent. Level 4 subgoal for proof by contradiction [] Proved by detecting an inconsistency. Level 3 subgoal for proof of =>: xc = yc [] Proved by contradiction. Level 2 subgoal for proof of =>: \A x:T \A y:T (fc ! (gc ! x) = fc ! (gc ! y) => x:T = y) [] Proved =>. Conjecture inj_inf3.1: is_inj(f:fun[U, V]) /\ is_inj(g:fun[T, U]) => is_inj(f \circ g) [] Proved =>. The system now contains 94 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.87: qed All conjectures have been proved. LP0.1.88: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.89: LP0.1.90: set name inj_inf4 The name-prefix is now `inj_inf4'. LP0.1.91: set order left The ordering-method is now `left-to-right'. LP0.1.92: prove is_inj (f:fun[T,U]) \/ is_inj (g:fun[T,V]) => is_inj (\) Attempting to prove conjecture inj_inf4.1: is_inj(f:fun[T, U]) \/ is_inj(g:fun[T, V]) => is_inj(\) Suspending proof of conjecture inj_inf4.1 LP0.1.93: resume by => Creating subgoals for proof of => New constants: fc, gc Hypothesis: inj_inf4ImpliesHyp.1: \A x:T \A y:T (fc ! x = fc ! y => x:T = y) \/ \A x:T \A y:T (gc ! x = gc ! y => x:T = y) Subgoal: \A x:T \A y:T (fc ! y = fc ! x /\ gc ! y = gc ! x => x:T = y) Attempting to prove level 2 subgoal for proof of => Added hypothesis inj_inf4ImpliesHyp.1 to the system. The system now contains 95 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 2 subgoal for proof of => LP0.1.94: resume by => Creating subgoals for proof of => New constants: xc, yc Hypothesis: inj_inf4ImpliesHyp.2: fc ! yc = fc ! xc /\ gc ! yc = gc ! xc Subgoal: xc = yc Attempting to prove level 3 subgoal for proof of => Added hypothesis inj_inf4ImpliesHyp.2 to the system. Deduction rule lp_and_is_true has been applied to formula inj_inf4ImpliesHyp.2 to yield the following formulas, which imply inj_inf4ImpliesHyp.2. inj_inf4ImpliesHyp.2.1: fc ! yc = fc ! xc inj_inf4ImpliesHyp.2.2: gc ! yc = gc ! xc The system now contains 97 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 3 subgoal for proof of => LP0.1.95: resume by contradiction Creating subgoals for proof by contradiction Hypothesis: inj_inf4ContraHyp.1: ~(xc = yc) Only subgoal: false Attempting to prove level 4 subgoal for proof by contradiction Added hypothesis inj_inf4ContraHyp.1 to the system. The system now contains 98 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 4 subgoal for proof by contradiction LP0.1.96: resume by cases is_inj (fc:fun[T,U]) Creating subgoals for proof by cases Case hypotheses: inj_inf4CaseHyp.1.1: is_inj(fc) inj_inf4CaseHyp.1.2: ~is_inj(fc) Same subgoal for all cases: false Attempting to prove level 5 subgoal for case 1 (out of 2) Added hypothesis inj_inf4CaseHyp.1.1 to the system. Deleted formula inj_inf4ImpliesHyp.1, which reduced to `true'. Suspending proof of level 5 subgoal for case 1 (out of 2) LP0.1.97: LP0.1.98: % Case 1 LP0.1.99: crit-pairs *Contra* with *Case* The following equations are critical pairs between rewrite rules inj_inf4ContraHyp.1 and inj_inf4CaseHyp.1.1. inj_inf4.2: false inj_inf4.3: false The system now contains 2 formulas and 98 rewrite rules. The rewriting system is NOT guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Formula inj_inf4.2, false, is inconsistent. Level 5 subgoal for case 1 (out of 2) [] Proved by impossible case. Attempting to prove level 5 subgoal for case 2 (out of 2) Added hypothesis inj_inf4CaseHyp.1.2 to the system. The system now contains 99 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.100: LP0.1.101: % Case 2 LP0.1.102: crit-pairs *Implies* with *Contra* The following equations are critical pairs between rewrite rules inj_inf4ImpliesHyp.1 and inj_inf4ContraHyp.1. inj_inf4.2: false inj_inf4.3: false The system now contains 2 formulas and 99 rewrite rules. The rewriting system is NOT guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Formula inj_inf4.2, false, is inconsistent. Level 5 subgoal for case 2 (out of 2): false [] Proved by impossible case. Level 4 subgoal for proof by contradiction: false [] Proved by cases is_inj(fc). Level 3 subgoal for proof of =>: xc = yc [] Proved by contradiction. Level 2 subgoal for proof of =>: \A x:T \A y:T (fc ! y = fc ! x /\ gc ! y = gc ! x => x:T = y) [] Proved =>. Conjecture inj_inf4.1: is_inj(f:fun[T, U]) \/ is_inj(g:fun[T, V]) => is_inj(\) [] Proved =>. The system now contains 95 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.103: LP0.1.104: qed All conjectures have been proved. LP0.1.105: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.106: LP0.1.107: set name inj_inf5 The name-prefix is now `inj_inf5'. LP0.1.108: prove is_inj (f:fun[T,U]) => is_inj (iterate (K (true), f)) Attempting to prove conjecture inj_inf5.1: is_inj(f:fun[T, U]) => is_inj(iterate(K(true), f)) Suspending proof of conjecture inj_inf5.1 LP0.1.109: LP0.1.110: resume by => Creating subgoals for proof of => New constant: fc Hypothesis: inj_inf5ImpliesHyp.1: \A x:T \A y:T (fc ! x = fc ! y => x:T = y) Subgoal: \A x:bag[T] \A y:bag[T] (iterate(K(true), fc) ! x = iterate(K(true), fc) ! y => x:bag[T] = y) Attempting to prove level 2 subgoal for proof of => Added hypothesis inj_inf5ImpliesHyp.1 to the system. The system now contains 96 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 2 subgoal for proof of => LP0.1.111: resume by induction on x:bag[T] Creating subgoals for proof by structural induction on `x:bag[T]' Basis subgoal: Subgoal 1: iterate(K(true), fc) ! {} = iterate(K(true), fc) ! y => {} = y Induction constant: xc Induction hypothesis: inj_inf5InductHyp.1: iterate(K(true), fc) ! xc = iterate(K(true), fc) ! y => xc = y Induction subgoal: Subgoal 2: iterate(K(true), fc) ! insert(t, xc) = iterate(K(true), fc) ! y => insert(t, xc) = y Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on x Suspending proof of level 3 subgoal 1 (basis step) for proof by induction on x LP0.1.112: LP0.1.113: % Base Case: LP0.1.114: resume by => Creating subgoals for proof of => New constant: yc Hypothesis: inj_inf5ImpliesHyp.2: {} = iterate(K(true), fc) ! yc Subgoal: {} = yc Attempting to prove level 4 subgoal for proof of => Added hypothesis inj_inf5ImpliesHyp.2 to the system. The system now contains 97 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 4 subgoal for proof of => LP0.1.115: resume by contra Creating subgoals for proof by contradiction Hypothesis: inj_inf5ContraHyp.1: ~({} = yc) Only subgoal: false Attempting to prove level 5 subgoal for proof by contradiction Added hypothesis inj_inf5ContraHyp.1 to the system. The system now contains 98 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 5 subgoal for proof by contradiction LP0.1.116: crit-pairs *Contra* with Bag The following equations are critical pairs between rewrite rules inj_inf5ContraHyp.1 and Bag.9. inj_inf5.2: \E x:T \E B:bag[T] (yc = insert(x, B)) The system now contains 1 formula and 98 rewrite rules. The rewriting system is NOT guaranteed to terminate. The system now contains 99 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.117: declare operator xc: -> T LP0.1.118: declare operator Bc: -> bag[T] LP0.1.119: fix x as xc in inj_inf5 A prenex-existential quantifier in formula inj_inf5.2 has been eliminated to produce formula inj_inf5.3, \E B:bag[T] (yc = insert(xc, B)) The system now contains 100 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.120: fix B as Bc in inj_inf5 / cont-oper (xc) A prenex-existential quantifier in formula inj_inf5.3 has been eliminated to produce formula inj_inf5.4, yc = insert(xc, Bc) Deleted formula inj_inf5ContraHyp.1, which reduced to `true'. Deleted formula inj_inf5.3, which reduced to `true'. Formula inj_inf5ImpliesHyp.2, false, is inconsistent. Level 5 subgoal for proof by contradiction: false [] Proved by detecting an inconsistency. Level 4 subgoal for proof of =>: {} = yc [] Proved by contradiction. Level 3 subgoal 1 (basis step) for proof by induction on x: iterate(K(true), fc) ! {} = iterate(K(true), fc) ! y => {} = y [] Proved =>. Attempting to prove level 3 subgoal 2 (induction step) for proof by induction on x: iterate(K(true), fc) ! insert(t, xc) = iterate(K(true), fc) ! y => insert(t, xc) = y Added hypothesis inj_inf5InductHyp.1 to the system. The system now contains 97 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.121: LP0.1.122: % Inductive Case: LP0.1.123: LP0.1.124: resume by => Creating subgoals for proof of => New constants: yc, tc Hypothesis: inj_inf5ImpliesHyp.2: insert(fc ! tc, iterate(K(true), fc) ! xc) = iterate(K(true), fc) ! yc Subgoal: insert(tc, xc) = yc Attempting to prove level 4 subgoal for proof of => Added hypothesis inj_inf5ImpliesHyp.2 to the system. The system now contains 98 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 4 subgoal for proof of => LP0.1.125: resume by cases tc \in yc Creating subgoals for proof by cases Case hypotheses: inj_inf5CaseHyp.1.1: tc \in yc inj_inf5CaseHyp.1.2: ~(tc \in yc) Same subgoal for all cases: insert(tc, xc) = yc Attempting to prove level 5 subgoal for case 1 (out of 2) Added hypothesis inj_inf5CaseHyp.1.1 to the system. The system now contains 99 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 5 subgoal for case 1 (out of 2) LP0.1.126: LP0.1.127: % Case 1 LP0.1.128: LP0.1.129: set immunity on The immunity is now `on'. LP0.1.130: prove \E B:bag[T] (yc = insert (tc, B)) Attempting to prove level 6 lemma inj_inf5.2: \E B:bag[T] (yc = insert(tc, B)) Level 6 lemma inj_inf5.2 [] Proved by normalization. Attempting to prove level 5 subgoal for case 1 (out of 2) The system now contains 100 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 5 subgoal for case 1 (out of 2) LP0.1.131: set immunity off The immunity is now `off'. LP0.1.132: LP0.1.133: declare operator zc: -> bag [T] LP0.1.134: fix B:bag[T] as zc in inj_inf5 A prenex-existential quantifier in formula inj_inf5.2 has been eliminated to produce formula inj_inf5.3, yc = insert(tc, zc) The system now contains 101 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.135: LP0.1.136: prove insert (fc ! tc, iterate (K (true), fc) ! xc) = iterate (K (true), fc) ! (insert (tc, zc)) .. Attempting to prove level 6 lemma inj_inf5.4: insert(fc ! tc, iterate(K(true), fc) ! xc) = iterate(K(true), fc) ! insert(tc, zc) Suspending proof of level 6 lemma inj_inf5.4 LP0.1.137: resume by contradiction Creating subgoals for proof by contradiction Hypothesis: inj_inf5ContraHyp.1: ~(iterate(K(true), fc) ! yc = insert(fc ! tc, iterate(K(true), fc) ! zc)) Only subgoal: false Attempting to prove level 7 subgoal for proof by contradiction Added hypothesis inj_inf5ContraHyp.1 to the system. The system now contains 102 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 7 subgoal for proof by contradiction LP0.1.138: crit-pairs inj_inf5 with Iterate The following equations are critical pairs between rewrite rules inj_inf5.3 and Iterate.3. inj_inf5.5: ~(p ? tc) => iterate(p, f) ! yc = iterate(p, f) ! zc The system now contains 1 formula and 102 rewrite rules. The rewriting system is NOT guaranteed to terminate. The following equations are critical pairs between rewrite rules inj_inf5.3 and Iterate.2. inj_inf5.6: p ? tc => iterate(p, f) ! yc = insert(f ! tc, iterate(p, f) ! zc) The system now contains 1 formula and 103 rewrite rules. The rewriting system is NOT guaranteed to terminate. The system now contains 104 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.139: instan p by K (true), f by fc in inj_inf5 Formula inj_inf5.6 has been instantiated to formula inj_inf5.6.1, false Formula inj_inf5.6.1, false, is inconsistent. Level 7 subgoal for proof by contradiction [] Proved by detecting an inconsistency. Level 6 lemma inj_inf5.4: insert(fc ! tc, iterate(K(true), fc) ! xc) = iterate(K(true), fc) ! insert(tc, zc) [] Proved by contradiction. Attempting to prove level 5 subgoal for case 1 (out of 2): insert(tc, xc) = yc The system now contains 102 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.140: LP0.1.141: prove iterate (K (true), fc) ! xc = iterate (K (true), fc) ! zc Attempting to prove level 6 lemma inj_inf5.5: iterate(K(true), fc) ! xc = iterate(K(true), fc) ! zc Suspending proof of level 6 lemma inj_inf5.5 LP0.1.142: set immunity on The immunity is now `on'. LP0.1.143: prove insert (fc ! tc, iterate (K (true), fc) ! xc) = insert (fc ! tc, iterate (K (true), fc) ! zc) .. Attempting to prove level 7 lemma inj_inf5.6: insert(fc ! tc, iterate(K(true), fc) ! xc) = insert(fc ! tc, iterate(K(true), fc) ! zc) Level 7 lemma inj_inf5.6 [] Proved by normalization. Attempting to prove level 6 lemma inj_inf5.5 Deleted formula inj_inf5ImpliesHyp.2, which reduced to `true'. Suspending proof of level 6 lemma inj_inf5.5 LP0.1.144: set immunity off The immunity is now `off'. LP0.1.145: crit-pairs inj_inf5 / cont-op (zc) with BagBasics / cont-oper (-:bag[U],U->bag[U]) .. The following equations are critical pairs between rewrite rules inj_inf5.4 and BagBasics.21. inj_inf5.7: (iterate(K(true), fc) ! yc) - (fc ! tc) = iterate(K(true), fc) ! zc The system now contains 1 formula and 102 rewrite rules. The rewriting system is NOT guaranteed to terminate. The following equations are critical pairs between rewrite rules inj_inf5.4 and BagBasics.14. inj_inf5.8: ~(fc ! tc = y) => (iterate(K(true), fc) ! yc) - y = insert(fc ! tc, (iterate(K(true), fc) ! zc) - y) The system now contains 1 formula and 103 rewrite rules. The rewriting system is NOT guaranteed to terminate. The following equations are critical pairs between rewrite rules inj_inf5.6 and BagBasics.21. inj_inf5.9: iterate(K(true), fc) ! zc = iterate(K(true), fc) ! xc The system now contains 1 formula and 104 rewrite rules. The rewriting system is NOT guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Level 6 lemma inj_inf5.5: iterate(K(true), fc) ! xc = iterate(K(true), fc) ! zc [] Proved by normalization. Attempting to prove level 5 subgoal for case 1 (out of 2): insert(tc, xc) = yc Deleted formula inj_inf5ImpliesHyp.2, which reduced to `true'. The system now contains 102 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.146: LP0.1.147: prove xc = zc Attempting to prove level 6 lemma inj_inf5.6: xc = zc Suspending proof of level 6 lemma inj_inf5.6 LP0.1.148: instan y by zc in *Induct* Formula inj_inf5InductHyp.1 has been instantiated to formula inj_inf5InductHyp.1.1, xc = zc Level 6 lemma inj_inf5.6 [] Proved by normalization. Attempting to prove level 5 subgoal for case 1 (out of 2) Level 5 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 5 subgoal for case 2 (out of 2): insert(tc, xc) = yc Added hypothesis inj_inf5CaseHyp.1.2 to the system. The system now contains 99 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.149: LP0.1.150: % Case 2: LP0.1.151: LP0.1.152: prove (fc ! tc) \in (iterate(K(true), fc) ! yc) Attempting to prove level 6 lemma inj_inf5.2: (fc ! tc) \in (iterate(K(true), fc) ! yc) Suspending proof of level 6 lemma inj_inf5.2 LP0.1.153: crit-pairs *BagBasics* / cont-oper (\in:U,bag[U]->Bool) with *Implies* .. The following equations are critical pairs between rewrite rules BagBasics.11 and inj_inf5ImpliesHyp.2. inj_inf5.3: \E x:T (x = fc ! x /\ x \in yc) = (x = fc ! tc \/ \E x:T (x = fc ! x /\ x \in xc)) The system now contains 1 formula and 99 rewrite rules. The rewriting system is NOT guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Level 6 lemma inj_inf5.2 [] Proved by normalization. Attempting to prove level 5 subgoal for case 2 (out of 2) The system now contains 100 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.154: LP0.1.155: declare operator zc: -> T, Bc: -> bag [T] LP0.1.156: fix x as zc in inj_inf5 A prenex-existential quantifier in formula inj_inf5.2 has been eliminated to produce formula inj_inf5.3, fc ! tc = fc ! zc /\ zc \in yc Deduction rule lp_and_is_true has been applied to formula inj_inf5.3 to yield the following formulas, which imply inj_inf5.3. inj_inf5.3.1: fc ! tc = fc ! zc inj_inf5.3.2: zc \in yc The system now contains 102 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.157: crit-pairs inj_inf5 / cont-oper (zc) with *Implies* The following equations are critical pairs between rewrite rules inj_inf5.3.1 and inj_inf5ImpliesHyp.1. inj_inf5.4: fc ! zc = fc ! y => tc = y inj_inf5.5: fc ! x = fc ! zc => x = tc The system now contains 2 formulas and 102 rewrite rules. The rewriting system is NOT guaranteed to terminate. Deleted formula inj_inf5.5, which reduced to `true'. The system now contains 103 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.158: prove tc = zc by contradiction Attempting to prove level 6 lemma inj_inf5.6: tc = zc Creating subgoals for proof by contradiction Hypothesis: inj_inf5ContraHyp.1: ~(tc = zc) Only subgoal: false Attempting to prove level 7 subgoal for proof by contradiction Added hypothesis inj_inf5ContraHyp.1 to the system. The system now contains 104 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 7 subgoal for proof by contradiction LP0.1.159: crit-pairs inj_inf5* with inj_inf5* The following equations are critical pairs between rewrite rules inj_inf5ContraHyp.1 and inj_inf5ImpliesHyp.1. inj_inf5.7: false inj_inf5.8: false The system now contains 2 formulas and 104 rewrite rules. The rewriting system is NOT guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Formula inj_inf5.7, false, is inconsistent. Level 7 subgoal for proof by contradiction [] Proved by detecting an inconsistency. Level 6 lemma inj_inf5.6 [] Proved by contradiction. Attempting to prove level 5 subgoal for case 2 (out of 2): insert(tc, xc) = yc Deleted formula inj_inf5.3.1, which reduced to `true'. Deleted formula inj_inf5.4, which reduced to `true'. Formula inj_inf5CaseHyp.1.2, false, is inconsistent. Level 5 subgoal for case 2 (out of 2) [] Proved by impossible case. Level 4 subgoal for proof of =>: insert(tc, xc) = yc [] Proved by cases tc \in yc. Level 3 subgoal 2 (induction step) for proof by induction on x: iterate(K(true), fc) ! insert(t, xc) = iterate(K(true), fc) ! y => insert(t, xc) = y [] Proved =>. Level 2 subgoal for proof of =>: \A x:bag[T] \A y:bag[T] (iterate(K(true), fc) ! x = iterate(K(true), fc) ! y => x:bag[T] = y) [] Proved by structural induction on `x:bag[T]'. Conjecture inj_inf5.1: is_inj(f:fun[T, U]) => is_inj(iterate(K(true), f)) [] Proved =>. The system now contains 96 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.160: qed All conjectures have been proved. LP0.1.161: LP0.1.162: LP0.1.163: % Section 2: Set Inference Rules LP0.1.164: % LP0.1.165: % Proof Scripts for the Inference Rules of Figure 4b LP0.1.166: % LP0.1.167: % is_set (set ! _) LP0.1.168: % is_type (A, set (_)) => is_set (A) LP0.1.169: % is_set (A) /\ is_set (B) => is_set (A \times B) LP0.1.170: % is_set (A) \/ is_set (B) => is_set (A \I B) LP0.1.171: % is_set (A) => is_set (A - B) LP0.1.172: % LP0.1.173: % Note that the 2nd rule relies on a correct identification by DB managers LP0.1.174: % as to what named collections are sets. The formal specification of is_type LP0.1.175: % is therefore derived solely from the schema and hence the proof of this rule LP0.1.176: % is omitted. LP0.1.177: % LP0.1.178: LP0.1.179: LP0.1.180: clear LP0.1.181: set order manual The ordering-method is now `manual'. LP0.1.182: exec-silently Set_Inf_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/Set_Inf_Aux_Axioms.lp'. LP0.1.183: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.184: order formulas The formulas cannot be ordered using the current ordering. LP0.1.185: make immune formulas LP0.1.186: LP0.1.187: declare variables A, B: bag [T], B: bag [U] .. LP0.1.188: LP0.1.189: LP0.1.190: % L1: Rules for Inference of "Setness" LP0.1.191: % ------------------------------------ LP0.1.192: LP0.1.193: set name set_inf1 The name-prefix is now `set_inf1'. LP0.1.194: prove is_set (set ! A:bag[U]) Attempting to prove conjecture set_inf1.1: is_set((set ! A):bag[U]) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture set_inf1.1 LP0.1.195: LP0.1.196: resume by induction on A:bag[U] Creating subgoals for proof by structural induction on `A:bag[U]' Basis subgoal: Subgoal 1: ~(x:U \in ((set ! {}) - x:U)) Induction constant: Ac Induction hypothesis: set_inf1InductHyp.1: ~(x \in ((set ! Ac) - x:U)) Induction subgoal: Subgoal 2: ~(x \in ((set ! insert(u, Ac)) - x:U)) 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 set_inf1InductHyp.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.197: LP0.1.198: % Base Case: Trivial LP0.1.199: % Inductive Case: LP0.1.200: LP0.1.201: resume by contradiction Creating subgoals for proof by contradiction New constants: xc, uc Hypothesis: set_inf1ContraHyp.1: ~(~(xc \in ((if uc \in Ac then set ! Ac else insert(uc, set ! Ac)) - xc))) Only subgoal: false Attempting to prove level 3 subgoal for proof by contradiction Added hypothesis set_inf1ContraHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for proof by contradiction LP0.1.202: resume by cases uc \in Ac Creating subgoals for proof by cases Case hypotheses: set_inf1CaseHyp.1.1: uc \in Ac set_inf1CaseHyp.1.2: ~(uc \in Ac) Same subgoal for all cases: false Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis set_inf1CaseHyp.1.1 to the system. Formula set_inf1ContraHyp.1, false, is inconsistent. Level 4 subgoal for case 1 (out of 2) [] Proved by impossible case. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis set_inf1CaseHyp.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.203: LP0.1.204: % Case 1: Trivial LP0.1.205: % Case 2: LP0.1.206: crit-pairs *Contra* with BagBasics The following equations are critical pairs between rewrite rules set_inf1ContraHyp.1 and BagBasics.26. set_inf1.2: xc = uc \/ xc \in Ac The system now contains 4 formulas and 120 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules set_inf1ContraHyp.1 and BagBasics.14. set_inf1.3: xc = uc The system now contains 4 formulas and 121 rewrite rules. The rewriting system is guaranteed to terminate. Deleted formula set_inf1.2, which reduced to `true'. Critical pair computation abandoned because a theorem has been proved. Formula set_inf1ContraHyp.1, false, is inconsistent. Level 4 subgoal for case 2 (out of 2): false [] Proved by impossible case. Level 3 subgoal for proof by contradiction: false [] Proved by cases uc \in Ac. Level 2 subgoal 2 (induction step) for proof by induction on A: ~(x \in ((set ! insert(u, Ac)) - x:U)) [] Proved by contradiction. Conjecture set_inf1.1: is_set((set ! A):bag[U]) [] Proved by structural induction on `A:bag[U]'. The formulas cannot be ordered using the current ordering. LP0.1.207: LP0.1.208: qed All conjectures have been proved. LP0.1.209: LP0.1.210: set name set_inf3 The name-prefix is now `set_inf3'. LP0.1.211: LP0.1.212: prove is_set (A:bag[T]) /\ is_set (B:bag[U]) => is_set (A \times B) Attempting to prove conjecture set_inf3.1: is_set(A:bag[T]) /\ is_set(B:bag[U]) => is_set(A \times B) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture set_inf3.1 LP0.1.213: resume by => Creating subgoals for proof of => New constants: Ac, Bc Hypothesis: set_inf3ImpliesHyp.1: \A x:T ~(x \in (Ac - x:T)) /\ \A x:U ~(x \in (Bc - x:U)) Subgoal: \A x:pair[T, U] ~(x \in ((Ac \times Bc) - x:pair[T, U])) Attempting to prove level 2 subgoal for proof of => Added hypothesis set_inf3ImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula set_inf3ImpliesHyp.1 to yield the following formulas, which imply set_inf3ImpliesHyp.1. set_inf3ImpliesHyp.1.1: \A x:T ~(x \in (Ac - x:T)) set_inf3ImpliesHyp.1.2: \A x:U ~(x \in (Bc - x:U)) The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal for proof of => LP0.1.214: resume by contradiction Creating subgoals for proof by contradiction New constant: xc Hypothesis: set_inf3ContraHyp.1: ~(~(xc \in ((Ac \times Bc) - xc))) Only subgoal: false Attempting to prove level 3 subgoal for proof by contradiction Added hypothesis set_inf3ContraHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for proof by contradiction LP0.1.215: LP0.1.216: set immunity on The immunity is now `on'. LP0.1.217: instan pr:pair[T,U] by xc in Pairs / cont-oper (=:pair[T,U],pair[T,U]->Bool) .. Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T \E y:U (xc = [x, y]) The formulas cannot be ordered using the current ordering. LP0.1.218: set immunity off The immunity is now `off'. LP0.1.219: declare operator tc: -> T, uc: -> U LP0.1.220: fix x:T as tc in Pairs / cont-oper (xc) A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula set_inf3.2, \E y:U (xc = [tc, y]) The formulas cannot be ordered using the current ordering. LP0.1.221: fix y:U as uc in set_inf3 / cont-oper (tc) A prenex-existential quantifier in formula set_inf3.2 has been eliminated to produce formula set_inf3.3, xc = [tc, uc] Deleted formula set_inf3.2, which reduced to `true'. The formulas cannot be ordered using the current ordering. LP0.1.222: LP0.1.223: prove [tc, uc] \in (Ac \times Bc) Attempting to prove level 4 lemma set_inf3.4: [tc, uc] \in (Ac \times Bc) The formulas cannot be ordered using the current ordering. Suspending proof of level 4 lemma set_inf3.4 LP0.1.224: crit-pairs *Contra* with BagBasics The following equations are critical pairs between rewrite rules set_inf3ContraHyp.1 and BagBasics.30. set_inf3.5: tc \in Ac /\ uc \in Bc The system now contains 4 formulas and 123 rewrite rules. The rewriting system is guaranteed to terminate. Deduction rule lp_and_is_true has been applied to formula set_inf3.5 to yield the following formulas, which imply set_inf3.5. set_inf3.5.1: tc \in Ac set_inf3.5.2: uc \in Bc Critical pair computation abandoned because a theorem has been proved. Level 4 lemma set_inf3.4 [] Proved by normalization. Attempting to prove level 3 subgoal for proof by contradiction: false Deduction rule lp_and_is_true has been applied to formula set_inf3.4 to yield the following formulas, which imply set_inf3.4. set_inf3.4.1: tc \in Ac set_inf3.4.2: uc \in Bc The formulas cannot be ordered using the current ordering. LP0.1.225: LP0.1.226: 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.227: set immunity on The immunity is now `on'. LP0.1.228: prove (Ac \times Bc) = (insert ([tc, uc], ((Ac - tc) \times (Bc - uc)) \U (insert(tc, {}) \times (Bc - uc)) \U ((Ac - tc) \times insert(uc, {})))) .. Attempting to prove level 4 lemma set_inf3.5: Ac \times Bc = insert([tc, uc], ((Ac - tc) \times (Bc - uc)) \U (insert(tc, {}) \times (Bc - uc)) \U ((Ac - tc) \times insert(uc, {}))) Level 4 lemma set_inf3.5 [] Proved by normalization. Attempting to prove level 3 subgoal for proof by contradiction Formula set_inf3ContraHyp.1, false, is inconsistent. Level 3 subgoal for proof by contradiction: false [] Proved by detecting an inconsistency. Level 2 subgoal for proof of =>: \A x:pair[T, U] ~(x \in ((Ac \times Bc) - x:pair[T, U])) [] Proved by contradiction. Conjecture set_inf3.1: is_set(A:bag[T]) /\ is_set(B:bag[U]) => is_set(A \times B) [] Proved =>. The formulas cannot be ordered using the current ordering. LP0.1.229: set immunity off The immunity is now `off'. LP0.1.230: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.231: qed All conjectures have been proved. LP0.1.232: LP0.1.233: set name set_inf4 The name-prefix is now `set_inf4'. LP0.1.234: prove is_set (A:bag[T]) \/ is_set (B:bag[T]) => is_set (A:bag[T] \I B) Attempting to prove conjecture set_inf4.1: is_set(A:bag[T]) \/ is_set(B:bag[T]) => is_set((A \I B):bag[T]) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture set_inf4.1 LP0.1.235: resume by => Creating subgoals for proof of => New constants: Ac, Bc Hypothesis: set_inf4ImpliesHyp.1: \A x:T ~(x \in (Ac - x:T)) \/ \A x:T ~(x \in (Bc - x:T)) Subgoal: \A x:T ~(x \in ((Ac \I Bc) - x:T)) Attempting to prove level 2 subgoal for proof of => Added hypothesis set_inf4ImpliesHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal for proof of => LP0.1.236: resume by contradiction Creating subgoals for proof by contradiction New constant: xc Hypothesis: set_inf4ContraHyp.1: ~(~(xc \in ((Ac \I Bc) - xc))) Only subgoal: false Attempting to prove level 3 subgoal for proof by contradiction Added hypothesis set_inf4ContraHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for proof by contradiction LP0.1.237: crit-pairs *Contra* with BagBasics The following equations are critical pairs between rewrite rules set_inf4ContraHyp.1 and BagBasics.22. set_inf4.2: xc \in Ac /\ xc \in Bc The system now contains 4 formulas and 121 rewrite rules. The rewriting system is guaranteed to terminate. Deduction rule lp_and_is_true has been applied to formula set_inf4.2 to yield the following formulas, which imply set_inf4.2. set_inf4.2.1: xc \in Ac set_inf4.2.2: xc \in Bc The system now contains 3 formulas and 123 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.238: LP0.1.239: 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.240: set immunity on The immunity is now `on'. LP0.1.241: prove (Ac \I Bc) = (insert (xc, Ac - xc) \I insert (xc, Bc - xc)) Attempting to prove level 4 lemma set_inf4.3: Ac \I Bc = insert(xc, Ac - xc) \I insert(xc, Bc - xc) Level 4 lemma set_inf4.3 [] Proved by normalization. Attempting to prove level 3 subgoal for proof by contradiction: false Deduction rule lp_and_is_true has been applied to formula set_inf4ContraHyp.1 to yield the following formulas, which imply set_inf4ContraHyp.1. set_inf4ContraHyp.1.1: xc \in (Ac - xc) set_inf4ContraHyp.1.2: xc \in (Bc - xc) The system now contains 128 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 3 subgoal for proof by contradiction LP0.1.242: set immunity off The immunity is now `off'. LP0.1.243: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.244: instan x by xc in *Implies* Formula set_inf4ImpliesHyp.1 has been instantiated to formula set_inf4ImpliesHyp.1.1, false Formula set_inf4ImpliesHyp.1.1, false, is inconsistent. Level 3 subgoal for proof by contradiction [] Proved by detecting an inconsistency. Level 2 subgoal for proof of =>: \A x:T ~(x \in ((Ac \I Bc) - x:T)) [] Proved by contradiction. Conjecture set_inf4.1: is_set(A:bag[T]) \/ is_set(B:bag[T]) => is_set((A \I B):bag[T]) [] Proved =>. The formulas cannot be ordered using the current ordering. LP0.1.245: qed All conjectures have been proved. LP0.1.246: LP0.1.247: set name set_inf5 The name-prefix is now `set_inf5'. LP0.1.248: prove is_set (A:bag[T]) => is_set (A:bag[T] - B) Attempting to prove conjecture set_inf5.1: is_set(A:bag[T]) => is_set((A - B):bag[T]) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture set_inf5.1 LP0.1.249: resume by => Creating subgoals for proof of => New constant: Ac Hypothesis: set_inf5ImpliesHyp.1: \A x:T ~(x \in (Ac - x:T)) Subgoal: \A x:T ~(x \in (Ac - B - x:T)) Attempting to prove level 2 subgoal for proof of => Added hypothesis set_inf5ImpliesHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal for proof of => LP0.1.250: resume by contradiction Creating subgoals for proof by contradiction New constants: xc, Bc Hypothesis: set_inf5ContraHyp.1: ~(~(xc \in (Ac - Bc - xc))) Only subgoal: false Attempting to prove level 3 subgoal for proof by contradiction Added hypothesis set_inf5ContraHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for proof by contradiction LP0.1.251: crit-pairs *Contra* with BagBasics The following equations are critical pairs between rewrite rules set_inf5ContraHyp.1 and BagBasics.22. set_inf5.2: xc \in Ac /\ ~(xc \in Bc) The system now contains 4 formulas and 122 rewrite rules. The rewriting system is guaranteed to terminate. Deduction rule lp_and_is_true has been applied to formula set_inf5.2 to yield the following formulas, which imply set_inf5.2. set_inf5.2.1: xc \in Ac set_inf5.2.2: ~(xc \in Bc) The system now contains 3 formulas and 124 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.252: LP0.1.253: 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.254: set immunity on The immunity is now `on'. LP0.1.255: prove (Ac - Bc) = (insert (xc, Ac - xc) - Bc) Attempting to prove level 4 lemma set_inf5.3: Ac - Bc = insert(xc, Ac - xc) - Bc The system now contains 127 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 4 lemma set_inf5.3 LP0.1.256: prove (Ac = insert (xc, Ac - xc)) Attempting to prove level 5 lemma set_inf5.4: Ac = insert(xc, Ac - xc) Level 5 lemma set_inf5.4 [] Proved by normalization. Attempting to prove level 4 lemma set_inf5.3 Level 4 lemma set_inf5.3 [] Proved by normalization. Attempting to prove level 3 subgoal for proof by contradiction: false Formula set_inf5ContraHyp.1, false, is inconsistent. Level 3 subgoal for proof by contradiction [] Proved by detecting an inconsistency. Level 2 subgoal for proof of =>: \A x:T ~(x \in (Ac - B - x:T)) [] Proved by contradiction. Conjecture set_inf5.1: is_set(A:bag[T]) => is_set((A - B):bag[T]) [] Proved =>. The formulas cannot be ordered using the current ordering. LP0.1.257: set immunity off The immunity is now `off'. LP0.1.258: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.259: qed All conjectures have been proved. LP0.1.260: LP0.1.261: LP0.1.262: % Section 3: Conditional Rewrite Rules Involving Injectivity and "Setness" LP0.1.263: % LP0.1.264: % Proof Scripts for the Conditional Rewrite Rules of Section 3.2 LP0.1.265: % LP0.1.266: % is_inj (f) /\ is_set (A) :: set ! (iterate (p, f) ! A) --> iterate (p, f) ! A LP0.1.267: % is_inj (f) :: LP0.1.268: % iterate (p, f) ! (A \I B) --> (iterate (p, f) ! A) \I (iterate (p, f) ! B) LP0.1.269: % LP0.1.270: LP0.1.271: LP0.1.272: clear LP0.1.273: set order manual The ordering-method is now `manual'. LP0.1.274: exec-silently Inj_RR_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/Inj_RR_Aux_Axioms.lp'. LP0.1.275: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.276: order formulas The formulas cannot be ordered using the current ordering. LP0.1.277: make immune formulas LP0.1.278: LP0.1.279: declare variables f: fun [T, U], A, B: bag [T], p: pred [T] .. LP0.1.280: LP0.1.281: LP0.1.282: % L1: Lemmas for the Rewrite Rules Conditioned on Injectivity and "Setness" LP0.1.283: % ------------------------------------------------------------------------- LP0.1.284: LP0.1.285: set name inj_RRLemma The name-prefix is now `inj_RRLemma'. LP0.1.286: % ---------------------------------------------------------- LP0.1.287: prove insert (x:T, A) \I B = (if (x:T \in B) then insert (x:T, (A \I (B - x:T))) else (A \I B)) .. Attempting to prove conjecture inj_RRLemma.1: (insert(x, A) \I B):bag[T] = (if x:T \in B then insert(x, A \I (B - x:T)) else A \I B) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture inj_RRLemma.1 LP0.1.288: LP0.1.289: resume by cases x:T \in B Creating subgoals for proof by cases New constants: xc, Bc Case hypotheses: inj_RRLemmaCaseHyp.1.1: xc \in Bc inj_RRLemmaCaseHyp.1.2: ~(xc \in Bc) Same subgoal for all cases: insert(xc, A) \I Bc = (if xc \in Bc then insert(xc, A \I (Bc - xc)) else A \I Bc) Attempting to prove level 2 subgoal for case 1 (out of 2) Added hypothesis inj_RRLemmaCaseHyp.1.1 to the system. Level 2 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 2 subgoal for case 2 (out of 2) Added hypothesis inj_RRLemmaCaseHyp.1.2 to the system. Level 2 subgoal for case 2 (out of 2) [] Proved by normalization. Conjecture inj_RRLemma.1 [] Proved by cases x:T \in B. The formulas cannot be ordered using the current ordering. LP0.1.290: qed All conjectures have been proved. LP0.1.291: % ---------------------------------------------------------- LP0.1.292: LP0.1.293: % ---------------------------------------------------------- LP0.1.294: prove insert (x:U, A) \I B = (if (x:U \in B) then insert (x:U, (A \I (B - x:U))) else (A \I B)) .. Attempting to prove conjecture inj_RRLemma.2: (insert(x, A) \I B):bag[U] = (if x:U \in B then insert(x, A \I (B - x:U)) else A \I B) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture inj_RRLemma.2 LP0.1.295: resume by cases x:U \in B Creating subgoals for proof by cases New constants: xc, Bc Case hypotheses: inj_RRLemmaCaseHyp.1.1: xc \in Bc inj_RRLemmaCaseHyp.1.2: ~(xc \in Bc) Same subgoal for all cases: insert(xc, A) \I Bc = (if xc \in Bc then insert(xc, A \I (Bc - xc)) else A \I Bc) Attempting to prove level 2 subgoal for case 1 (out of 2) Added hypothesis inj_RRLemmaCaseHyp.1.1 to the system. Level 2 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 2 subgoal for case 2 (out of 2) Added hypothesis inj_RRLemmaCaseHyp.1.2 to the system. Level 2 subgoal for case 2 (out of 2) [] Proved by normalization. Conjecture inj_RRLemma.2 [] Proved by cases x:U \in B. The formulas cannot be ordered using the current ordering. LP0.1.296: qed All conjectures have been proved. LP0.1.297: % ---------------------------------------------------------- LP0.1.298: LP0.1.299: LP0.1.300: % ---------------------------------------------------------- LP0.1.301: prove iterate (p, f:fun[T,U]) ! (A - x:T) = (if (x:T \in A /\ p ? x:T) then (iterate (p, f:fun[T,U]) ! A) - (f:fun[T,U] ! x) else (iterate (p, f:fun[T,U]) ! A)) .. Attempting to prove conjecture inj_RRLemma.3: (iterate(p, f) ! (A - x:T)):bag[U] = (if x:T \in A /\ p ? x then (iterate(p, f) ! A) - ((f ! x):U) else iterate(p, f) ! A) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture inj_RRLemma.3 LP0.1.302: LP0.1.303: resume by cases x:T \in A Creating subgoals for proof by cases New constants: xc, Ac Case hypotheses: inj_RRLemmaCaseHyp.1.1: xc \in Ac inj_RRLemmaCaseHyp.1.2: ~(xc \in Ac) Same subgoal for all cases: (iterate(p, f) ! (Ac - xc)):bag[U] = (if xc \in Ac /\ p ? xc then (iterate(p, f) ! Ac) - (f ! xc) else iterate(p, f) ! Ac) Attempting to prove level 2 subgoal for case 1 (out of 2) Added hypothesis inj_RRLemmaCaseHyp.1.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal for case 1 (out of 2) LP0.1.304: LP0.1.305: % Case 1 LP0.1.306: LP0.1.307: set immunity on The immunity is now `on'. LP0.1.308: prove \E B:bag [T] (Ac = insert (xc, B)) Attempting to prove level 3 lemma inj_RRLemma.4: \E B:bag[T] (Ac = insert(xc, B)) Level 3 lemma inj_RRLemma.4 [] Proved by normalization. Attempting to prove level 2 subgoal for case 1 (out of 2) The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal for case 1 (out of 2) LP0.1.309: set immunity off The immunity is now `off'. LP0.1.310: declare operator Bc: -> bag [T] LP0.1.311: fix B as Bc in inj_RRLemma A prenex-existential quantifier in formula inj_RRLemma.4 has been eliminated to produce formula inj_RRLemma.5, Ac = insert(xc, Bc) Deleted formula inj_RRLemmaCaseHyp.1.1, which reduced to `true'. The formulas cannot be ordered using the current ordering. LP0.1.312: LP0.1.313: resume by cases p ? xc Creating subgoals for proof by cases New constant: pc Case hypotheses: inj_RRLemmaCaseHyp.2.1: pc ? xc inj_RRLemmaCaseHyp.2.2: ~(pc ? xc) Same subgoal for all cases: (iterate(pc, f) ! Bc):bag[U] = (if pc ? xc then (iterate(pc, f) ! insert(xc, Bc)) - (f ! xc) else iterate(pc, f) ! insert(xc, Bc)) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis inj_RRLemmaCaseHyp.2.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 inj_RRLemmaCaseHyp.2.2 to the system. Level 3 subgoal for case 2 (out of 2) [] Proved by normalization. Level 2 subgoal for case 1 (out of 2): (iterate(p, f) ! (Ac - xc)):bag[U] = (if xc \in Ac /\ p ? xc then (iterate(p, f) ! Ac) - (f ! xc) else iterate(p, f) ! Ac) [] Proved by cases p ? xc. Attempting to prove level 2 subgoal for case 2 (out of 2): (iterate(p, f) ! (Ac - xc)):bag[U] = (if xc \in Ac /\ p ? xc then (iterate(p, f) ! Ac) - (f ! xc) else iterate(p, f) ! Ac) Added hypothesis inj_RRLemmaCaseHyp.1.2 to the system. Level 2 subgoal for case 2 (out of 2) [] Proved by normalization. Conjecture inj_RRLemma.3: (iterate(p, f) ! (A - x:T)):bag[U] = (if x:T \in A /\ p ? x then (iterate(p, f) ! A) - ((f ! x):U) else iterate(p, f) ! A) [] Proved by cases x:T \in A. The formulas cannot be ordered using the current ordering. LP0.1.314: LP0.1.315: % Case 2: Trivial LP0.1.316: LP0.1.317: qed All conjectures have been proved. LP0.1.318: % ---------------------------------------------------------- LP0.1.319: LP0.1.320: % ---------------------------------------------------------- LP0.1.321: set immunity on The immunity is now `on'. LP0.1.322: prove A:bag [T] \I B = B:bag[T] \I A Attempting to prove conjecture inj_RRLemma.4: (A \I B):bag[T] = B \I A The formulas cannot be ordered using the current ordering. Suspending proof of conjecture inj_RRLemma.4 LP0.1.323: resume by induction on A:bag[T] Creating subgoals for proof by structural induction on `A:bag[T]' Basis subgoal: Subgoal 1: ({} \I B):bag[T] = B \I {} Induction constant: Ac Induction hypothesis: inj_RRLemmaInductHyp.1: Ac \I B = B \I Ac Induction subgoal: Subgoal 2: insert(t, Ac) \I B = B \I 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 inj_RRLemmaInductHyp.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.324: LP0.1.325: % Base Case: Trivial LP0.1.326: % Inductive Case: LP0.1.327: resume by cases t \in B Creating subgoals for proof by cases New constants: tc, Bc Case hypotheses: inj_RRLemmaCaseHyp.1.1: tc \in Bc inj_RRLemmaCaseHyp.1.2: ~(tc \in Bc) Same subgoal for all cases: (if tc \in Bc then insert(tc, Ac \I (Bc - tc)) else Ac \I Bc) = Bc \I insert(tc, Ac) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis inj_RRLemmaCaseHyp.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.328: LP0.1.329: % Case 1 LP0.1.330: normalize conjecture 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 inj_RRLemmaCaseHyp.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) The formulas cannot be ordered using the current ordering. LP0.1.331: LP0.1.332: % Case 2 LP0.1.333: normalize conjecture Level 3 subgoal for case 2 (out of 2) [] Proved by normalization. Level 2 subgoal 2 (induction step) for proof by induction on A: insert(t, Ac) \I B = B \I insert(t, Ac) [] Proved by cases t \in B. Conjecture inj_RRLemma.4: (A \I B):bag[T] = B \I A [] Proved by structural induction on `A:bag[T]'. The formulas cannot be ordered using the current ordering. The formulas cannot be ordered using the current ordering. LP0.1.334: LP0.1.335: qed All conjectures have been proved. LP0.1.336: LP0.1.337: prove A:bag [U] \I B = B:bag[U] \I A Attempting to prove conjecture inj_RRLemma.5: (A \I B):bag[U] = B \I A The formulas cannot be ordered using the current ordering. Suspending proof of conjecture inj_RRLemma.5 LP0.1.338: resume by induction on A:bag[U] Creating subgoals for proof by structural induction on `A:bag[U]' Basis subgoal: Subgoal 1: ({} \I B):bag[U] = B \I {} Induction constant: Ac Induction hypothesis: inj_RRLemmaInductHyp.1: Ac \I B = B \I Ac Induction subgoal: Subgoal 2: insert(u, Ac) \I B = B \I insert(u, 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 inj_RRLemmaInductHyp.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.339: LP0.1.340: % Base Case: Trivial LP0.1.341: % Inductive Case: LP0.1.342: resume by cases u \in B Creating subgoals for proof by cases New constants: uc, Bc Case hypotheses: inj_RRLemmaCaseHyp.1.1: uc \in Bc inj_RRLemmaCaseHyp.1.2: ~(uc \in Bc) Same subgoal for all cases: (if uc \in Bc then insert(uc, Ac \I (Bc - uc)) else Ac \I Bc) = Bc \I insert(uc, Ac) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis inj_RRLemmaCaseHyp.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.343: LP0.1.344: % Case 1 LP0.1.345: normalize conjecture 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 inj_RRLemmaCaseHyp.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) The formulas cannot be ordered using the current ordering. LP0.1.346: LP0.1.347: % Case 2 LP0.1.348: normalize conjecture Level 3 subgoal for case 2 (out of 2) [] Proved by normalization. Level 2 subgoal 2 (induction step) for proof by induction on A: insert(u, Ac) \I B = B \I insert(u, Ac) [] Proved by cases u \in B. Conjecture inj_RRLemma.5: (A \I B):bag[U] = B \I A [] Proved by structural induction on `A:bag[U]'. The formulas cannot be ordered using the current ordering. The formulas cannot be ordered using the current ordering. LP0.1.349: LP0.1.350: qed All conjectures have been proved. LP0.1.351: set immunity off The immunity is now `off'. LP0.1.352: % ---------------------------------------------------------- LP0.1.353: LP0.1.354: LP0.1.355: % L1: Rewrite Rules Conditioned on Injectivity and "Setness" LP0.1.356: % ---------------------------------------------------------- LP0.1.357: LP0.1.358: set name inj_rr1 The name-prefix is now `inj_rr1'. LP0.1.359: prove (is_inj (f) /\ is_set (A)) => set ! (iterate (p, f) ! A) = iterate (p, f) ! A .. Attempting to prove conjecture inj_rr1.1: is_inj(f) /\ is_set(A) => set ! (iterate(p, f) ! A) = iterate(p, f) ! A The formulas cannot be ordered using the current ordering. Suspending proof of conjecture inj_rr1.1 LP0.1.360: LP0.1.361: resume by induction on A:bag[T] Creating subgoals for proof by structural induction on `A:bag[T]' Basis subgoal: Subgoal 1: \A x:T \A y:T ((f ! x):U = f ! y => x:T = y) /\ \A x:T ~(x:T \in ({} - x:T)) => set ! (iterate(p, f) ! {}) = iterate(p, f) ! {} Induction constant: Ac Induction hypothesis: inj_rr1InductHyp.1: \A x:T \A y:T ((f ! x):U = f ! y => x:T = y) /\ \A x:T ~(x \in (Ac - x:T)) => set ! (iterate(p, f) ! Ac) = iterate(p, f) ! Ac Induction subgoal: Subgoal 2: \A x:T \A y:T ((f ! x):U = f ! y => x:T = y) /\ \A x:T ~(x \in (insert(t, Ac) - x:T)) => set ! (iterate(p, f) ! insert(t, Ac)) = iterate(p, f) ! 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 inj_rr1InductHyp.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.362: LP0.1.363: % Base Case: Trivial LP0.1.364: % Inductive Case: LP0.1.365: LP0.1.366: resume by => Creating subgoals for proof of => New constants: tc, fc Hypothesis: inj_rr1ImpliesHyp.1: \A x:T \A y:T (fc ! x = fc ! y => x:T = y) /\ \A x:T ~(x \in (insert(tc, Ac) - x:T)) Subgoal: set ! (iterate(p, fc) ! insert(tc, Ac)) = iterate(p, fc) ! insert(tc, Ac) Attempting to prove level 3 subgoal for proof of => Added hypothesis inj_rr1ImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula inj_rr1ImpliesHyp.1 to yield the following formulas, which imply inj_rr1ImpliesHyp.1. inj_rr1ImpliesHyp.1.1: \A x:T ~(x \in (insert(tc, Ac) - x:T)) inj_rr1ImpliesHyp.1.2: \A x:T \A y:T (fc ! x = fc ! y => x:T = y) The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for proof of => LP0.1.367: LP0.1.368: prove is_set (Ac) by contradiction Attempting to prove level 4 lemma inj_rr1.2: is_set(Ac) Creating subgoals for proof by contradiction Hypothesis: inj_rr1ContraHyp.1: ~is_set(Ac) Only subgoal: false Attempting to prove level 5 subgoal for proof by contradiction Added hypothesis inj_rr1ContraHyp.1 to the system. Deleted rewrite rule inj_rr1InductHyp.1, which reduced to `true'. The formulas cannot be ordered using the current ordering. Suspending proof of level 5 subgoal for proof by contradiction LP0.1.369: declare operator wc: -> T LP0.1.370: fix x as wc in *Contra* A prenex-existential quantifier in formula inj_rr1ContraHyp.1 has been eliminated to produce formula inj_rr1.3, wc \in (Ac - wc) The formulas cannot be ordered using the current ordering. LP0.1.371: crit-pairs inj_rr1 with BagBasics The following equations are critical pairs between rewrite rules inj_rr1.3 and BagBasics.15. inj_rr1.4: wc \in Ac The system now contains 5 formulas and 92 rewrite rules. The rewriting system is guaranteed to terminate. The system now contains 4 formulas and 93 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.372: resume by cases wc = tc Creating subgoals for proof by cases Case hypotheses: inj_rr1CaseHyp.1.1: wc = tc inj_rr1CaseHyp.1.2: ~(wc = tc) Same subgoal for all cases: false Attempting to prove level 6 subgoal for case 1 (out of 2) Added hypothesis inj_rr1CaseHyp.1.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 6 subgoal for case 1 (out of 2) LP0.1.373: LP0.1.374: % Case 1 LP0.1.375: instan x by tc in *Implies* Formula inj_rr1ImpliesHyp.1.1 has been instantiated to formula inj_rr1ImpliesHyp.1.1.1, false Formula inj_rr1ImpliesHyp.1.2 has been instantiated to formula inj_rr1ImpliesHyp.1.2.1, fc ! tc = fc ! y => tc = y Deleted formula inj_rr1ImpliesHyp.1.2.1, which reduced to `true'. Formula inj_rr1ImpliesHyp.1.1.1, false, is inconsistent. Level 6 subgoal for case 1 (out of 2) [] Proved by impossible case. Attempting to prove level 6 subgoal for case 2 (out of 2) Added hypothesis inj_rr1CaseHyp.1.2 to the system. The formulas cannot be ordered using the current ordering. LP0.1.376: LP0.1.377: % Case 2 LP0.1.378: crit-pairs inj_rr1* with BagBasics The following equations are critical pairs between rewrite rules inj_rr1ImpliesHyp.1.1 and BagBasics.17. inj_rr1.5: ~(tc \in Ac) The system now contains 5 formulas and 94 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules inj_rr1ImpliesHyp.1.1 and BagBasics.7. inj_rr1.6: ~(tc = x) => ~(x = tc \/ x \in (Ac - x:T)) The system now contains 5 formulas and 95 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules inj_rr1ImpliesHyp.1.1 and BagBasics.16. inj_rr1.7: ~(x \in (insert(tc, Ac) - x:T - y)) The system now contains 5 formulas and 96 rewrite rules. The rewriting system is guaranteed to terminate. The system now contains 4 formulas and 97 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.379: crit-pairs inj_rr1* with inj_rr1* The following equations are critical pairs between rewrite rules inj_rr1CaseHyp.1.2 and inj_rr1.6. inj_rr1.8: false The system now contains 5 formulas and 97 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Formula inj_rr1.8, false, is inconsistent. Level 6 subgoal for case 2 (out of 2): false [] Proved by impossible case. Level 5 subgoal for proof by contradiction: false [] Proved by cases wc = tc. Level 4 lemma inj_rr1.2: is_set(Ac) [] Proved by contradiction. Attempting to prove level 3 subgoal for proof of =>: set ! (iterate(p, fc) ! insert(tc, Ac)) = iterate(p, fc) ! insert(tc, Ac) The formulas cannot be ordered using the current ordering. LP0.1.380: LP0.1.381: resume by cases p ? tc Creating subgoals for proof by cases New constant: pc Case hypotheses: inj_rr1CaseHyp.1.1: pc ? tc inj_rr1CaseHyp.1.2: ~(pc ? tc) Same subgoal for all cases: set ! (iterate(pc, fc) ! insert(tc, Ac)) = iterate(pc, fc) ! insert(tc, Ac) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis inj_rr1CaseHyp.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.382: LP0.1.383: % Case 1 LP0.1.384: LP0.1.385: resume by cases (fc ! tc) \in (iterate (pc, fc) ! Ac) Creating subgoals for proof by cases Case hypotheses: inj_rr1CaseHyp.2.1: (fc ! tc) \in (iterate(pc, fc) ! Ac) inj_rr1CaseHyp.2.2: ~((fc ! tc) \in (iterate(pc, fc) ! Ac)) Same subgoal for all cases: (if \E x:T (fc ! tc = fc ! x /\ pc ? x /\ x \in Ac) then iterate(pc, fc) ! Ac else insert(fc ! tc, iterate(pc, fc) ! Ac)) = insert(fc ! tc, iterate(pc, fc) ! Ac) Attempting to prove level 5 subgoal for case 1 (out of 2) Added hypothesis inj_rr1CaseHyp.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.386: LP0.1.387: % Case 1.1 LP0.1.388: LP0.1.389: declare operator uc: -> T LP0.1.390: fix x as uc in *Case* A prenex-existential quantifier in formula inj_rr1CaseHyp.2.1 has been eliminated to produce formula inj_rr1.3, fc ! tc = fc ! uc /\ pc ? uc /\ uc \in Ac Deduction rule lp_and_is_true has been applied to formula inj_rr1.3 to yield the following formulas, which imply inj_rr1.3. inj_rr1.3.1: fc ! tc = fc ! uc inj_rr1.3.2: pc ? uc inj_rr1.3.3: uc \in Ac The formulas cannot be ordered using the current ordering. LP0.1.391: prove uc = tc Attempting to prove level 6 lemma inj_rr1.4: uc = tc The formulas cannot be ordered using the current ordering. Suspending proof of level 6 lemma inj_rr1.4 LP0.1.392: instan x by uc, y by tc in *Implies* Formula inj_rr1ImpliesHyp.1.1 has been instantiated to formula inj_rr1ImpliesHyp.1.1.1, ~(uc \in (insert(tc, Ac) - uc)) Formula inj_rr1ImpliesHyp.1.2 has been instantiated to formula inj_rr1ImpliesHyp.1.2.1, uc = tc Deleted formula inj_rr1ImpliesHyp.1.1.1, which reduced to `true'. Level 6 lemma inj_rr1.4 [] Proved by normalization. Attempting to prove level 5 subgoal for case 1 (out of 2): (if \E x:T (fc ! tc = fc ! x /\ pc ? x /\ x \in Ac) then iterate(pc, fc) ! Ac else insert(fc ! tc, iterate(pc, fc) ! Ac)) = insert(fc ! tc, iterate(pc, fc) ! Ac) Current subgoal: iterate(pc, fc) ! Ac = insert(fc ! uc, iterate(pc, fc) ! Ac) Deleted formula inj_rr1CaseHyp.1.1, which reduced to `true'. Deleted formula inj_rr1.3.1, which reduced to `true'. The formulas cannot be ordered using the current ordering. LP0.1.393: LP0.1.394: prove uc = tc Attempting to prove level 6 lemma inj_rr1.5: uc = tc Level 6 lemma inj_rr1.5 [] Proved by normalization. Attempting to prove level 5 subgoal for case 1 (out of 2) Deleted formula inj_rr1.5, which reduced to `true'. The formulas cannot be ordered using the current ordering. Suspending proof of level 5 subgoal for case 1 (out of 2) LP0.1.395: instan x by uc, y by tc in *Implies* Formula inj_rr1ImpliesHyp.1.1 has been instantiated to formula inj_rr1ImpliesHyp.1.1.1, false Formula inj_rr1ImpliesHyp.1.1.1, false, is inconsistent. Level 5 subgoal for case 1 (out of 2) [] Proved by impossible case. Attempting to prove level 5 subgoal for case 2 (out of 2): (if \E x:T (fc ! tc = fc ! x /\ pc ? x /\ x \in Ac) then iterate(pc, fc) ! Ac else insert(fc ! tc, iterate(pc, fc) ! Ac)) = insert(fc ! tc, iterate(pc, fc) ! Ac) Added hypothesis inj_rr1CaseHyp.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): set ! (iterate(pc, fc) ! insert(tc, Ac)) = iterate(pc, fc) ! insert(tc, Ac) [] Proved by cases (fc ! tc) \in (iterate(pc, fc) ! Ac). Attempting to prove level 4 subgoal for case 2 (out of 2): set ! (iterate(pc, fc) ! insert(tc, Ac)) = iterate(pc, fc) ! insert(tc, Ac) Added hypothesis inj_rr1CaseHyp.1.2 to the system. Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for proof of =>: set ! (iterate(p, fc) ! insert(tc, Ac)) = iterate(p, fc) ! insert(tc, Ac) [] Proved by cases p ? tc. Level 2 subgoal 2 (induction step) for proof by induction on A: \A x:T \A y:T ((f ! x):U = f ! y => x:T = y) /\ \A x:T ~(x \in (insert(t, Ac) - x:T)) => set ! (iterate(p, f) ! insert(t, Ac)) = iterate(p, f) ! insert(t, Ac) [] Proved =>. Conjecture inj_rr1.1: is_inj(f) /\ is_set(A) => set ! (iterate(p, f) ! A) = iterate(p, f) ! A [] Proved by structural induction on `A:bag[T]'. The formulas cannot be ordered using the current ordering. LP0.1.396: LP0.1.397: % Case 1.2: Trivial LP0.1.398: LP0.1.399: % Case 2: Trivial LP0.1.400: LP0.1.401: qed All conjectures have been proved. LP0.1.402: LP0.1.403: set name inj_rr2 The name-prefix is now `inj_rr2'. LP0.1.404: prove is_inj (f:fun[T,U]) => iterate (p, f:fun[T,U]) ! (A \I B) = (iterate (p, f:fun[T,U]) ! A) \I (iterate (p, f:fun[T,U]) ! B) .. Attempting to prove conjecture inj_rr2.1: is_inj(f) => (iterate(p, f) ! (A \I B)):bag[U] = (iterate(p, f) ! A) \I (iterate(p, f) ! B) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture inj_rr2.1 LP0.1.405: resume by => Creating subgoals for proof of => New constant: fc Hypothesis: inj_rr2ImpliesHyp.1: \A x:T \A y:T (fc ! x = fc ! y => x:T = y) Subgoal: iterate(p, fc) ! (A \I B) = (iterate(p, fc) ! A) \I (iterate(p, fc) ! B) Attempting to prove level 2 subgoal for proof of => Added hypothesis inj_rr2ImpliesHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal for proof of => LP0.1.406: resume by induction on A:bag[T] Creating subgoals for proof by structural induction on `A:bag[T]' Basis subgoal: Subgoal 1: iterate(p, fc) ! ({} \I B) = (iterate(p, fc) ! {}) \I (iterate(p, fc) ! B) Induction constant: Ac Induction hypothesis: inj_rr2InductHyp.1: iterate(p, fc) ! (Ac \I B) = (iterate(p, fc) ! Ac) \I (iterate(p, fc) ! B) Induction subgoal: Subgoal 2: iterate(p, fc) ! (insert(t, Ac) \I B) = (iterate(p, fc) ! insert(t, Ac)) \I (iterate(p, fc) ! B) Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on A Level 3 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 3 subgoal 2 (induction step) for proof by induction on A Added hypothesis inj_rr2InductHyp.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 A LP0.1.407: LP0.1.408: % Base Case: Trivial LP0.1.409: % Inductive Case LP0.1.410: LP0.1.411: resume by cases t \in B Creating subgoals for proof by cases New constants: tc, Bc Case hypotheses: inj_rr2CaseHyp.1.1: tc \in Bc inj_rr2CaseHyp.1.2: ~(tc \in Bc) Same subgoal for all cases: iterate(p, fc) ! (if tc \in Bc then insert(tc, Ac \I (Bc - tc)) else Ac \I Bc) = (iterate(p, fc) ! insert(tc, Ac)) \I (iterate(p, fc) ! Bc) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis inj_rr2CaseHyp.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.412: LP0.1.413: % Case 1 LP0.1.414: LP0.1.415: resume by cases p ? tc Creating subgoals for proof by cases New constant: pc Case hypotheses: inj_rr2CaseHyp.2.1: pc ? tc inj_rr2CaseHyp.2.2: ~(pc ? tc) Same subgoal for all cases: iterate(pc, fc) ! insert(tc, Ac \I (Bc - tc)) = (iterate(pc, fc) ! insert(tc, Ac)) \I (iterate(pc, fc) ! Bc) Attempting to prove level 5 subgoal for case 1 (out of 2) Added hypothesis inj_rr2CaseHyp.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.416: LP0.1.417: % Case 1.1 LP0.1.418: LP0.1.419: prove \E x:T (fc ! tc = fc ! x /\ pc ? x /\ x \in Bc) by specializing x to tc .. Attempting to prove level 6 lemma inj_rr2.2: \E x:T (fc ! tc = fc ! x /\ pc ? x /\ x \in Bc) Creating subgoals for proof by specialization Subgoal: fc ! tc = fc ! tc /\ pc ? tc /\ tc \in Bc Attempting to prove level 7 subgoal for proof by specialization Level 7 subgoal for proof by specialization [] Proved by normalization. Level 6 lemma inj_rr2.2 [] Proved by specialization. Attempting to prove level 5 subgoal for case 1 (out of 2): iterate(pc, fc) ! insert(tc, Ac \I (Bc - tc)) = (iterate(pc, fc) ! insert(tc, Ac)) \I (iterate(pc, fc) ! Bc) Current subgoal: insert(fc ! tc, (iterate(pc, fc) ! Ac) \I ((iterate(pc, fc) ! Bc) - (fc ! tc))) = (if \E x:T (fc ! tc = fc ! x /\ pc ? x /\ x \in Bc) then insert(fc ! tc, (iterate(pc, fc) ! Ac) \I ((iterate(pc, fc) ! Bc) - (fc ! tc))) else (iterate(pc, fc) ! Ac) \I (iterate(pc, fc) ! Bc)) Level 5 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 5 subgoal for case 2 (out of 2): iterate(pc, fc) ! insert(tc, Ac \I (Bc - tc)) = (iterate(pc, fc) ! insert(tc, Ac)) \I (iterate(pc, fc) ! Bc) Added hypothesis inj_rr2CaseHyp.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(p, fc) ! (if tc \in Bc then insert(tc, Ac \I (Bc - tc)) else Ac \I Bc) = (iterate(p, fc) ! insert(tc, Ac)) \I (iterate(p, fc) ! Bc) [] Proved by cases p ? tc. Attempting to prove level 4 subgoal for case 2 (out of 2): iterate(p, fc) ! (if tc \in Bc then insert(tc, Ac \I (Bc - tc)) else Ac \I Bc) = (iterate(p, fc) ! insert(tc, Ac)) \I (iterate(p, fc) ! Bc) Added hypothesis inj_rr2CaseHyp.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.420: LP0.1.421: % Case 1.2: Trivial LP0.1.422: LP0.1.423: % Case 2 LP0.1.424: LP0.1.425: resume by cases p ? tc Creating subgoals for proof by cases New constant: pc Case hypotheses: inj_rr2CaseHyp.2.1: pc ? tc inj_rr2CaseHyp.2.2: ~(pc ? tc) Same subgoal for all cases: (iterate(pc, fc) ! Ac) \I (iterate(pc, fc) ! Bc) = (iterate(pc, fc) ! insert(tc, Ac)) \I (iterate(pc, fc) ! Bc) Attempting to prove level 5 subgoal for case 1 (out of 2) Added hypothesis inj_rr2CaseHyp.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.426: LP0.1.427: % Case 2.1 LP0.1.428: LP0.1.429: resume by cases ~ ((fc ! tc) \in (iterate (pc, fc) ! Bc)) Creating subgoals for proof by cases Case hypotheses: inj_rr2CaseHyp.3.1: ~((fc ! tc) \in (iterate(pc, fc) ! Bc)) inj_rr2CaseHyp.3.2: ~(~((fc ! tc) \in (iterate(pc, fc) ! Bc))) Same subgoal for all cases: (iterate(pc, fc) ! Ac) \I (iterate(pc, fc) ! Bc) = (if \E x:T (fc ! tc = fc ! x /\ pc ? x /\ x \in Bc) then insert(fc ! tc, (iterate(pc, fc) ! Ac) \I ((iterate(pc, fc) ! Bc) - (fc ! tc))) else (iterate(pc, fc) ! Ac) \I (iterate(pc, fc) ! Bc)) Attempting to prove level 6 subgoal for case 1 (out of 2) Added hypothesis inj_rr2CaseHyp.3.1 to the system. Level 6 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 6 subgoal for case 2 (out of 2) Added hypothesis inj_rr2CaseHyp.3.2 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 6 subgoal for case 2 (out of 2) LP0.1.430: LP0.1.431: % Case 2.1.1: Trivial LP0.1.432: LP0.1.433: % Case 2.1.2: LP0.1.434: declare operator xc: -> T LP0.1.435: fix x:T as xc in *Case* A prenex-existential quantifier in formula inj_rr2CaseHyp.3.2 has been eliminated to produce formula inj_rr2.2, fc ! tc = fc ! xc /\ pc ? xc /\ xc \in Bc Deduction rule lp_and_is_true has been applied to formula inj_rr2.2 to yield the following formulas, which imply inj_rr2.2. inj_rr2.2.1: fc ! tc = fc ! xc inj_rr2.2.2: pc ? xc inj_rr2.2.3: xc \in Bc The formulas cannot be ordered using the current ordering. LP0.1.436: instan x by xc, y by tc in *Implies* Formula inj_rr2ImpliesHyp.1 has been instantiated to formula inj_rr2ImpliesHyp.1.1, xc = tc Deleted formula inj_rr2CaseHyp.2.1, which reduced to `true'. Deleted formula inj_rr2.2.1, which reduced to `true'. Formula inj_rr2CaseHyp.1.2, false, is inconsistent. Level 6 subgoal for case 2 (out of 2): (iterate(pc, fc) ! Ac) \I (iterate(pc, fc) ! Bc) = (if \E x:T (fc ! tc = fc ! x /\ pc ? x /\ x \in Bc) then insert(fc ! tc, (iterate(pc, fc) ! Ac) \I ((iterate(pc, fc) ! Bc) - (fc ! tc))) else (iterate(pc, fc) ! Ac) \I (iterate(pc, fc) ! Bc)) [] Proved by impossible case. Level 5 subgoal for case 1 (out of 2): (iterate(pc, fc) ! Ac) \I (iterate(pc, fc) ! Bc) = (iterate(pc, fc) ! insert(tc, Ac)) \I (iterate(pc, fc) ! Bc) [] Proved by cases ~((fc ! tc) \in (iterate(pc, fc) ! Bc)). Attempting to prove level 5 subgoal for case 2 (out of 2): (iterate(pc, fc) ! Ac) \I (iterate(pc, fc) ! Bc) = (iterate(pc, fc) ! insert(tc, Ac)) \I (iterate(pc, fc) ! Bc) Added hypothesis inj_rr2CaseHyp.2.2 to the system. Level 5 subgoal for case 2 (out of 2) [] Proved by normalization. Level 4 subgoal for case 2 (out of 2): iterate(p, fc) ! (if tc \in Bc then insert(tc, Ac \I (Bc - tc)) else Ac \I Bc) = (iterate(p, fc) ! insert(tc, Ac)) \I (iterate(p, fc) ! Bc) [] Proved by cases p ? tc. Level 3 subgoal 2 (induction step) for proof by induction on A: iterate(p, fc) ! (insert(t, Ac) \I B) = (iterate(p, fc) ! insert(t, Ac)) \I (iterate(p, fc) ! B) [] Proved by cases t \in B. Level 2 subgoal for proof of =>: iterate(p, fc) ! (A \I B) = (iterate(p, fc) ! A) \I (iterate(p, fc) ! B) [] Proved by structural induction on `A:bag[T]'. Conjecture inj_rr2.1: is_inj(f) => (iterate(p, f) ! (A \I B)):bag[U] = (iterate(p, f) ! A) \I (iterate(p, f) ! B) [] Proved =>. The formulas cannot be ordered using the current ordering. LP0.1.437: LP0.1.438: qed All conjectures have been proved. LP0.1.439: LP0.1.440: LP0.1.441: % Section 4: Predicate Strength Inference Rules LP0.1.442: % LP0.1.443: % Proof Scripts for the Inference Rules of Figure 5 LP0.1.444: % LP0.1.445: % is_stronger (p, p) LP0.1.446: % is_stronger ((equal \oplus (f \times g)) & (p \oplus f \oplus fst), LP0.1.447: % (p \oplus g \oplus snd)) LP0.1.448: % is_stronger ((equal \oplus (f \times g)) & (p \oplus g \oplus snd), LP0.1.449: % (p \oplus f \oplus fst)) LP0.1.450: % is_stronger ((equal \oplus (f \times f)), LP0.1.451: % (equal \oplus ((g \circ f) \times (g \circ f)))) LP0.1.452: % is_stronger (p, q) /\ is_stronger (p', q') => is_stronger (p & p', q & q') LP0.1.453: % is_stronger (p, r) \/ is_stronger (q, r) => is_stronger (p & q, r) LP0.1.454: % is_inj (f) => is_stronger (equal \oplus (f \times f), equal \oplus (g \times g)) LP0.1.455: % LP0.1.456: LP0.1.457: LP0.1.458: clear LP0.1.459: set order manual The ordering-method is now `manual'. LP0.1.460: exec-silently PS_Inf_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/PS_Inf_Aux_Axioms.lp'. LP0.1.461: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.462: order formulas The system now contains 40 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.463: make immune formulas LP0.1.464: LP0.1.465: declare variables p, p', q, q', r: pred [U], f, g: fun [T, U], g: fun [U, V], g: fun [T, V] .. LP0.1.466: LP0.1.467: LP0.1.468: % L1: Rules for Inference of Predicate Strength LP0.1.469: % --------------------------------------------- LP0.1.470: LP0.1.471: set name ps_inf1 The name-prefix is now `ps_inf1'. LP0.1.472: prove is_stronger (p:pred[T], p) Attempting to prove conjecture ps_inf1.1: is_stronger(p:pred[T], p) Conjecture ps_inf1.1 [] Proved by normalization. Deleted formula ps_inf1.1, which reduced to `true'. LP0.1.473: qed All conjectures have been proved. LP0.1.474: LP0.1.475: set name ps_inf2 The name-prefix is now `ps_inf2'. LP0.1.476: prove is_stronger ((eq \oplus (f:fun[T,U] \times g:fun[T,U])) & (p \oplus f:fun[T,U] \oplus fst), (p \oplus g:fun[T,U] \oplus snd)) .. Attempting to prove conjecture ps_inf2.1: is_stronger( (eq:pred[pair[U, U]] \oplus (f \times g)) & (p \oplus f \oplus fst), p \oplus g \oplus snd) Suspending proof of conjecture ps_inf2.1 LP0.1.477: resume by => Creating subgoals for proof of => New constants: pc, fc, xc, gc Hypothesis: ps_inf2ImpliesHyp.1: eq ? ((fc \times gc) ! xc) /\ pc ? (fc ! (fst ! xc)) Subgoal: pc ? (gc ! (snd ! xc)) Attempting to prove level 2 subgoal for proof of => Added hypothesis ps_inf2ImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula ps_inf2ImpliesHyp.1 to yield the following formulas, which imply ps_inf2ImpliesHyp.1. ps_inf2ImpliesHyp.1.1: pc ? (fc ! (fst ! xc)) ps_inf2ImpliesHyp.1.2: eq ? ((fc \times gc) ! xc) The system now contains 42 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 2 subgoal for proof of => LP0.1.478: set immunity on The immunity is now `on'. LP0.1.479: instan pr:pair[T,T] by xc in Pairs / cont-oper (=:pair[T,T],pair[T,T] -> Bool) .. Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T \E y:T (xc = [x, y]) The system now contains 43 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.480: set immunity off The immunity is now `off'. LP0.1.481: LP0.1.482: declare operator tc, t'c: -> T LP0.1.483: fix x:T as tc in Pairs / cont-oper (xc) A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula ps_inf2.2, \E y:T (xc = [tc, y]) The system now contains 44 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.484: fix y:T as t'c in ps_inf2 / cont-oper (tc) A prenex-existential quantifier in formula ps_inf2.2 has been eliminated to produce formula ps_inf2.3, xc = [tc, t'c] Deleted formula ps_inf2.2, which reduced to `true'. Level 2 subgoal for proof of =>: pc ? (gc ! (snd ! xc)) [] Proved by normalization. Conjecture ps_inf2.1: is_stronger( (eq:pred[pair[U, U]] \oplus (f \times g)) & (p \oplus f \oplus fst), p \oplus g \oplus snd) [] Proved =>. The system now contains 41 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.485: LP0.1.486: qed All conjectures have been proved. LP0.1.487: LP0.1.488: set name ps_inf3 The name-prefix is now `ps_inf3'. LP0.1.489: prove is_stronger ((eq \oplus (f:fun[T,U] \times g:fun[T,U])) & (p \oplus g:fun[T,U] \oplus snd), (p \oplus f:fun[T,U] \oplus fst)) .. Attempting to prove conjecture ps_inf3.1: is_stronger( (eq:pred[pair[U, U]] \oplus (f \times g)) & (p \oplus g \oplus snd), p \oplus f \oplus fst) Suspending proof of conjecture ps_inf3.1 LP0.1.490: LP0.1.491: resume by => Creating subgoals for proof of => New constants: pc, gc, xc, fc Hypothesis: ps_inf3ImpliesHyp.1: eq ? ((fc \times gc) ! xc) /\ pc ? (gc ! (snd ! xc)) Subgoal: pc ? (fc ! (fst ! xc)) Attempting to prove level 2 subgoal for proof of => Added hypothesis ps_inf3ImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula ps_inf3ImpliesHyp.1 to yield the following formulas, which imply ps_inf3ImpliesHyp.1. ps_inf3ImpliesHyp.1.1: pc ? (gc ! (snd ! xc)) ps_inf3ImpliesHyp.1.2: eq ? ((fc \times gc) ! xc) The system now contains 43 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 2 subgoal for proof of => LP0.1.492: set immunity on The immunity is now `on'. LP0.1.493: instan pr:pair[T,T] by xc in Pairs / cont-oper (=:pair[T,T],pair[T,T] -> Bool) .. Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T \E y:T (xc = [x, y]) The system now contains 44 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.494: set immunity off The immunity is now `off'. LP0.1.495: LP0.1.496: declare operator tc, t'c: -> T LP0.1.497: fix x:T as tc in Pairs / cont-oper (xc) A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula ps_inf3.2, \E y:T (xc = [tc, y]) The system now contains 45 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.498: fix y:T as t'c in ps_inf3 / cont-oper (tc) A prenex-existential quantifier in formula ps_inf3.2 has been eliminated to produce formula ps_inf3.3, xc = [tc, t'c] Deleted formula ps_inf3.2, which reduced to `true'. Level 2 subgoal for proof of =>: pc ? (fc ! (fst ! xc)) [] Proved by normalization. Conjecture ps_inf3.1: is_stronger( (eq:pred[pair[U, U]] \oplus (f \times g)) & (p \oplus g \oplus snd), p \oplus f \oplus fst) [] Proved =>. The system now contains 42 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.499: LP0.1.500: qed All conjectures have been proved. LP0.1.501: LP0.1.502: set name ps_inf4 The name-prefix is now `ps_inf4'. LP0.1.503: prove is_stronger ((eq \oplus (f:fun[T,U] \times f)), (eq \oplus ((g:fun[U,V] \circ f:fun[T,U]) \times (g:fun[U,V] \circ f:fun[T,U])))) .. Attempting to prove conjecture ps_inf4.1: is_stronger(eq:pred[pair[U, U]] \oplus (f \times f), eq \oplus ((g \circ f) \times (g \circ f))) Suspending proof of conjecture ps_inf4.1 LP0.1.504: resume by => Creating subgoals for proof of => New constants: fc, xc Hypothesis: ps_inf4ImpliesHyp.1: eq ? ((fc \times fc) ! xc) Subgoal: eq ? (((g \circ fc) \times (g \circ fc)) ! xc) Attempting to prove level 2 subgoal for proof of => Added hypothesis ps_inf4ImpliesHyp.1 to the system. The system now contains 43 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 2 subgoal for proof of => LP0.1.505: set immunity on The immunity is now `on'. LP0.1.506: instan pr:pair[T,T] by xc in Pairs / cont-oper (=:pair[T,T],pair[T,T] -> Bool) Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T \E y:T (xc = [x, y]) The system now contains 44 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.507: set immunity off The immunity is now `off'. LP0.1.508: LP0.1.509: declare operator tc, t'c: -> T LP0.1.510: fix x:T as tc in Pairs / cont-oper (xc) A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula ps_inf4.2, \E y:T (xc = [tc, y]) The system now contains 45 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.511: fix y:T as t'c in ps_inf4 / cont-oper (tc) A prenex-existential quantifier in formula ps_inf4.2 has been eliminated to produce formula ps_inf4.3, xc = [tc, t'c] Deleted formula ps_inf4.2, which reduced to `true'. Level 2 subgoal for proof of =>: eq ? (((g \circ fc) \times (g \circ fc)) ! xc) [] Proved by normalization. Conjecture ps_inf4.1: is_stronger(eq:pred[pair[U, U]] \oplus (f \times f), eq \oplus ((g \circ f) \times (g \circ f))) [] Proved =>. The system now contains 43 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.512: qed All conjectures have been proved. LP0.1.513: LP0.1.514: set name ps_inf5 The name-prefix is now `ps_inf5'. LP0.1.515: prove is_stronger (p:pred[U], q) /\ is_stronger (p':pred[U], q') => is_stronger (p:pred[U] & p', q:pred[U] & q') .. Attempting to prove conjecture ps_inf5.1: is_stronger(p:pred[U], q) /\ is_stronger(p', q') => is_stronger(p & p', q & q') Suspending proof of conjecture ps_inf5.1 LP0.1.516: resume by => Creating subgoals for proof of => New constants: p'c, q'c, pc, qc Hypothesis: ps_inf5ImpliesHyp.1: \A x:U (pc ? x => qc ? x) /\ \A x:U (p'c ? x => q'c ? x) Subgoal: \A x:U (pc ? x /\ p'c ? x => qc ? x /\ q'c ? x) Attempting to prove level 2 subgoal for proof of => Added hypothesis ps_inf5ImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula ps_inf5ImpliesHyp.1 to yield the following formulas, which imply ps_inf5ImpliesHyp.1. ps_inf5ImpliesHyp.1.1: \A x:U (p'c ? x => q'c ? x) ps_inf5ImpliesHyp.1.2: \A x:U (pc ? x => qc ? x) The system now contains 45 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 2 subgoal for proof of => LP0.1.517: resume by => Creating subgoals for proof of => New constant: xc Hypothesis: ps_inf5ImpliesHyp.2: pc ? xc /\ p'c ? xc Subgoal: qc ? xc /\ q'c ? xc Attempting to prove level 3 subgoal for proof of => Added hypothesis ps_inf5ImpliesHyp.2 to the system. Deduction rule lp_and_is_true has been applied to formula ps_inf5ImpliesHyp.2 to yield the following formulas, which imply ps_inf5ImpliesHyp.2. ps_inf5ImpliesHyp.2.1: p'c ? xc ps_inf5ImpliesHyp.2.2: pc ? xc Level 3 subgoal for proof of => [] Proved by normalization. Level 2 subgoal for proof of => [] Proved =>. Conjecture ps_inf5.1: is_stronger(p:pred[U], q) /\ is_stronger(p', q') => is_stronger(p & p', q & q') [] Proved =>. The system now contains 44 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.518: qed All conjectures have been proved. LP0.1.519: LP0.1.520: set name ps_inf6 The name-prefix is now `ps_inf6'. LP0.1.521: prove is_stronger (p:pred[U], r) \/ is_stronger (q:pred[U], r) => is_stronger (p:pred[U] & q, r) .. Attempting to prove conjecture ps_inf6.1: is_stronger(p, r) \/ is_stronger(q, r) => is_stronger(p & q, r) Suspending proof of conjecture ps_inf6.1 LP0.1.522: resume by => Creating subgoals for proof of => New constants: pc, rc, qc Hypothesis: ps_inf6ImpliesHyp.1: \A x:U (pc ? x => rc ? x) \/ \A x:U (qc ? x => rc ? x) Subgoal: \A x:U (pc ? x /\ qc ? x => rc ? x) Attempting to prove level 2 subgoal for proof of => Added hypothesis ps_inf6ImpliesHyp.1 to the system. The system now contains 45 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 2 subgoal for proof of => LP0.1.523: resume by => Creating subgoals for proof of => New constant: xc Hypothesis: ps_inf6ImpliesHyp.2: pc ? xc /\ qc ? xc Subgoal: rc ? xc Attempting to prove level 3 subgoal for proof of => Added hypothesis ps_inf6ImpliesHyp.2 to the system. Deduction rule lp_and_is_true has been applied to formula ps_inf6ImpliesHyp.2 to yield the following formulas, which imply ps_inf6ImpliesHyp.2. ps_inf6ImpliesHyp.2.1: pc ? xc ps_inf6ImpliesHyp.2.2: qc ? xc The system now contains 47 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 3 subgoal for proof of => LP0.1.524: resume by cases is_stronger (pc, rc) Creating subgoals for proof by cases Case hypotheses: ps_inf6CaseHyp.1.1: is_stronger(pc, rc) ps_inf6CaseHyp.1.2: ~is_stronger(pc, rc) Same subgoal for all cases: rc ? xc Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis ps_inf6CaseHyp.1.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 ps_inf6CaseHyp.1.2 to the system. Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for proof of => [] Proved by cases is_stronger(pc, rc). Level 2 subgoal for proof of =>: \A x:U (pc ? x /\ qc ? x => rc ? x) [] Proved =>. Conjecture ps_inf6.1: is_stronger(p, r) \/ is_stronger(q, r) => is_stronger(p & q, r) [] Proved =>. The system now contains 45 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.525: qed All conjectures have been proved. LP0.1.526: LP0.1.527: set name ps_inf7 The name-prefix is now `ps_inf7'. LP0.1.528: prove is_inj (f:fun[T,U]) => is_stronger (eq \oplus (f:fun[T,U] \times f:fun[T,U]), eq \oplus (g:fun[T,V] \times g:fun[T,V])) .. Attempting to prove conjecture ps_inf7.1: is_inj(f) => is_stronger(eq:pred[pair[U, U]] \oplus (f \times f), eq:pred[pair[V, V]] \oplus (g \times g)) Suspending proof of conjecture ps_inf7.1 LP0.1.529: resume by => Creating subgoals for proof of => New constant: fc Hypothesis: ps_inf7ImpliesHyp.1: \A x:T \A y:T (fc ! x = fc ! y => x:T = y) Subgoal: \A x:pair[T, T] (eq ? ((fc \times fc) ! x) => eq:pred[pair[V, V]] ? ((g \times g) ! x)) Attempting to prove level 2 subgoal for proof of => Added hypothesis ps_inf7ImpliesHyp.1 to the system. The system now contains 46 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 2 subgoal for proof of => LP0.1.530: resume by => Creating subgoals for proof of => New constant: xc Hypothesis: ps_inf7ImpliesHyp.2: eq ? ((fc \times fc) ! xc) Subgoal: eq:pred[pair[V, V]] ? ((g \times g) ! xc) Attempting to prove level 3 subgoal for proof of => Added hypothesis ps_inf7ImpliesHyp.2 to the system. The system now contains 47 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 3 subgoal for proof of => LP0.1.531: set immunity on The immunity is now `on'. LP0.1.532: instan pr:pair[T,T] by xc in Pairs / cont-oper (=:pair[T,T],pair[T,T] -> Bool) Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T \E y:T (xc = [x, y]) The system now contains 48 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.533: set immunity off The immunity is now `off'. LP0.1.534: LP0.1.535: declare operator tc, t'c: -> T LP0.1.536: fix x:T as tc in Pairs / cont-oper (xc) A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula ps_inf7.2, \E y:T (xc = [tc, y]) The system now contains 49 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.537: fix y:T as t'c in ps_inf7 / cont-oper (tc) A prenex-existential quantifier in formula ps_inf7.2 has been eliminated to produce formula ps_inf7.3, xc = [tc, t'c] Deleted formula ps_inf7.2, which reduced to `true'. LP0.1.538: instan x by tc, y by t'c in *Implies* Formula ps_inf7ImpliesHyp.1 has been instantiated to formula ps_inf7ImpliesHyp.1.1, tc = t'c Level 3 subgoal for proof of =>: eq:pred[pair[V, V]] ? ((g \times g) ! xc) [] Proved by normalization. Level 2 subgoal for proof of =>: \A x:pair[T, T] (eq ? ((fc \times fc) ! x) => eq:pred[pair[V, V]] ? ((g \times g) ! x)) [] Proved =>. Conjecture ps_inf7.1: is_inj(f) => is_stronger(eq:pred[pair[U, U]] \oplus (f \times f), eq:pred[pair[V, V]] \oplus (g \times g)) [] Proved =>. The system now contains 46 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.539: qed All conjectures have been proved. LP0.1.540: LP0.1.541: LP0.1.542: LP0.1.543: % Section 5: Conditional Rewrite Rules Involving Predicate Strength LP0.1.544: % LP0.1.545: % Proof Scripts for the Conditional Rewrite Rules of Figure 6 LP0.1.546: % LP0.1.547: % is_stronger (p, q) :: (p & q) --> p LP0.1.548: % is_stronger (p, q) :: p --> (p & q) LP0.1.549: % is_stronger (p, q) :: forall (q) ? (iterate (p, id) ! _) --> true LP0.1.550: % is_stronger (p, q) :: exists (q) ? (iterate (p, id) ! _) --> exists (p) ? A LP0.1.551: % is_stronger (p, q) :: forall (q) ? (join (p, id) ! [_, _]) --> true LP0.1.552: % LP0.1.553: LP0.1.554: LP0.1.555: clear LP0.1.556: set order manual The ordering-method is now `manual'. LP0.1.557: exec-silently PS_RR_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/PS_RR_Aux_Axioms.lp'. LP0.1.558: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.559: order formulas The formulas cannot be ordered using the current ordering. LP0.1.560: make immune formulas LP0.1.561: LP0.1.562: declare variables p, q: pred [T], p, q: pred [pair [T, U]], A: bag [T], B: bag [U] .. LP0.1.563: LP0.1.564: LP0.1.565: % L1: Rewrite Rules Conditioned on Predicate Strength LP0.1.566: % --------------------------------------------------- LP0.1.567: LP0.1.568: set name ps_rr1 The name-prefix is now `ps_rr1'. LP0.1.569: prove is_stronger (p:pred[T], q) => ((p:pred[T] & q) = p) Attempting to prove conjecture ps_rr1.1: is_stronger(p:pred[T], q) => p & q = p The formulas cannot be ordered using the current ordering. Suspending proof of conjecture ps_rr1.1 LP0.1.570: resume by => Creating subgoals for proof of => New constants: pc, qc Hypothesis: ps_rr1ImpliesHyp.1: \A x:T (pc ? x => qc ? x) Subgoal: \A x:T (pc ? x /\ qc ? x <=> pc ? x) Attempting to prove level 2 subgoal for proof of => Added hypothesis ps_rr1ImpliesHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal for proof of => LP0.1.571: resume by <=> Creating subgoals for proof of <=> New constant: xc => hypothesis: ps_rr1ImpliesHyp.2: pc ? xc /\ qc ? xc => subgoal: pc ? xc <= hypothesis: ps_rr1ImpliesHyp.3: pc ? xc <= subgoal: pc ? xc /\ qc ? xc Attempting to prove level 3 subgoal 1 for proof of <=> Added hypothesis ps_rr1ImpliesHyp.2 to the system. Deduction rule lp_and_is_true has been applied to formula ps_rr1ImpliesHyp.2 to yield the following formulas, which imply ps_rr1ImpliesHyp.2. ps_rr1ImpliesHyp.2.1: pc ? xc ps_rr1ImpliesHyp.2.2: qc ? xc Level 3 subgoal 1 for proof of <=> [] Proved by normalization. Attempting to prove level 3 subgoal 2 for proof of <=> Added hypothesis ps_rr1ImpliesHyp.3 to the system. Level 3 subgoal 2 for proof of <=> [] Proved by normalization. Level 2 subgoal for proof of => [] Proved <=>. Conjecture ps_rr1.1: is_stronger(p:pred[T], q) => p & q = p [] Proved =>. The formulas cannot be ordered using the current ordering. LP0.1.572: qed All conjectures have been proved. LP0.1.573: LP0.1.574: set name ps_rr2 The name-prefix is now `ps_rr2'. LP0.1.575: prove is_stronger (p:pred[T], q) => (p:pred[T] = (p & q)) Attempting to prove conjecture ps_rr2.1: is_stronger(p:pred[T], q) => p = p & q The formulas cannot be ordered using the current ordering. Suspending proof of conjecture ps_rr2.1 LP0.1.576: resume by => Creating subgoals for proof of => New constants: pc, qc Hypothesis: ps_rr2ImpliesHyp.1: \A x:T (pc ? x => qc ? x) Subgoal: \A x:T (pc ? x /\ qc ? x <=> pc ? x) Attempting to prove level 2 subgoal for proof of => Added hypothesis ps_rr2ImpliesHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal for proof of => LP0.1.577: resume by <=> Creating subgoals for proof of <=> New constant: xc => hypothesis: ps_rr2ImpliesHyp.2: pc ? xc /\ qc ? xc => subgoal: pc ? xc <= hypothesis: ps_rr2ImpliesHyp.3: pc ? xc <= subgoal: pc ? xc /\ qc ? xc Attempting to prove level 3 subgoal 1 for proof of <=> Added hypothesis ps_rr2ImpliesHyp.2 to the system. Deduction rule lp_and_is_true has been applied to formula ps_rr2ImpliesHyp.2 to yield the following formulas, which imply ps_rr2ImpliesHyp.2. ps_rr2ImpliesHyp.2.1: pc ? xc ps_rr2ImpliesHyp.2.2: qc ? xc Level 3 subgoal 1 for proof of <=> [] Proved by normalization. Attempting to prove level 3 subgoal 2 for proof of <=> Added hypothesis ps_rr2ImpliesHyp.3 to the system. Level 3 subgoal 2 for proof of <=> [] Proved by normalization. Level 2 subgoal for proof of => [] Proved <=>. Conjecture ps_rr2.1: is_stronger(p:pred[T], q) => p = p & q [] Proved =>. Deleted formula ps_rr2.1, which reduced to `true'. The formulas cannot be ordered using the current ordering. LP0.1.578: qed All conjectures have been proved. LP0.1.579: LP0.1.580: set name ps_rr3 The name-prefix is now `ps_rr3'. LP0.1.581: prove is_stronger (p:pred[T], q) => (for_all (q:pred[T]) ? (iterate (p:pred[T], id) ! A) = true) .. Attempting to prove conjecture ps_rr3.1: is_stronger(p:pred[T], q) => for_all(q) ? (iterate(p, id) ! A) = true The formulas cannot be ordered using the current ordering. Suspending proof of conjecture ps_rr3.1 LP0.1.582: resume by => Creating subgoals for proof of => New constants: pc, qc Hypothesis: ps_rr3ImpliesHyp.1: \A x:T (pc ? x => qc ? x) Subgoal: \A x:T (pc ? x /\ x:T \in A => qc ? x) Attempting to prove level 2 subgoal for proof of => Added hypothesis ps_rr3ImpliesHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal for proof of => LP0.1.583: resume by => Creating subgoals for proof of => New constants: xc, Ac Hypothesis: ps_rr3ImpliesHyp.2: pc ? xc /\ xc \in Ac Subgoal: qc ? xc Attempting to prove level 3 subgoal for proof of => Added hypothesis ps_rr3ImpliesHyp.2 to the system. Deduction rule lp_and_is_true has been applied to formula ps_rr3ImpliesHyp.2 to yield the following formulas, which imply ps_rr3ImpliesHyp.2. ps_rr3ImpliesHyp.2.1: pc ? xc ps_rr3ImpliesHyp.2.2: xc \in Ac Level 3 subgoal for proof of => [] Proved by normalization. Level 2 subgoal for proof of => [] Proved =>. Conjecture ps_rr3.1 [] Proved =>. The formulas cannot be ordered using the current ordering. LP0.1.584: qed All conjectures have been proved. LP0.1.585: LP0.1.586: set name ps_rr4 The name-prefix is now `ps_rr4'. LP0.1.587: prove is_stronger (p:pred[T], q) => (exists (q:pred[T]) ? (iterate (p:pred[T], id) ! A) = exists (p) ? A) .. Attempting to prove conjecture ps_rr4.1: is_stronger(p:pred[T], q) => exists(q) ? (iterate(p, id) ! A) = exists(p) ? A The formulas cannot be ordered using the current ordering. Suspending proof of conjecture ps_rr4.1 LP0.1.588: resume by => Creating subgoals for proof of => New constants: pc, qc Hypothesis: ps_rr4ImpliesHyp.1: \A x:T (pc ? x => qc ? x) Subgoal: \E x:T (pc ? x /\ qc ? x /\ x:T \in A) = \E x:T (x:T \in A /\ pc ? x) Attempting to prove level 2 subgoal for proof of => Added hypothesis ps_rr4ImpliesHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal for proof of => LP0.1.589: declare operator xc: -> T LP0.1.590: resume by <=> Creating subgoals for proof of <=> New constant: Ac => hypothesis: ps_rr4ImpliesHyp.2: \E x:T (pc ? x /\ qc ? x /\ x \in Ac) => subgoal: \E x:T (x \in Ac /\ pc ? x) <= hypothesis: ps_rr4ImpliesHyp.3: \E x:T (x \in Ac /\ pc ? x) <= subgoal: \E x:T (pc ? x /\ qc ? x /\ x \in Ac) Attempting to prove level 3 subgoal 1 for proof of <=> Added hypothesis ps_rr4ImpliesHyp.2 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal 1 for proof of <=> LP0.1.591: LP0.1.592: % => LP0.1.593: LP0.1.594: fix x as xc in *Implies* A prenex-existential quantifier in formula ps_rr4ImpliesHyp.2 has been eliminated to produce formula ps_rr4.2, pc ? xc /\ qc ? xc /\ xc \in Ac Deduction rule lp_and_is_true has been applied to formula ps_rr4.2 to yield the following formulas, which imply ps_rr4.2. ps_rr4.2.1: pc ? xc ps_rr4.2.2: qc ? xc ps_rr4.2.3: xc \in Ac The formulas cannot be ordered using the current ordering. LP0.1.595: resume by specializing x to xc Creating subgoals for proof by specialization Subgoal: xc \in Ac /\ pc ? xc Attempting to prove level 4 subgoal for proof by specialization Level 4 subgoal for proof by specialization [] Proved by normalization. Level 3 subgoal 1 for proof of <=> [] Proved by specialization. Attempting to prove level 3 subgoal 2 for proof of <=> Added hypothesis ps_rr4ImpliesHyp.3 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal 2 for proof of <=>: \E x:T (pc ? x /\ qc ? x /\ x \in Ac) LP0.1.596: LP0.1.597: % <= LP0.1.598: LP0.1.599: fix x as xc in *Implies* A prenex-existential quantifier in formula ps_rr4ImpliesHyp.3 has been eliminated to produce formula ps_rr4.2, xc \in Ac /\ pc ? xc Deduction rule lp_and_is_true has been applied to formula ps_rr4.2 to yield the following formulas, which imply ps_rr4.2. ps_rr4.2.1: pc ? xc ps_rr4.2.2: xc \in Ac The formulas cannot be ordered using the current ordering. LP0.1.600: resume by specializing x to xc Creating subgoals for proof by specialization Subgoal: pc ? xc /\ qc ? xc /\ xc \in Ac Attempting to prove level 4 subgoal for proof by specialization Level 4 subgoal for proof by specialization [] Proved by normalization. Level 3 subgoal 2 for proof of <=> [] Proved by specialization. Level 2 subgoal for proof of =>: \E x:T (pc ? x /\ qc ? x /\ x:T \in A) = \E x:T (x:T \in A /\ pc ? x) [] Proved <=>. Conjecture ps_rr4.1: is_stronger(p:pred[T], q) => exists(q) ? (iterate(p, id) ! A) = exists(p) ? A [] Proved =>. The formulas cannot be ordered using the current ordering. LP0.1.601: LP0.1.602: qed All conjectures have been proved. LP0.1.603: LP0.1.604: set name ps_rr5 The name-prefix is now `ps_rr5'. LP0.1.605: prove is_stronger (p:pred[pair [T, U]], q) => (for_all (q:pred[pair [T, U]]) ? (join (p:pred[pair [T, U]], id) ! [A, B]) = true) .. Attempting to prove conjecture ps_rr5.1: is_stronger(p:pred[pair[T, U]], q) => for_all(q) ? (join(p, id) ! [A, B]) = true The formulas cannot be ordered using the current ordering. Suspending proof of conjecture ps_rr5.1 LP0.1.606: resume by => Creating subgoals for proof of => New constants: pc, qc Hypothesis: ps_rr5ImpliesHyp.1: \A x:pair[T, U] (pc ? x => qc ? x) Subgoal: \A x:pair[T, U] (\E x:T \E y:U (x:pair[T, U] = [x, y] /\ pc ? [x, y] /\ x:T \in A /\ y:U \in B) => qc ? x) Attempting to prove level 2 subgoal for proof of => Added hypothesis ps_rr5ImpliesHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal for proof of => LP0.1.607: resume by => Creating subgoals for proof of => New constants: xc, Ac, Bc Hypothesis: ps_rr5ImpliesHyp.2: \E x:T \E y:U (xc = [x, y] /\ pc ? [x, y] /\ x \in Ac /\ y \in Bc) Subgoal: qc ? xc Attempting to prove level 3 subgoal for proof of => Added hypothesis ps_rr5ImpliesHyp.2 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for proof of => LP0.1.608: declare operator tc: -> T, uc: -> U LP0.1.609: fix x as tc in *Implies* A prenex-existential quantifier in formula ps_rr5ImpliesHyp.2 has been eliminated to produce formula ps_rr5.2, \E y:U (xc = [tc, y] /\ pc ? [tc, y] /\ tc \in Ac /\ y \in Bc) The formulas cannot be ordered using the current ordering. LP0.1.610: fix y as uc in ps_rr5 / contains-oper (tc) A prenex-existential quantifier in formula ps_rr5.2 has been eliminated to produce formula ps_rr5.3, xc = [tc, uc] /\ pc ? [tc, uc] /\ tc \in Ac /\ uc \in Bc Deduction rule lp_and_is_true has been applied to formula ps_rr5.3 to yield the following formulas, which imply ps_rr5.3. ps_rr5.3.1: xc = [tc, uc] ps_rr5.3.2: pc ? [tc, uc] ps_rr5.3.3: tc \in Ac ps_rr5.3.4: uc \in Bc Level 3 subgoal for proof of => [] Proved by normalization. Level 2 subgoal for proof of =>: \A x:pair[T, U] (\E x:T \E y:U (x:pair[T, U] = [x, y] /\ pc ? [x, y] /\ x:T \in A /\ y:U \in B) => qc ? x) [] Proved =>. Conjecture ps_rr5.1: is_stronger(p:pred[pair[T, U]], q) => for_all(q) ? (join(p, id) ! [A, B]) = true [] Proved =>. The formulas cannot be ordered using the current ordering. LP0.1.611: qed All conjectures have been proved. LP0.1.612: LP0.1.613: quit End of input from file `/pro/oodb/specs/KOLA98/VLDB98_Scripts.lp'. End of input from file `command line arguments'.