LP (the Larch Prover), Release 3.1a (95/04/27) logging to `/pro/oodb/specs/KOLA98/pushdown-scripts.lplog' on 21 June 1998 18:55:51. LP0.1.2: LP0.1.3: % ****************************************************************************** LP0.1.4: % * * LP0.1.5: % * Script File: SIGMOD98_Scripts * LP0.1.6: % * -------------------------------------------------------------------------- * LP0.1.7: % * Scripts Author: Mitch Cherniack (mfc@cs.brandeis.edu) * LP0.1.8: % * Date: June, 1998 * LP0.1.9: % * * LP0.1.10: % * Present Address: Computer Science Department * LP0.1.11: % * Brandeis University * LP0.1.12: % * Waltham, MA 02254 * LP0.1.13: % * -------------------------------------------------------------------------- * LP0.1.14: % * * LP0.1.15: % * Proof Scripts Establishing Correctness of Rewrite Rules used in the paper, * LP0.1.16: % * [CZ98a]: * LP0.1.17: % * * LP0.1.18: % * [CZ98a] Changing the Rules: Transformations for Rule-Based Optimizers * LP0.1.19: % * Mitch Cherniack and Stan Zdonik, In Proceedings of the 1998 ACM * LP0.1.20: % * SIGMOD International Conference on Management of Data, Seattle, * LP0.1.21: % * WA, June, 1998. * LP0.1.22: % * * LP0.1.23: % * For an up-to-date version of [CZ98a], see: * LP0.1.24: % * ftp://wilma.cs.brown.edu/u/mfc/sigmod98.ps.Z * LP0.1.25: % * * LP0.1.26: % * * LP0.1.27: % * Instructions: * LP0.1.28: % * * LP0.1.29: % * Requires Version 3.1a of the LP Theorem Prover, available from * LP0.1.30: % * MIT, Laboratory of Computer Science. For software and documentation on * LP0.1.31: % * LP see: * LP0.1.32: % * * LP0.1.33: % * http://www.sds.lcs.mit.edu/spd/larch/LP/overview.html * LP0.1.34: % * * LP0.1.35: % * With LP installed in $path, run this theorem prover script by typing * LP0.1.36: % * * LP0.1.37: % * $path/lp -c SIGMOD98_Scripts * LP0.1.38: % * * LP0.1.39: % ****************************************************************************** LP0.1.40: LP0.1.41: % Section 3: Predicate Pushdown LP0.1.42: % LP0.1.43: % Proof Scripts for COKO Transformation, LP0.1.44: % LP0.1.45: % TRANSFORMATION Pushdown LP0.1.46: % USES LP0.1.47: % SNF, LP0.1.48: % push: join ((p OPLUS #1) & (q OPLUS #2) & r, f) ! [A, B] --> LP0.1.49: % join (r, f) ! [iterate (p, id) ! A, iterate (q, id) ! B], LP0.1.50: % simp: iterate (K (true), id) ! A --> A LP0.1.51: % LP0.1.52: % BEGIN LP0.1.53: % GIVEN join (p, _F) ! _O DO { LP0.1.54: % SNF (p); LP0.1.55: % push; LP0.1.56: % GIVEN join (_P, _F) ! [A, B] DO { LP0.1.57: % simp (A); LP0.1.58: % simp (B) LP0.1.59: % } LP0.1.60: % } LP0.1.61: % END LP0.1.62: % LP0.1.63: % In [CZ98a], only rules push and simp are described. LP0.1.64: % LP0.1.65: LP0.1.66: clear LP0.1.67: forget Critical pair list cleared. LP0.1.68: unregister registry LP0.1.69: set order manual The ordering-method is now `manual'. LP0.1.70: exec-silently Pushdown_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/Pushdown_Aux_Axioms.lp'. LP0.1.71: declare variables p: pred [T1], p: pred [T2], q: pred [T2], x: T1, y: T2, r: pred [pair [T1, T2]], f: fun [pair [T1, T2], U], f, g: fun [T2, T2], A: bag [T1], B: bag [T2] .. LP0.1.72: LP0.1.73: LP0.1.74: register height [__,__]:T2,T1->pair[T2, T1] = [__,__]:T1,T2->pair[T1, T2] Registry extended. LP0.1.75: register height ?:pred[pair[T2, T1]],pair[T2, T1]->Bool = ?:pred[pair[T1, T2]],pair[T1, T2]->Bool .. Registry extended. LP0.1.76: register height ?:pred[T1],T1->Bool = ?:pred[pair[T2, T1]],pair[T2, T1]->Bool Registry extended. LP0.1.77: register height ?:pred[T1],T1->Bool > [__,__]:T2,T1->pair[T2, T1] Registry extended. LP0.1.78: register height ?:pred[T2],T2->Bool = ?:pred[pair[T1, T2]],pair[T1, T2]->Bool Registry extended. LP0.1.79: register height ?:pred[T2],T2->Bool > [__,__]:T1,T2->pair[T1, T2] Registry extended. LP0.1.80: register height !:fun[bag[T2], bag[T2]],bag[T2]->bag[T2] = !:fun[bag[T2], bag[U]],bag[T2]->bag[U] .. Registry extended. LP0.1.81: register height C:pred[pair[T1, T2]],T1->pred[T2] > (&:pred[T2],pred[T2]->pred[T2], \circ:fun[bag[T2], bag[U]],fun[bag[T2], bag[T2]]->fun[bag[T2], bag[U]], iterate:pred[T2],fun[T2, U]->fun[bag[T2], bag[U]], iterate:pred[T2],fun[T2, T2]->fun[bag[T2], bag[T2]]) .. Registry extended. LP0.1.82: register height &:pred[T2],pred[T2]->pred[T2] = \circ:fun[bag[T2], bag[U]],fun[bag[T2], bag[T2]]->fun[bag[T2], bag[U]] = iterate:pred[T2],fun[T2, U]->fun[bag[T2], bag[U]] .. Registry extended. LP0.1.83: register height &:pred[T2],pred[T2]->pred[T2] >= iterate:pred[T2],fun[T2, T2]->fun[bag[T2], bag[T2]] .. Registry extended. LP0.1.84: register stat L =>, !:fun[bag[T2], bag[U]],bag[T2]->bag[U], !:fun[bag[T2], bag[T2]],bag[T2]->bag[T2], &:pred[T2],pred[T2]->pred[T2], \circ:fun[bag[T2], bag[U]],fun[bag[T2], bag[T2]]->fun[bag[T2], bag[U]] .. LP0.1.85: register stat R iterate:pred[T2],fun[T2, U]->fun[bag[T2], bag[U]] .. LP0.1.86: register stat multiset /\, \/, <=> LP0.1.87: register stat L =>, ?:pred[pair[T1, T2]],pair[T1, T2]->Bool, ?:pred[pair[T2, T1]],pair[T2, T1]->Bool .. LP0.1.88: register stat multiset /\, \/, <=>, [__,__]:T2,T1->pair[T2, T1] LP0.1.89: LP0.1.90: LP0.1.91: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.92: order * The formulas cannot be ordered using the current ordering. LP0.1.93: make immune formulas LP0.1.94: LP0.1.95: % L1: Lemmas for Transformation, Pushdown LP0.1.96: % --------------------------------------- LP0.1.97: LP0.1.98: declare variables p: pred [T1], p: pred [T2], q: pred [T2], x: T1, y: T2, r: pred [pair [T1, T2]], f: fun [pair [T1, T2], U], f, g: fun [T2, T2], A: bag [T1], B: bag [T2] .. LP0.1.99: LP0.1.100: % ---------------------------------------------------------- LP0.1.101: set immunity on The immunity is now `on'. LP0.1.102: set name pdLemma1 The name-prefix is now `pdLemma1'. LP0.1.103: prove C (p & q, x) = (C (p, x) & C (q, x)) Attempting to prove conjecture pdLemma1.1: C(p & q, x) = C(p, x) & C(q, x) Conjecture pdLemma1.1 [] Proved by normalization. The formulas cannot be ordered using the current ordering. LP0.1.104: qed All conjectures have been proved. LP0.1.105: % ---------------------------------------------------------- LP0.1.106: LP0.1.107: % ---------------------------------------------------------- LP0.1.108: set name pdLemma2 The name-prefix is now `pdLemma2'. LP0.1.109: prove C (p \oplus fst, x) = K (p:pred[T1] ? x) Attempting to prove conjecture pdLemma2.1: C(p \oplus fst, x) = K(p:pred[T1] ? x) Conjecture pdLemma2.1 [] Proved by normalization. The formulas cannot be ordered using the current ordering. LP0.1.110: qed All conjectures have been proved. LP0.1.111: % ---------------------------------------------------------- LP0.1.112: LP0.1.113: % ---------------------------------------------------------- LP0.1.114: set name pdLemma3 The name-prefix is now `pdLemma3'. LP0.1.115: prove C (p \oplus snd, x) = p Attempting to prove conjecture pdLemma3.1: C(p \oplus snd, x) = p Conjecture pdLemma3.1 [] Proved by normalization. The formulas cannot be ordered using the current ordering. LP0.1.116: qed All conjectures have been proved. LP0.1.117: % ---------------------------------------------------------- LP0.1.118: LP0.1.119: % ---------------------------------------------------------- LP0.1.120: set name pdLemma4 The name-prefix is now `pdLemma4'. LP0.1.121: prove iterate (p & q, f) = iterate (p, f) \circ iterate (q, id) Attempting to prove conjecture pdLemma4.1: iterate(p & q, f) = iterate(p, f) \circ iterate(q, id) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture pdLemma4.1 LP0.1.122: resume by induction on x:bag[T2] Creating subgoals for proof by structural induction on `x:bag[T2]' Basis subgoal: Subgoal 1: (iterate(p & q, f) ! {}):bag[U] = iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! {}) Induction constant: xc Induction hypothesis: pdLemma4InductHyp.1: (iterate(p & q, f) ! xc):bag[U] = iterate(p, f) ! (iterate(q, id) ! xc) Induction subgoal: Subgoal 2: (iterate(p & q, f) ! insert(t, xc)):bag[U] = iterate(p, f) ! (iterate(q, id) ! insert(t, xc)) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on x Level 2 subgoal 1 (basis step) for proof by induction on x [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on x Added hypothesis pdLemma4InductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on x LP0.1.123: resume by cases q ? t Creating subgoals for proof by cases New constants: qc, tc Case hypotheses: pdLemma4CaseHyp.1.1: qc ? tc pdLemma4CaseHyp.1.2: ~(qc ? tc) Same subgoal for all cases: (iterate(p & qc, f) ! insert(tc, xc)):bag[U] = iterate(p, f) ! (iterate(qc, id) ! insert(tc, xc)) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis pdLemma4CaseHyp.1.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for case 1 (out of 2) LP0.1.124: resume by cases p ? tc Creating subgoals for proof by cases New constant: pc Case hypotheses: pdLemma4CaseHyp.2.1: pc ? tc pdLemma4CaseHyp.2.2: ~(pc ? tc) Same subgoal for all cases: (iterate(pc & qc, f) ! insert(tc, xc)):bag[U] = iterate(pc, f) ! insert(tc, iterate(qc, id) ! xc) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis pdLemma4CaseHyp.2.1 to the system. Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis pdLemma4CaseHyp.2.2 to the system. Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for case 1 (out of 2) [] Proved by cases p ? tc. Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis pdLemma4CaseHyp.1.2 to the system. Level 3 subgoal for case 2 (out of 2): (iterate(p & qc, f) ! insert(tc, xc)):bag[U] = iterate(p, f) ! (iterate(qc, id) ! insert(tc, xc)) [] Proved by normalization. Level 2 subgoal 2 (induction step) for proof by induction on x: (iterate(p & q, f) ! insert(t, xc)):bag[U] = iterate(p, f) ! (iterate(q, id) ! insert(t, xc)) [] Proved by cases q ? t. Conjecture pdLemma4.1: iterate(p & q, f) = iterate(p, f) \circ iterate(q, id) [] Proved by structural induction on `x:bag[T2]'. The formulas cannot be ordered using the current ordering. LP0.1.125: qed All conjectures have been proved. LP0.1.126: % ---------------------------------------------------------- LP0.1.127: LP0.1.128: LP0.1.129: % ---------------------------------------------------------- LP0.1.130: set name pdLemma5 The name-prefix is now `pdLemma5'. LP0.1.131: prove iterate (q & (p:pred[T2] \oplus g:fun[T2,T2]), f \circ g) ! B = iterate (p, f:fun[T2,T2]) ! (iterate (q:pred[T2], g) ! B) .. Attempting to prove conjecture pdLemma5.1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! B):bag[T2] = iterate(p, f) ! (iterate(q, g) ! B) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture pdLemma5.1 LP0.1.132: resume by induction on B:bag[T2] Creating subgoals for proof by structural induction on `B:bag[T2]' Basis subgoal: Subgoal 1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! {}):bag[T2] = iterate(p, f) ! (iterate(q, g) ! {}) Induction constant: Bc Induction hypothesis: pdLemma5InductHyp.1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! Bc):bag[T2] = iterate(p, f) ! (iterate(q, g) ! Bc) Induction subgoal: Subgoal 2: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! insert(t, Bc)): bag[T2] = iterate(p, f) ! (iterate(q, g) ! insert(t, Bc)) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on B Level 2 subgoal 1 (basis step) for proof by induction on B [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on B Added hypothesis pdLemma5InductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on B LP0.1.133: resume by cases q ? t Creating subgoals for proof by cases New constants: qc, tc Case hypotheses: pdLemma5CaseHyp.1.1: qc ? tc pdLemma5CaseHyp.1.2: ~(qc ? tc) Same subgoal for all cases: (iterate(qc & (p:pred[T2] \oplus g), f \circ g) ! insert(tc, Bc)):bag[T2] = iterate(p, f) ! (iterate(qc, g) ! insert(tc, Bc)) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis pdLemma5CaseHyp.1.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for case 1 (out of 2) LP0.1.134: resume by cases p:pred[T2] ? (g ! tc) Creating subgoals for proof by cases New constants: pc, gc Case hypotheses: pdLemma5CaseHyp.2.1: pc ? (gc ! tc) pdLemma5CaseHyp.2.2: ~(pc ? (gc ! tc)) Same subgoal for all cases: (iterate(qc & (pc \oplus gc), f \circ gc) ! insert(tc, Bc)):bag[T2] = iterate(pc, f) ! insert(gc ! tc, iterate(qc, gc) ! Bc) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis pdLemma5CaseHyp.2.1 to the system. Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis pdLemma5CaseHyp.2.2 to the system. Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for case 1 (out of 2) [] Proved by cases p:pred[T2] ? (g ! tc). Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis pdLemma5CaseHyp.1.2 to the system. Level 3 subgoal for case 2 (out of 2): (iterate(qc & (p:pred[T2] \oplus g), f \circ g) ! insert(tc, Bc)):bag[T2] = iterate(p, f) ! (iterate(qc, g) ! insert(tc, Bc)) [] Proved by normalization. Level 2 subgoal 2 (induction step) for proof by induction on B: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! insert(t, Bc)):bag[T2] = iterate(p, f) ! (iterate(q, g) ! insert(t, Bc)) [] Proved by cases q ? t. Conjecture pdLemma5.1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! B):bag[T2] = iterate(p, f) ! (iterate(q, g) ! B) [] Proved by structural induction on `B:bag[T2]'. The formulas cannot be ordered using the current ordering. LP0.1.135: qed All conjectures have been proved. LP0.1.136: % ---------------------------------------------------------- LP0.1.137: LP0.1.138: LP0.1.139: % ---------------------------------------------------------- LP0.1.140: set name pdLemma6 The name-prefix is now `pdLemma6'. LP0.1.141: prove iterate (q & (p:pred[T2] \oplus g:fun[T2,T2]), f \circ g) ! B = iterate (p, f:fun[T2,U]) ! (iterate (q:pred[T2], g) ! B) .. Attempting to prove conjecture pdLemma6.1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! B):bag[U] = iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, g) ! B) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture pdLemma6.1 LP0.1.142: resume by induction on B:bag[T2] Creating subgoals for proof by structural induction on `B:bag[T2]' Basis subgoal: Subgoal 1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! {}):bag[U] = iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, g) ! {}) Induction constant: Bc Induction hypothesis: pdLemma6InductHyp.1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! Bc):bag[U] = iterate(p, f) ! (iterate(q, g) ! Bc) Induction subgoal: Subgoal 2: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! insert(t, Bc)): bag[U] = iterate(p, f) ! (iterate(q, g) ! insert(t, Bc)) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on B Level 2 subgoal 1 (basis step) for proof by induction on B [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on B Added hypothesis pdLemma6InductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on B LP0.1.143: resume by cases q ? t Creating subgoals for proof by cases New constants: qc, tc Case hypotheses: pdLemma6CaseHyp.1.1: qc ? tc pdLemma6CaseHyp.1.2: ~(qc ? tc) Same subgoal for all cases: (iterate(qc & (p:pred[T2] \oplus g), f \circ g) ! insert(tc, Bc)):bag[U] = iterate(p, f) ! (iterate(qc, g) ! insert(tc, Bc)) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis pdLemma6CaseHyp.1.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for case 1 (out of 2) LP0.1.144: resume by cases p:pred[T2] ? (g ! tc) Creating subgoals for proof by cases New constants: pc, gc Case hypotheses: pdLemma6CaseHyp.2.1: pc ? (gc ! tc) pdLemma6CaseHyp.2.2: ~(pc ? (gc ! tc)) Same subgoal for all cases: (iterate(qc & (pc \oplus gc), f \circ gc) ! insert(tc, Bc)):bag[U] = iterate(pc, f) ! insert(gc ! tc, iterate(qc, gc) ! Bc) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis pdLemma6CaseHyp.2.1 to the system. Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis pdLemma6CaseHyp.2.2 to the system. Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for case 1 (out of 2) [] Proved by cases p:pred[T2] ? (g ! tc). Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis pdLemma6CaseHyp.1.2 to the system. Level 3 subgoal for case 2 (out of 2): (iterate(qc & (p:pred[T2] \oplus g), f \circ g) ! insert(tc, Bc)):bag[U] = iterate(p, f) ! (iterate(qc, g) ! insert(tc, Bc)) [] Proved by normalization. Level 2 subgoal 2 (induction step) for proof by induction on B: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! insert(t, Bc)):bag[U] = iterate(p, f) ! (iterate(q, g) ! insert(t, Bc)) [] Proved by cases q ? t. Conjecture pdLemma6.1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! B):bag[U] = iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, g) ! B) [] Proved by structural induction on `B:bag[T2]'. The formulas cannot be ordered using the current ordering. LP0.1.145: qed All conjectures have been proved. LP0.1.146: % ---------------------------------------------------------- LP0.1.147: LP0.1.148: % ---------------------------------------------------------- LP0.1.149: set name pdLemma7 The name-prefix is now `pdLemma7'. LP0.1.150: prove iterate (p:pred[T2], f:fun[T2,U]) ! (iterate (q:pred[T2],id) ! B) = iterate (q, f:fun[T2,U]) ! (iterate (p, id) ! B) by induction on B:bag[T2] .. Attempting to prove conjecture pdLemma7.1: (iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! B)):bag[U] = iterate(q, f):fun[bag[T2], bag[U]] ! (iterate(p, id) ! B) Creating subgoals for proof by structural induction on `B:bag[T2]' Basis subgoal: Subgoal 1: (iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! {})): bag[U] = iterate(q, f):fun[bag[T2], bag[U]] ! (iterate(p, id) ! {}) Induction constant: Bc Induction hypothesis: pdLemma7InductHyp.1: (iterate(p, f) ! (iterate(q, id) ! Bc)):bag[U] = iterate(q, f) ! (iterate(p, id) ! Bc) Induction subgoal: Subgoal 2: (iterate(p, f) ! (iterate(q, id) ! insert(t, Bc))):bag[U] = iterate(q, f) ! (iterate(p, id) ! insert(t, Bc)) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on B Level 2 subgoal 1 (basis step) for proof by induction on B [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on B Added hypothesis pdLemma7InductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on B LP0.1.151: resume by cases q ? t Creating subgoals for proof by cases New constants: qc, tc Case hypotheses: pdLemma7CaseHyp.1.1: qc ? tc pdLemma7CaseHyp.1.2: ~(qc ? tc) Same subgoal for all cases: (iterate(p, f) ! (iterate(qc, id) ! insert(tc, Bc))):bag[U] = iterate(qc, f) ! (iterate(p, id) ! insert(tc, Bc)) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis pdLemma7CaseHyp.1.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for case 1 (out of 2) LP0.1.152: resume by cases p ? tc Creating subgoals for proof by cases New constant: pc Case hypotheses: pdLemma7CaseHyp.2.1: pc ? tc pdLemma7CaseHyp.2.2: ~(pc ? tc) Same subgoal for all cases: (iterate(pc, f) ! insert(tc, iterate(qc, id) ! Bc)):bag[U] = iterate(qc, f) ! (iterate(pc, id) ! insert(tc, Bc)) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis pdLemma7CaseHyp.2.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 4 subgoal for case 1 (out of 2) LP0.1.153: instan p by pc, q by qc, B by Bc in *Induct* Formula pdLemma7InductHyp.1 has been instantiated to formula pdLemma7InductHyp.1.1, (iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U] = iterate(qc, f) ! (iterate(pc, id) ! Bc) Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis pdLemma7CaseHyp.2.2 to the system. The formulas cannot be ordered using the current ordering. LP0.1.154: instan p by pc, q by qc, B by Bc in *Induct* Formula pdLemma7InductHyp.1 has been instantiated to formula pdLemma7InductHyp.1.1, (iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U] = iterate(qc, f) ! (iterate(pc, id) ! Bc) Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for case 1 (out of 2): (iterate(p, f) ! (iterate(qc, id) ! insert(tc, Bc))):bag[U] = iterate(qc, f) ! (iterate(p, id) ! insert(tc, Bc)) [] Proved by cases p ? tc. Attempting to prove level 3 subgoal for case 2 (out of 2): (iterate(p, f) ! (iterate(qc, id) ! insert(tc, Bc))):bag[U] = iterate(qc, f) ! (iterate(p, id) ! insert(tc, Bc)) Added hypothesis pdLemma7CaseHyp.1.2 to the system. The formulas cannot be ordered using the current ordering. LP0.1.155: resume by cases p ? tc Creating subgoals for proof by cases New constant: pc Case hypotheses: pdLemma7CaseHyp.2.1: pc ? tc pdLemma7CaseHyp.2.2: ~(pc ? tc) Same subgoal for all cases: (iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U] = iterate(qc, f) ! (iterate(pc, id) ! insert(tc, Bc)) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis pdLemma7CaseHyp.2.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 4 subgoal for case 1 (out of 2) LP0.1.156: instan p by pc, q by qc, B by Bc in *Induct* Formula pdLemma7InductHyp.1 has been instantiated to formula pdLemma7InductHyp.1.1, (iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U] = iterate(qc, f) ! (iterate(pc, id) ! Bc) Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis pdLemma7CaseHyp.2.2 to the system. The formulas cannot be ordered using the current ordering. LP0.1.157: instan p by pc, q by qc, B by Bc in *Induct* Formula pdLemma7InductHyp.1 has been instantiated to formula pdLemma7InductHyp.1.1, (iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U] = iterate(qc, f) ! (iterate(pc, id) ! Bc) Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for case 2 (out of 2): (iterate(p, f) ! (iterate(qc, id) ! insert(tc, Bc))):bag[U] = iterate(qc, f) ! (iterate(p, id) ! insert(tc, Bc)) [] Proved by cases p ? tc. Level 2 subgoal 2 (induction step) for proof by induction on B: (iterate(p, f) ! (iterate(q, id) ! insert(t, Bc))):bag[U] = iterate(q, f) ! (iterate(p, id) ! insert(t, Bc)) [] Proved by cases q ? t. Conjecture pdLemma7.1: (iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! B)):bag[U] = iterate(q, f):fun[bag[T2], bag[U]] ! (iterate(p, id) ! B) [] Proved by structural induction on `B:bag[T2]'. The formulas cannot be ordered using the current ordering. LP0.1.158: qed All conjectures have been proved. LP0.1.159: make immune formulas LP0.1.160: % ---------------------------------------------------------- LP0.1.161: LP0.1.162: % ---------------------------------------------------------- LP0.1.163: set name pdLemma8 The name-prefix is now `pdLemma8'. LP0.1.164: prove K (true) & p:pred[T2] = p Attempting to prove conjecture pdLemma8.1: K(true) & p = p Conjecture pdLemma8.1 [] Proved by normalization. The formulas cannot be ordered using the current ordering. LP0.1.165: qed All conjectures have been proved. LP0.1.166: % ---------------------------------------------------------- LP0.1.167: LP0.1.168: % ---------------------------------------------------------- LP0.1.169: set name pdLemma9 The name-prefix is now `pdLemma9'. LP0.1.170: prove K (false) & p:pred[T2] = K (false) Attempting to prove conjecture pdLemma9.1: K(false) & p = K(false) Conjecture pdLemma9.1 [] Proved by normalization. The formulas cannot be ordered using the current ordering. LP0.1.171: qed All conjectures have been proved. LP0.1.172: % ---------------------------------------------------------- LP0.1.173: LP0.1.174: % ---------------------------------------------------------- LP0.1.175: set name pdLemma10 The name-prefix is now `pdLemma10'. LP0.1.176: prove iterate (K (false), f:fun[T2,U]) ! B = {} by induction on B:bag[T2] Attempting to prove conjecture pdLemma10.1: (iterate(K(false), f) ! B):bag[U] = {} Creating subgoals for proof by structural induction on `B:bag[T2]' Basis subgoal: Subgoal 1: (iterate(K(false), f) ! {}):bag[U] = {} Induction constant: Bc Induction hypothesis: pdLemma10InductHyp.1: (iterate(K(false), f) ! Bc):bag[U] = {} Induction subgoal: Subgoal 2: (iterate(K(false), f) ! insert(t, Bc)):bag[U] = {} Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on B Level 2 subgoal 1 (basis step) for proof by induction on B [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on B Added hypothesis pdLemma10InductHyp.1 to the system. Level 2 subgoal 2 (induction step) for proof by induction on B [] Proved by normalization. Conjecture pdLemma10.1 [] Proved by structural induction on `B:bag[T2]'. The formulas cannot be ordered using the current ordering. LP0.1.177: qed All conjectures have been proved. LP0.1.178: set immunity off The immunity is now `off'. LP0.1.179: LP0.1.180: LP0.1.181: % L1: Rules Used in Transformation, Pushdown LP0.1.182: % ------------------------------------------ LP0.1.183: LP0.1.184: set name push The name-prefix is now `push'. LP0.1.185: LP0.1.186: make passive formulas LP0.1.187: 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.188: LP0.1.189: prove join ((p \oplus fst) & (q \oplus snd) & r, f) ! [A, B] = join (r, f) ! [iterate (p, id) ! A, iterate (q, id) ! B] .. Attempting to prove conjecture push.1: join((p \oplus fst) & (q \oplus snd) & r, f) ! [A, B] = join(r, f) ! [iterate(p, id) ! A, iterate(q, id) ! B] The system now contains 173 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of conjecture push.1 LP0.1.190: LP0.1.191: resume by induction on A:bag[T1] Creating subgoals for proof by structural induction on `A:bag[T1]' Basis subgoal: Subgoal 1: join((p \oplus fst) & (q \oplus snd) & r, f) ! [{}, B] = join(r, f) ! [iterate(p, id) ! {}, iterate(q, id) ! B] Induction constant: Ac Induction hypothesis: pushInductHyp.1: join((p \oplus fst) & (q \oplus snd) & r, f) ! [Ac, B] = join(r, f) ! [iterate(p, id) ! Ac, iterate(q, id) ! B] Induction subgoal: Subgoal 2: join((p \oplus fst) & (q \oplus snd) & r, f) ! [insert(t, Ac), B] = join(r, f) ! [iterate(p, id) ! insert(t, Ac), iterate(q, id) ! B] Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A Level 2 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on A Added hypothesis pushInductHyp.1 to the system. The system now contains 174 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on A LP0.1.192: LP0.1.193: % Base Case: Trivial LP0.1.194: % Inductive Case: LP0.1.195: LP0.1.196: resume by cases p ? t Creating subgoals for proof by cases New constants: pc, tc Case hypotheses: pushCaseHyp.1.1: pc ? tc pushCaseHyp.1.2: ~(pc ? tc) Same subgoal for all cases: (iterate(K(pc ? tc) & q & C(r, tc), C(f, tc)) ! B) \U (join(r, f) ! [iterate(pc, id) ! Ac, iterate(q, id) ! B]) = join(r, f) ! [iterate(pc, id) ! insert(tc, Ac), iterate(q, id) ! B] Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis pushCaseHyp.1.1 to the system. The system now contains 175 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 3 subgoal for case 1 (out of 2) LP0.1.197: LP0.1.198: % Case 1: p ? t LP0.1.199: LP0.1.200: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.201: LP0.1.202: crit-pairs *Lemma* with Composition The following equations are critical pairs between rewrite rules pdLemma4.1 and Composition.2. push.2: (iterate(p & q, f) ! x):bag[U] = iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! x) The system now contains 1 formula and 175 rewrite rules. The rewriting system is NOT guaranteed to terminate. The system now contains 176 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.203: norm conjecture Level 3 subgoal for case 1 (out of 2): (iterate(K(pc ? tc) & q & C(r, tc), C(f, tc)) ! B) \U (join(r, f) ! [iterate(pc, id) ! Ac, iterate(q, id) ! B]) = join(r, f) ! [iterate(pc, id) ! insert(tc, Ac), iterate(q, id) ! B] [] Proved by normalization. Attempting to prove level 3 subgoal for case 2 (out of 2): (iterate(K(pc ? tc) & q & C(r, tc), C(f, tc)) ! B) \U (join(r, f) ! [iterate(pc, id) ! Ac, iterate(q, id) ! B]) = join(r, f) ! [iterate(pc, id) ! insert(tc, Ac), iterate(q, id) ! B] Added hypothesis pushCaseHyp.1.2 to the system. Level 3 subgoal for case 2 (out of 2) [] Proved by normalization. Level 2 subgoal 2 (induction step) for proof by induction on A: join((p \oplus fst) & (q \oplus snd) & r, f) ! [insert(t, Ac), B] = join(r, f) ! [iterate(p, id) ! insert(t, Ac), iterate(q, id) ! B] [] Proved by cases p ? t. Conjecture push.1: join((p \oplus fst) & (q \oplus snd) & r, f) ! [A, B] = join(r, f) ! [iterate(p, id) ! A, iterate(q, id) ! B] [] Proved by structural induction on `A:bag[T1]'. The system now contains 174 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.204: LP0.1.205: % Case 2: ~ (p ? t) LP0.1.206: LP0.1.207: qed All conjectures have been proved. LP0.1.208: make immune formulas LP0.1.209: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.210: LP0.1.211: set name simp The name-prefix is now `simp'. LP0.1.212: prove iterate (K (true), id) ! A = A Attempting to prove conjecture simp.1: iterate(K(true), id) ! A = A Suspending proof of conjecture simp.1 LP0.1.213: resume by induction on A:bag[T2] Creating subgoals for proof by structural induction on `A:bag[T2]' Basis subgoal: Subgoal 1: iterate(K(true), id) ! {} = {} Induction constant: Ac Induction hypothesis: simpInductHyp.1: iterate(K(true), id) ! Ac = Ac Induction subgoal: Subgoal 2: iterate(K(true), id) ! insert(t, Ac) = insert(t, Ac) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A Level 2 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on A Added hypothesis simpInductHyp.1 to the system. Level 2 subgoal 2 (induction step) for proof by induction on A [] Proved by normalization. Conjecture simp.1 [] Proved by structural induction on `A:bag[T2]'. The system now contains 175 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.214: qed All conjectures have been proved. LP0.1.215: LP0.1.216: quit End of input from file `/pro/oodb/specs/KOLA98/pushdown-scripts.lp'. End of input from file `command line arguments'.