LP (the Larch Prover), Release 3.1a (95/04/27) logging to `/pro/oodb/specs/KOLA98/magic-scripts.lplog' on 21 June 1998 18:38:13. 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: LP0.1.42: % Section 4: SNF2 LP0.1.43: % LP0.1.44: % Proof Scripts for COKO Transformations: LP0.1.45: % LP0.1.46: % TRANSFORMATION SNF2 LP0.1.47: % USES LP0.1.48: % SimpLits2, LP0.1.49: % CNF, LP0.1.50: % OrderConjs2, LP0.1.51: % pushneg: ~ (p OPLUS f) --> (~ (p)) OPLUS f, LP0.1.52: % init: p --> (K (true) OPLUS (id X #1)) & LP0.1.53: % (K (true) OPLUS (id X #2)) & LP0.1.54: % K (true) & p, LP0.1.55: % pull: (p OPLUS f) | (q OPLUS f) --> (p | q) OPLUS f, LP0.1.56: % shift: p & (q & r) --> (p & r) & q, LP0.1.57: % simplify: K (true) & p --> p LP0.1.58: % BEGIN LP0.1.59: % SimpLits2; LP0.1.60: % CNF; LP0.1.61: % TD {pushneg}; LP0.1.62: % init; LP0.1.63: % BU {pull || {REPEAT shift}}; LP0.1.64: % OrderConjs2; LP0.1.65: % BU {simplify} LP0.1.66: % END LP0.1.67: % LP0.1.68: % TRANSFORMATION SimpLits2 LP0.1.69: % USES LP0.1.70: % SL11: --> K ([x, y]), LP0.1.71: % SL12: f o K (x) --> K (f ! x), LP0.1.72: % SL13: --> o f, LP0.1.73: % SL14: --> o f, LP0.1.74: % SL21: --> o h, LP0.1.75: % SL22: --> o (id X h), LP0.1.76: % SL23: --> o (id X h), LP0.1.77: % SL24: --> o (id X h), LP0.1.78: % SL25: --> o (id X h), LP0.1.79: % SL26: --> o #2, LP0.1.80: % SL27: --> o #2 LP0.1.81: % Shft, LP0.1.82: % Pr2Times, LP0.1.83: % PR1: p OPLUS (f o g) --> p OPLUS f OPLUS g, LP0.1.84: % PR2: p OPLUS K (x) --> K (p ? x) LP0.1.85: % BEGIN LP0.1.86: % BU {Pr2Times || LP0.1.87: % SL11 || SL12 || {{SL13 || SL14} -> Shft} || LP0.1.88: % SL21 || SL22 || SL23 || SL24 || SL25 || SL26 || SL27 || LP0.1.89: % Shft}; LP0.1.90: % BU {PR1 || PR2} LP0.1.91: % END LP0.1.92: % LP0.1.93: % TRANSFORMATION Pr2Times LP0.1.94: % USES LP0.1.95: % CO1: --> (f X g) o (id X h), LP0.1.96: % CO2: --> <#2, #1> o (g X f) o (id X h), LP0.1.97: % CO3: --> (f X g) o #2, LP0.1.98: % CO4: --> <#2, #1> o (g X f) o #2, LP0.1.99: % CO5: --> (f X id) o (id X g), LP0.1.100: % CO6: --> <#2, #1> o (g X id) o (id X f), LP0.1.101: % CO7: <#1, #2> --> id, LP0.1.102: % CO8: f o id --> f, LP0.1.103: % CO9: id o f --> f LP0.1.104: % BEGIN LP0.1.105: % CO1 || CO2 || CO3 || CO4 || CO5 || CO6 || CO7 || CO8 || CO9 LP0.1.106: % END LP0.1.107: % LP0.1.108: % TRANSFORMATION Shft LP0.1.109: % USES LP0.1.110: % SL1: f o #1 o #2 --> f o (#1 o #2), LP0.1.111: % SL2: f o #2 o #2 --> f o (#2 o #2), LP0.1.112: % SL3: f o (g o h) --> (f o g) o h LP0.1.113: % BEGIN LP0.1.114: % REPEAT SL3; LP0.1.115: % {SL1 || SL2} LP0.1.116: % END LP0.1.117: % LP0.1.118: % TRANSFORMATION OrderConjs2 LP0.1.119: % USES LP0.1.120: % OC1: (p OPLUS (id X #1)) & q & r & (r' OPLUS (id X #1)) --> LP0.1.121: % ((p & r') OPLUS (id X #1)) & q & r, LP0.1.122: % OC2: p & (q OPLUS (id X #2)) & r & (r' OPLUS (id X #2)) --> LP0.1.123: % p & ((q & r') OPLUS (id X #2)) & r, LP0.1.124: % OC3: p & q & r & r' --> p & q & (r & r') LP0.1.125: % BEGIN LP0.1.126: % BU {OC1 || OC2 || OC3} LP0.1.127: % END LP0.1.128: % LP0.1.129: % In [CZ98a], the effects of SNF2 are described but the transformations LP0.1.130: % themselves are not presented. The effect of SNF2 on any predicate, p is LP0.1.131: % to rewrite p to the form, LP0.1.132: % LP0.1.133: % (\rho OPLUS (id \times fst)) & (\sigma OPLUS (id \times snd)) & \tau LP0.1.134: % LP0.1.135: % See Section 2 for proofs of rewrite rules: LP0.1.136: % LP0.1.137: % pushneg, pull, shift, simplify (from SNF2), LP0.1.138: % SL11 (SL2 in Section 2), SL12 (SL6 in Section 2), SL13 (SL3 in Section 2), LP0.1.139: % SL14 (SL4 in Section 2), SL21 (SL1 in Section 2), PR1 (SL7 in Section 2), LP0.1.140: % and PR2 (SL8 in Section 2) (from SimpLits2), and LP0.1.141: % OC3 (from OrderConjs2) LP0.1.142: % LP0.1.143: LP0.1.144: clear LP0.1.145: forget Critical pair list cleared. LP0.1.146: unregister registry LP0.1.147: set order manual The ordering-method is now `manual'. LP0.1.148: exec-silently SNF2_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/SNF2_Aux_Axioms.lp'. LP0.1.149: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.150: order * The system now contains 170 rewrite rules. The rewriting system is guaranteed to terminate. All equations have been oriented into rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.151: LP0.1.152: % L1: Rules Used in Transformation, SNF2 LP0.1.153: % -------------------------------------- LP0.1.154: LP0.1.155: set name init The name-prefix is now `init'. LP0.1.156: declare variables p: pred [pair [T1, pair [T2, T3]]] LP0.1.157: prove p = (K (true) \oplus (id \times fst)) & (K (true) \oplus (id \times snd)) & K (true) & p .. Attempting to prove conjecture init.1: p = (K(true) \oplus (id \times fst)) & (K(true) \oplus (id \times snd)) & K(true) & p Conjecture init.1 [] Proved by normalization. Deleted formula init.1, which reduced to `true'. LP0.1.158: qed All conjectures have been proved. LP0.1.159: LP0.1.160: LP0.1.161: % L1: Rules Used in Transformation, SimpLits2 LP0.1.162: % ------------------------------------------- LP0.1.163: LP0.1.164: set name SL22 The name-prefix is now `SL22'. LP0.1.165: declare variables f: fun [T1, U], h: fun [T2, V], g: fun [pair [T1, V], W] .. LP0.1.166: prove \ = \ \circ (id \times h) .. Attempting to prove conjecture SL22.1: \ = \ \circ (id \times h) Suspending proof of conjecture SL22.1 LP0.1.167: declare operator one: pair [T1, T2] -> T1, two: pair [T1, T2] -> T2 .. LP0.1.168: set immunity on The immunity is now `on'. LP0.1.169: instan pr:pair[T1,T2] by x in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y]) Deleted rewrite rule Pairs.1, which reduced to `true'. LP0.1.170: set immunity off The immunity is now `off'. LP0.1.171: LP0.1.172: fix x:T1 as one (x:pair[T1,T2]) in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula SL22.2, \E y:T2 (x:pair[T1, T2] = [one(x), y]) The system now contains 171 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.173: LP0.1.174: fix y:T2 as two (x:pair[T1,T2]) in SL22 / contains-operator (one: pair [T1, T2] -> T1) .. A prenex-existential quantifier in formula SL22.2 has been eliminated to produce formula SL22.3, x = [one(x), two(x)] The system now contains 172 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.175: LP0.1.176: crit-pairs SL22 with ProductsF The following equations are critical pairs between rewrite rules SL22.3 and ProductsF.1. SL22.4: ((f \times g) ! x):pair[T1, V] = [f ! one(x), g ! two(x)] The system now contains 1 formula and 172 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.177: crit-pairs SL22 with Projection The following equations are critical pairs between rewrite rules SL22.3 and Projection.4. SL22.5: snd ! x = two(x) The system now contains 2 formulas and 172 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules SL22.3 and Projection.3. SL22.6: fst:fun[pair[T1, T2], T1] ! x = one(x) The system now contains 1 formula and 174 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Conjecture SL22.1: \ = \ \circ (id \times h) [] Proved by normalization. The system now contains 171 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.178: qed All conjectures have been proved. LP0.1.179: LP0.1.180: set name SL23 The name-prefix is now `SL23'. LP0.1.181: declare variables f: fun [pair [T1, V], W], h: fun [T2, V], g: fun [T1, U] .. LP0.1.182: prove \ = \ \circ (id \times h) .. Attempting to prove conjecture SL23.1: \ = \ \circ (id \times h) Conjecture SL23.1 [] Proved by normalization. Deleted formula SL23.1, which reduced to `true'. LP0.1.183: qed All conjectures have been proved. LP0.1.184: LP0.1.185: set name SL24 The name-prefix is now `SL24'. LP0.1.186: declare variables f: fun [V, W], h: fun [T2, V], g: fun [pair [T1, V], U] .. LP0.1.187: prove \ = \ \circ (id \times h) .. Attempting to prove conjecture SL24.1: \ = \ \circ (id \times h) Suspending proof of conjecture SL24.1 LP0.1.188: declare operator one: pair [T1, T2] -> T1, two: pair [T1, T2] -> T2 .. LP0.1.189: set immunity on The immunity is now `on'. LP0.1.190: instan pr:pair[T1,T2] by x in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y]) Deleted rewrite rule Pairs.1, which reduced to `true'. LP0.1.191: set immunity off The immunity is now `off'. LP0.1.192: LP0.1.193: fix x:T1 as one (x:pair[T1,T2]) in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula SL24.2, \E y:T2 (x:pair[T1, T2] = [one(x), y]) The system now contains 172 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.194: LP0.1.195: fix y:T2 as two (x:pair[T1,T2]) in SL24 / contains-operator (one: pair [T1, T2] -> T1) .. A prenex-existential quantifier in formula SL24.2 has been eliminated to produce formula SL24.3, x = [one(x), two(x)] The system now contains 173 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.196: LP0.1.197: crit-pairs SL24 with ProductsF The following equations are critical pairs between rewrite rules SL24.3 and ProductsF.1. SL24.4: ((f \times g) ! x):pair[T1, V] = [f ! one(x), g ! two(x)] The system now contains 1 formula and 173 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.198: crit-pairs SL24 with Projection The following equations are critical pairs between rewrite rules SL24.3 and Projection.4. SL24.5: snd ! x = two(x) The system now contains 2 formulas and 173 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Conjecture SL24.1: \ = \ \circ (id \times h) [] Proved by normalization. The system now contains 172 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.199: qed All conjectures have been proved. LP0.1.200: LP0.1.201: set name SL25 The name-prefix is now `SL25'. LP0.1.202: declare variables f: fun [pair [T1, V], W], h: fun [T2, V], g: fun [pair [T1, V], U] .. LP0.1.203: prove \ = \ \circ (id \times h) .. Attempting to prove conjecture SL25.1: \ = \ \circ (id \times h) Conjecture SL25.1 [] Proved by normalization. Deleted formula SL25.1, which reduced to `true'. LP0.1.204: qed All conjectures have been proved. LP0.1.205: LP0.1.206: set name SL26 The name-prefix is now `SL26'. LP0.1.207: declare variables f: fun [U, W], h: fun [T2, V], g: fun [T2, U] .. LP0.1.208: prove \ = \ \circ snd .. Attempting to prove conjecture SL26.1: \ = \ \circ snd Conjecture SL26.1 [] Proved by normalization. Deleted formula SL26.1, which reduced to `true'. LP0.1.209: qed All conjectures have been proved. LP0.1.210: LP0.1.211: set name SL27 The name-prefix is now `SL27'. LP0.1.212: declare variables f: fun [T2, W], h: fun [U, V], g: fun [T2, U] .. LP0.1.213: prove \ = \ \circ snd .. Attempting to prove conjecture SL27.1: \ = \ \circ snd Conjecture SL27.1 [] Proved by normalization. Deleted formula SL27.1, which reduced to `true'. LP0.1.214: qed All conjectures have been proved. LP0.1.215: LP0.1.216: LP0.1.217: LP0.1.218: % L1: Rules Used in Transformation, Pr2Times LP0.1.219: % ------------------------------------------ LP0.1.220: LP0.1.221: set name CO1 The name-prefix is now `CO1'. LP0.1.222: declare variables f: fun [T1, U], h: fun [T2, V], g: fun [V, W] .. LP0.1.223: prove \ = (f \times g) \circ (id \times h) .. Attempting to prove conjecture CO1.1: \ = (f \times g) \circ (id \times h) Suspending proof of conjecture CO1.1 LP0.1.224: declare operator one: pair [T1, T2] -> T1, two: pair [T1, T2] -> T2 .. LP0.1.225: set immunity on The immunity is now `on'. LP0.1.226: instan pr:pair[T1,T2] by x in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y]) Deleted rewrite rule Pairs.1, which reduced to `true'. LP0.1.227: set immunity off The immunity is now `off'. LP0.1.228: LP0.1.229: fix x:T1 as one (x:pair[T1,T2]) in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula CO1.2, \E y:T2 (x:pair[T1, T2] = [one(x), y]) The system now contains 173 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.230: LP0.1.231: fix y:T2 as two (x:pair[T1,T2]) in CO1 / contains-operator (one: pair [T1, T2] -> T1) .. A prenex-existential quantifier in formula CO1.2 has been eliminated to produce formula CO1.3, x = [one(x), two(x)] The system now contains 174 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.232: LP0.1.233: crit-pairs CO1 with ProductsF The following equations are critical pairs between rewrite rules CO1.3 and ProductsF.1. CO1.4: ((f \times g) ! x):pair[T1, V] = [f ! one(x), g ! two(x)] The system now contains 1 formula and 174 rewrite rules. The rewriting system is guaranteed to terminate. Deduction rule lp_and_is_true has been applied to formula ProductsF.1 to yield the following formulas, which imply ProductsF.1. ProductsF.1.1: (f:fun[T1, T1] ! x):T1 = f ! one([x, y]) ProductsF.1.2: (g:fun[T2, V] ! y):V = g ! two([x, y]) Critical pair computation abandoned because a theorem has been proved. Conjecture CO1.1: \ = (f \times g) \circ (id \times h) [] Proved by normalization. The system now contains 173 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.234: qed All conjectures have been proved. LP0.1.235: LP0.1.236: set name CO2 The name-prefix is now `CO2'. LP0.1.237: declare variables f: fun [V, W], h: fun [T2, V], g: fun [T1, U] .. LP0.1.238: prove \ = \ \circ (g \times f) \circ (id \times h) .. Attempting to prove conjecture CO2.1: \ = \ \circ (g \times f) \circ (id \times h) Conjecture CO2.1 [] Proved by normalization. Deleted formula CO2.1, which reduced to `true'. LP0.1.239: qed All conjectures have been proved. LP0.1.240: LP0.1.241: set name CO3 The name-prefix is now `CO3'. LP0.1.242: declare variables f: fun [T2, V], g: fun [T4, U] .. LP0.1.243: prove \ = (f:fun [T2, V] \times g:fun [T4, U]) \circ snd .. Attempting to prove conjecture CO3.1: \ = (f \times g) \circ snd Suspending proof of conjecture CO3.1 LP0.1.244: declare operator one: pair [pair [T1, T3], pair[T2, T4]] -> pair[T1, T3], two: pair [pair [T1, T3], pair[T2, T4]] -> pair[T2, T4], one: pair [T1, T3] -> T1, two: pair [T1, T3] -> T3, one: pair [T2, T4] -> T2, two: pair [T2, T4] -> T4 .. LP0.1.245: set immunity on The immunity is now `on'. LP0.1.246: instan pr:pair [pair [T1, T3], pair[T2, T4]] by x in Pairs / contains-oper (=:pair [pair [T1,T3], pair[T2,T4]], pair [pair [T1,T3], pair[T2,T4]] -> Bool) .. Formula Pairs.13 has been instantiated to formula Pairs.13.1, \E x:pair[T1, T3] \E y:pair[T2, T4] (x:pair[pair[T1, T3], pair[T2, T4]] = [x, y]) Deleted rewrite rule Pairs.13, which reduced to `true'. LP0.1.247: set immunity off The immunity is now `off'. LP0.1.248: fix x as one (x:pair [pair [T1, T3], pair[T2, T4]]) in Pairs / contains-oper (=:pair [pair [T1,T3], pair[T2,T4]], pair [pair [T1,T3], pair[T2,T4]] -> Bool) .. A prenex-existential quantifier in formula Pairs.13.1 has been eliminated to produce formula CO3.2, \E y:pair[T2, T4] (x:pair[pair[T1, T3], pair[T2, T4]] = [one(x), y]) The system now contains 174 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.249: fix y as two (x:pair [pair [T1, T3], pair[T2, T4]]) in CO3 / contains-oper (one: pair [pair [T1,T3], pair[T2,T4]] -> pair [T1,T3]) .. A prenex-existential quantifier in formula CO3.2 has been eliminated to produce formula CO3.3, x:pair[pair[T1, T3], pair[T2, T4]] = [one(x), two(x)] The system now contains 175 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.250: LP0.1.251: set immunity on The immunity is now `on'. LP0.1.252: instan pr:pair[T1,T3] by x in Pairs / contains-operator (=:pair[T1,T3],pair[T1,T3]->Bool) .. Formula Pairs.5 has been instantiated to formula Pairs.5.1, \E x:T1 \E y:T3 (x:pair[T1, T3] = [x, y]) Deleted rewrite rule Pairs.5, which reduced to `true'. LP0.1.253: set immunity off The immunity is now `off'. LP0.1.254: LP0.1.255: fix x:T1 as one (x:pair[T1,T3]) in Pairs / contains-operator (=:pair[T1, T3],pair[T1, T3]->Bool) .. A prenex-existential quantifier in formula Pairs.5.1 has been eliminated to produce formula CO3.4, \E y:T3 (x:pair[T1, T3] = [one(x), y]) The system now contains 176 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.256: LP0.1.257: fix y as two (x:pair[T1,T3]) in CO3 / contains-operator (one: pair [T1, T3] -> T1) .. A prenex-existential quantifier in formula CO3.4 has been eliminated to produce formula CO3.5, x:pair[T1, T3] = [one(x), two(x)] The system now contains 177 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.258: LP0.1.259: set immunity on The immunity is now `on'. LP0.1.260: instan pr:pair[T2,T4] by x in Pairs / contains-operator (=:pair[T2,T4],pair[T2,T4]->Bool) .. Formula Pairs.7 has been instantiated to formula Pairs.7.1, \E x:T2 \E y:T4 (x:pair[T2, T4] = [x, y]) Deleted rewrite rule Pairs.7, which reduced to `true'. LP0.1.261: set immunity off The immunity is now `off'. LP0.1.262: LP0.1.263: fix x:T2 as one (x:pair[T2,T4]) in Pairs / contains-operator (=:pair[T2, T4],pair[T2, T4]->Bool) .. A prenex-existential quantifier in formula Pairs.7.1 has been eliminated to produce formula CO3.6, \E y:T4 (x:pair[T2, T4] = [one(x), y]) The system now contains 178 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.264: LP0.1.265: fix y:T4 as two (x:pair[T2,T4]) in CO3 / contains-operator (one: pair [T2, T4] -> T2) .. A prenex-existential quantifier in formula CO3.6 has been eliminated to produce formula CO3.7, x:pair[T2, T4] = [one(x), two(x)] The system now contains 179 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.266: LP0.1.267: crit-pairs CO3 with Projection The following equations are critical pairs between rewrite rules CO3.3 and Projection.16. CO3.8: (snd ! x):pair[T2, T4] = two(x) The system now contains 1 formula and 179 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules CO3.3 and Projection.15. CO3.9: (fst ! x):pair[T1, T3] = one(x) The system now contains 1 formula and 180 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules CO3.7 and Projection.8. CO3.10: (snd ! x):T4 = two(x) The system now contains 1 formula and 181 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules CO3.7 and Projection.7. CO3.11: (fst:fun[pair[T2, T4], T2] ! x):T2 = one(x) The system now contains 1 formula and 182 rewrite rules. The rewriting system is guaranteed to terminate. The system now contains 183 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.268: crit-pairs CO3 with ProductsF The following equations are critical pairs between rewrite rules CO3.7 and ProductsF.2. CO3.12: ((f \times g) ! x):pair[V, U] = [f ! one(x), g ! two(x)] The system now contains 1 formula and 183 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Conjecture CO3.1: \ = (f \times g) \circ snd [] Proved by normalization. The system now contains 174 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.269: qed All conjectures have been proved. LP0.1.270: LP0.1.271: LP0.1.272: set name CO4 The name-prefix is now `CO4'. LP0.1.273: declare variables g: fun [T2, V], f: fun [T4, U] .. LP0.1.274: prove \ = \ \circ (g:fun [T2, V] \times f:fun [T4, U]) \circ snd .. Attempting to prove conjecture CO4.1: \ = \ \circ (g \times f) \circ snd Conjecture CO4.1 [] Proved by normalization. Deleted formula CO4.1, which reduced to `true'. LP0.1.275: qed All conjectures have been proved. LP0.1.276: LP0.1.277: set name CO5 The name-prefix is now `CO5'. LP0.1.278: declare variables g: fun [T2, V], f: fun [T1, U] .. LP0.1.279: prove \ = (f \times id) \circ (id \times g) Attempting to prove conjecture CO5.1: \ = (f \times id) \circ (id \times g) Suspending proof of conjecture CO5.1 LP0.1.280: declare operator one: pair [T1, T2] -> T1, two: pair [T1, T2] -> T2 .. LP0.1.281: set immunity on The immunity is now `on'. LP0.1.282: instan pr:pair[T1,T2] by x in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y]) Deleted rewrite rule Pairs.1, which reduced to `true'. LP0.1.283: set immunity off The immunity is now `off'. LP0.1.284: LP0.1.285: fix x:T1 as one (x:pair[T1,T2]) in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula CO5.2, \E y:T2 (x:pair[T1, T2] = [one(x), y]) The system now contains 175 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.286: LP0.1.287: fix y:T2 as two (x:pair[T1,T2]) in CO5 / contains-operator (one: pair [T1, T2] -> T1) .. A prenex-existential quantifier in formula CO5.2 has been eliminated to produce formula CO5.3, x = [one(x), two(x)] The system now contains 176 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.288: LP0.1.289: crit-pairs CO5 with ProductsF The following equations are critical pairs between rewrite rules CO5.3 and ProductsF.1. CO5.4: ((f \times g) ! x):pair[T1, V] = [f ! one(x), g ! two(x)] The system now contains 1 formula and 176 rewrite rules. The rewriting system is guaranteed to terminate. Deduction rule lp_and_is_true has been applied to formula ProductsF.1 to yield the following formulas, which imply ProductsF.1. ProductsF.1.1: (f:fun[T1, T1] ! x):T1 = f ! one([x, y]) ProductsF.1.2: (g:fun[T2, V] ! y):V = g ! two([x, y]) Deleted formula CO1.1, which reduced to `true'. The system now contains 177 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.290: crit-pairs CO5 with Projection The following equations are critical pairs between rewrite rules CO5.3 and Projection.4. CO5.5: snd ! x = two(x) The system now contains 1 formula and 177 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Conjecture CO5.1: \ = (f \times id) \circ (id \times g) [] Proved by normalization. The system now contains 175 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.291: qed All conjectures have been proved. LP0.1.292: LP0.1.293: set name CO6 The name-prefix is now `CO6'. LP0.1.294: declare variables f: fun [T2, V], g: fun [T1, U] .. LP0.1.295: prove \ = \ \circ (g \times id) \circ (id \times f) .. Attempting to prove conjecture CO6.1: \ = \ \circ (g \times id) \circ (id \times f) Conjecture CO6.1 [] Proved by normalization. Deleted formula CO6.1, which reduced to `true'. LP0.1.296: qed All conjectures have been proved. LP0.1.297: LP0.1.298: set name CO7 The name-prefix is now `CO7'. LP0.1.299: prove \ = id Attempting to prove conjecture CO7.1: \ = id Suspending proof of conjecture CO7.1 LP0.1.300: declare operator one: pair [T1, T2] -> T1, two: pair [T1, T2] -> T2 .. LP0.1.301: set immunity on The immunity is now `on'. LP0.1.302: instan pr:pair[T1,T2] by x in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. Formula Pairs.1 has been instantiated to formula Pairs.1.1, \E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y]) Deleted rewrite rule Pairs.1, which reduced to `true'. LP0.1.303: set immunity off The immunity is now `off'. LP0.1.304: fix x:T1 as one (x:pair[T1,T2]) in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool) .. A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to produce formula CO7.2, \E y:T2 (x:pair[T1, T2] = [one(x), y]) The system now contains 176 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.305: fix y:T2 as two (x:pair[T1,T2]) in CO7 / contains-operator (one: pair [T1, T2] -> T1) .. A prenex-existential quantifier in formula CO7.2 has been eliminated to produce formula CO7.3, x = [one(x), two(x)] The system now contains 177 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.306: crit-pairs CO7 with Projection The following equations are critical pairs between rewrite rules CO7.3 and Projection.4. CO7.4: snd ! x = two(x) The system now contains 1 formula and 177 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules CO7.3 and Projection.3. CO7.5: fst:fun[pair[T1, T2], T1] ! x = one(x) The system now contains 1 formula and 178 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Conjecture CO7.1: \ = id [] Proved by normalization. The system now contains 176 rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.307: qed All conjectures have been proved. LP0.1.308: LP0.1.309: set name CO8 The name-prefix is now `CO8'. LP0.1.310: declare variables f: fun [T2, V] LP0.1.311: prove f \circ id = f Attempting to prove conjecture CO8.1: f \circ id = f Conjecture CO8.1 [] Proved by normalization. Deleted formula CO8.1, which reduced to `true'. LP0.1.312: qed All conjectures have been proved. LP0.1.313: LP0.1.314: set name CO9 The name-prefix is now `CO9'. LP0.1.315: declare variables f: fun [T2, V] LP0.1.316: prove id \circ f = f Attempting to prove conjecture CO9.1: id \circ f = f Conjecture CO9.1 [] Proved by normalization. Deleted formula CO9.1, which reduced to `true'. LP0.1.317: qed All conjectures have been proved. LP0.1.318: LP0.1.319: LP0.1.320: % L1: Rules Used in Transformation, Shft LP0.1.321: % -------------------------------------- LP0.1.322: LP0.1.323: set name SL1 The name-prefix is now `SL1'. LP0.1.324: declare variables f: fun [T2, V] .. LP0.1.325: prove f \circ fst \circ snd = f \circ (fst \circ snd) Attempting to prove conjecture SL1.1: f \circ fst \circ snd = f \circ (fst \circ snd) Conjecture SL1.1 [] Proved by normalization. Deleted formula SL1.1, which reduced to `true'. LP0.1.326: qed All conjectures have been proved. LP0.1.327: LP0.1.328: set name SL2 The name-prefix is now `SL2'. LP0.1.329: declare variables f: fun [T4, V] .. LP0.1.330: prove f \circ snd \circ snd = f \circ (snd \circ snd) Attempting to prove conjecture SL2.1: f \circ snd \circ snd = f \circ (snd \circ snd) Conjecture SL2.1 [] Proved by normalization. Deleted formula SL2.1, which reduced to `true'. LP0.1.331: qed All conjectures have been proved. LP0.1.332: LP0.1.333: set name SL3 The name-prefix is now `SL3'. LP0.1.334: declare variables h: fun [T2, U], g: fun [U, V], f: fun [V, W] .. LP0.1.335: prove f \circ (g:fun [U, V] \circ h) = (f \circ g) \circ h Attempting to prove conjecture SL3.1: f \circ (g:fun[U, V] \circ h) = f \circ g \circ h Conjecture SL3.1 [] Proved by normalization. Deleted formula SL3.1, which reduced to `true'. LP0.1.336: qed All conjectures have been proved. LP0.1.337: LP0.1.338: LP0.1.339: % L1: Rules Used in Transformation, OrderConjs2 LP0.1.340: % --------------------------------------------- LP0.1.341: LP0.1.342: set name OC1 The name-prefix is now `OC1'. LP0.1.343: declare variables p, r': pred [pair [T1, T2]], q, r: pred [pair [T1, pair [T2, T3]]] .. LP0.1.344: prove (p \oplus (id \times fst)) & q & r & (r' \oplus (id \times fst)) = ((p & r') \oplus (id \times fst)) & q & r .. Attempting to prove conjecture OC1.1: (p \oplus (id \times fst)) & q & r & (r' \oplus (id \times fst)) = ((p & r') \oplus (id \times fst)) & q & r Conjecture OC1.1 [] Proved by normalization. Deleted formula OC1.1, which reduced to `true'. LP0.1.345: qed All conjectures have been proved. LP0.1.346: LP0.1.347: set name OC2 The name-prefix is now `OC2'. LP0.1.348: declare variables q, r': pred [pair [T1, T3]], p, r: pred [pair [T1, pair [T2, T3]]] .. LP0.1.349: prove p & (q \oplus (id \times snd)) & r & (r' \oplus (id \times snd)) = p & ((q & r') \oplus (id \times snd)) & r .. Attempting to prove conjecture OC2.1: p & (q \oplus (id \times snd)) & r & (r' \oplus (id \times snd)) = p & ((q & r') \oplus (id \times snd)) & r Conjecture OC2.1 [] Proved by normalization. Deleted formula OC2.1, which reduced to `true'. LP0.1.350: qed All conjectures have been proved. LP0.1.351: LP0.1.352: LP0.1.353: % Section 5: Magic LP0.1.354: % LP0.1.355: % Proof Scripts for COKO Transformation, LP0.1.356: % LP0.1.357: % TRANSFORMATION Magic LP0.1.358: % USES LP0.1.359: % SNF2, LP0.1.360: % Pushdown, LP0.1.361: % SimplifyJoin, LP0.1.362: % shift: p & q & r --> p & (q & r), LP0.1.363: % nod: njoin (p, f, g) ! [set ! A, B] --> njoin (p, f, g) ! [A, B], LP0.1.364: % LP0.1.365: % magic: join (q OPLUS (id X #1) & r, f) ! LP0.1.366: % [A, njoin (p, g, h) ! [A', B]] --> LP0.1.367: % join (q OPLUS (id X #1) & r, f) ! LP0.1.368: % [A, njoin (p, g, h) ! [set ! (join (q, #2) ! [A, A']), B]] LP0.1.369: % LP0.1.370: % BEGIN LP0.1.371: % Pushdown; LP0.1.372: % LP0.1.373: % GIVEN join (p, _F) ! _O DO { LP0.1.374: % SNF2 (p); LP0.1.375: % shift (p); LP0.1.376: % magic LP0.1.377: % }; LP0.1.378: % LP0.1.379: % GIVEN _F ! [_O, A], A = _F ! [B, _O] DO { LP0.1.380: % SimplifyJoin (B); LP0.1.381: % nod (A) LP0.1.382: % } LP0.1.383: % LP0.1.384: % END LP0.1.385: % LP0.1.386: % In [CZ98a], only rule magic is described. LP0.1.387: % LP0.1.388: LP0.1.389: clear LP0.1.390: forget Critical pair list cleared. LP0.1.391: unregister registry LP0.1.392: set order manual The ordering-method is now `manual'. LP0.1.393: exec-silently Magic_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/Magic_Aux_Axioms.lp'. LP0.1.394: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.395: order * The formulas cannot be ordered using the current ordering. LP0.1.396: LP0.1.397: % L1: Lemmas for Transformation, Magic LP0.1.398: % ------------------------------------ LP0.1.399: LP0.1.400: set name magicLemma1 The name-prefix is now `magicLemma1'. LP0.1.401: LP0.1.402: declare variables q: pred [pair [W, pair [T1, V]]], f: fun [pair [W, pair [T1, V]], X], A, B: bag [pair [W, pair [T1, V]]] .. LP0.1.403: prove iterate (p, f:fun [pair [W, pair [T1, V]], X]) ! (A \U B) = (iterate (p, f:fun [pair [W, pair [T1, V]], X]) ! A) \U (iterate (p, f:fun [pair [W, pair [T1, V]], X]) ! B) .. Attempting to prove conjecture magicLemma1.1: (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (A \U B)):bag[X] = (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! A) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture magicLemma1.1 LP0.1.404: LP0.1.405: resume by induction on A: bag [pair [W, pair [T1, V]]] Creating subgoals for proof by structural induction on `A:bag[pair[W, pair[T1, V]]]' Basis subgoal: Subgoal 1: (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! ({} \U B)): bag[X] = (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! {}) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) Induction constant: Ac Induction hypothesis: magicLemma1InductHyp.1: iterate(p, f) ! (Ac \U B) = (iterate(p, f) ! Ac) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) Induction subgoal: Subgoal 2: iterate(p, f) ! (insert(p1, Ac) \U B) = (iterate(p, f) ! insert(p1, Ac)) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A Level 2 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on A Added hypothesis magicLemma1InductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on A LP0.1.406: LP0.1.407: % Base Case: Trivial LP0.1.408: % Inductive Case LP0.1.409: resume by cases p ? p1 Creating subgoals for proof by cases New constants: pc, p1c Case hypotheses: magicLemma1CaseHyp.1.1: pc ? p1c magicLemma1CaseHyp.1.2: ~(pc ? p1c) Same subgoal for all cases: iterate(pc, f) ! insert(p1c, Ac \U B) = (iterate(pc, f) ! insert(p1c, Ac)) \U (iterate(pc, f) ! B) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis magicLemma1CaseHyp.1.1 to the system. Level 3 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis magicLemma1CaseHyp.1.2 to the system. Level 3 subgoal for case 2 (out of 2) [] Proved by normalization. Level 2 subgoal 2 (induction step) for proof by induction on A: iterate(p, f) ! (insert(p1, Ac) \U B) = (iterate(p, f) ! insert(p1, Ac)) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) [] Proved by cases p ? p1. Conjecture magicLemma1.1: (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (A \U B)):bag[X] = (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! A) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) [] Proved by structural induction on `A:bag[pair[W, pair[T1, V]]]'. The formulas cannot be ordered using the current ordering. LP0.1.410: LP0.1.411: qed All conjectures have been proved. LP0.1.412: % ---------------------------------------------------------- LP0.1.413: LP0.1.414: % ---------------------------------------------------------- LP0.1.415: set name magicLemma2 The name-prefix is now `magicLemma2'. LP0.1.416: set immunity on The immunity is now `on'. LP0.1.417: declare variables p, q: pred [pair [W, pair [T1, V]]], x: W .. LP0.1.418: prove C (p & q, x) = (C (p, x:W) & C (q, x:W)) Attempting to prove conjecture magicLemma2.1: C(p & q, x) = C(p, x) & C(q, x) Conjecture magicLemma2.1 [] Proved by normalization. The formulas cannot be ordered using the current ordering. LP0.1.419: set immunity off The immunity is now `off'. LP0.1.420: qed All conjectures have been proved. LP0.1.421: % ---------------------------------------------------------- LP0.1.422: LP0.1.423: % ---------------------------------------------------------- LP0.1.424: set name magicLemma3 The name-prefix is now `magicLemma3'. LP0.1.425: LP0.1.426: declare variables q: pred [pair [T1, V]], g: fun [pair [T1, V], pair [W, pair [T1, V]]], p: pred [pair [W, pair [T1, V]]], f: fun [pair [W, pair [T1, V]], X], A: bag [pair [T1, V]] .. LP0.1.427: prove iterate (p, f:fun [pair [W, pair [T1, V]], X]) ! (iterate (q, g:fun [pair [T1, V], pair [W, pair [T1, V]]]) ! A) = iterate (q & (p:pred [pair [W, pair [T1, V]]] \oplus g), f \circ g) ! A .. Attempting to prove conjecture magicLemma3.1: iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (iterate(q, g):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]] ! A) = iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! A The formulas cannot be ordered using the current ordering. Suspending proof of conjecture magicLemma3.1 LP0.1.428: LP0.1.429: resume by induction on A:bag [pair [T1, V]] Creating subgoals for proof by structural induction on `A:bag[pair[T1, V]]' Basis subgoal: Subgoal 1: iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (iterate(q, g):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]] ! {}) = iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! {} Induction constant: Ac Induction hypothesis: magicLemma3InductHyp.1: iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (iterate(q, g) ! Ac) = iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! Ac Induction subgoal: Subgoal 2: iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (iterate(q, g) ! insert(p1, Ac)) = iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! insert(p1, Ac) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A Level 2 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on A Added hypothesis magicLemma3InductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on A LP0.1.430: LP0.1.431: % Base Case: Trivial LP0.1.432: % Inductive Case LP0.1.433: LP0.1.434: resume by cases (q & (p \oplus g:fun [pair [T1, V], pair [W, pair [T1, V]]])) ? p1 .. Creating subgoals for proof by cases New constants: qc, pc, gc, p1c Case hypotheses: magicLemma3CaseHyp.1.1: (qc & (pc \oplus gc)) ? p1c magicLemma3CaseHyp.1.2: ~((qc & (pc \oplus gc)) ? p1c) Same subgoal for all cases: iterate(pc, f) ! (iterate(qc, gc) ! insert(p1c, Ac)) = iterate(qc & (pc \oplus gc), f \circ gc) ! insert(p1c, Ac) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis magicLemma3CaseHyp.1.1 to the system. Deduction rule lp_and_is_true has been applied to formula magicLemma3CaseHyp.1.1 to yield the following formulas, which imply magicLemma3CaseHyp.1.1. magicLemma3CaseHyp.1.1.1: qc ? p1c magicLemma3CaseHyp.1.1.2: pc ? (gc ! p1c) Level 3 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis magicLemma3CaseHyp.1.2 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal for case 2 (out of 2) LP0.1.435: LP0.1.436: % Case 1: Trivial LP0.1.437: % Case 2: LP0.1.438: resume by cases qc ? p1c Creating subgoals for proof by cases Case hypotheses: magicLemma3CaseHyp.2.1: qc ? p1c magicLemma3CaseHyp.2.2: ~(qc ? p1c) Same subgoal for all cases: iterate(pc, f) ! (iterate(qc, gc) ! insert(p1c, Ac)) = iterate(qc & (pc \oplus gc), f \circ gc) ! Ac Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis magicLemma3CaseHyp.2.1 to the system. Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis magicLemma3CaseHyp.2.2 to the system. Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for case 2 (out of 2): iterate(pc, f) ! (iterate(qc, gc) ! insert(p1c, Ac)) = iterate(qc & (pc \oplus gc), f \circ gc) ! insert(p1c, Ac) [] Proved by cases qc ? p1c. Level 2 subgoal 2 (induction step) for proof by induction on A: iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (iterate(q, g) ! insert(p1, Ac)) = iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! insert(p1, Ac) [] Proved by cases (q & (p:pred[pair[W, pair[T1, V]]] \oplus g)) ? p1. Conjecture magicLemma3.1: iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (iterate(q, g):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]] ! A) = iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! A [] Proved by structural induction on `A:bag[pair[T1, V]]'. The formulas cannot be ordered using the current ordering. LP0.1.439: qed All conjectures have been proved. LP0.1.440: % ---------------------------------------------------------- LP0.1.441: LP0.1.442: LP0.1.443: % ---------------------------------------------------------- LP0.1.444: set name magicLemma4 The name-prefix is now `magicLemma4'. LP0.1.445: LP0.1.446: declare variables p, q: pred [pair [W, pair [T1, V]]], A: bag [W], B: bag [pair [T1, V]], f: fun [pair [W, pair [T1, V]], X], w: W .. LP0.1.447: LP0.1.448: set order left-to-right Warning: the rewriting system is known to terminate, but its termination cannot be verified with the `left-to-right' ordering. When another rewrite rule is added, the rewriting system will be treated as nonterminating. The ordering-method is now `left-to-right'. LP0.1.449: prove (join (p & q, f) ! [A, B]):bag[X] = iterate (q, f) ! (join (p, id) ! [A, B]) .. Attempting to prove conjecture magicLemma4.1: join(p & q, f) ! [A, B] = iterate(q, f) ! (join(p, id) ! [A, B]) The system now contains 480 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of conjecture magicLemma4.1 LP0.1.450: resume by induction on A: bag [W] Creating subgoals for proof by structural induction on `A:bag[W]' Basis subgoal: Subgoal 1: join(p & q, f) ! [{}, B] = iterate(q, f) ! (join(p, id) ! [{}, B]) Induction constant: Ac Induction hypothesis: magicLemma4InductHyp.1: join(p & q, f) ! [Ac, B] = iterate(q, f) ! (join(p, id) ! [Ac, B]) Induction subgoal: Subgoal 2: join(p & q, f) ! [insert(w, Ac), B] = iterate(q, f) ! (join(p, id) ! [insert(w, Ac), B]) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A Level 2 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on A Added hypothesis magicLemma4InductHyp.1 to the system. The system now contains 481 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on A LP0.1.451: LP0.1.452: % Base Case: Trivial LP0.1.453: % Inductive Case LP0.1.454: LP0.1.455: resume by induction on B:bag [pair [T1, V]] Creating subgoals for proof by structural induction on `B:bag[pair[T1, V]]' Basis subgoal: Subgoal 1: (iterate(C(p, w) & C(q, w), C(f, w)) ! {}) \U (iterate(q, f) ! (join(p, id) ! [Ac, {}])) = (iterate(C(p, w) & (q \oplus C(id, w)), f \circ C(id, w)) ! {}) \U (iterate(q, f) ! (join(p, id) ! [Ac, {}])) Induction constant: Bc Induction hypothesis: magicLemma4InductHyp.2: (iterate(C(p, w) & C(q, w), C(f, w)) ! Bc) \U (iterate(q, f) ! (join(p, id) ! [Ac, Bc])) = (iterate(C(p, w) & (q \oplus C(id, w)), f \circ C(id, w)) ! Bc) \U (iterate(q, f) ! (join(p, id) ! [Ac, Bc])) Induction subgoal: Subgoal 2: (iterate(C(p, w) & C(q, w), C(f, w)) ! insert(p1, Bc)) \U (iterate(q, f) ! (join(p, id) ! [Ac, insert(p1, Bc)])) = (iterate(C(p, w) & (q \oplus C(id, w)), f \circ C(id, w)) ! insert(p1, Bc)) \U (iterate(q, f) ! (join(p, id) ! [Ac, insert(p1, Bc)])) Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on B Level 3 subgoal 1 (basis step) for proof by induction on B [] Proved by normalization. Attempting to prove level 3 subgoal 2 (induction step) for proof by induction on B Added hypothesis magicLemma4InductHyp.2 to the system. The system now contains 482 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 3 subgoal 2 (induction step) for proof by induction on B LP0.1.456: LP0.1.457: % Base Case: Trivial LP0.1.458: % Inductive Case LP0.1.459: LP0.1.460: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.461: resume by cases (p & q) ? [w, p1] Creating subgoals for proof by cases New constants: pc, qc, wc, p1c Case hypotheses: magicLemma4CaseHyp.1.1: (pc & qc) ? [wc, p1c] magicLemma4CaseHyp.1.2: ~((pc & qc) ? [wc, p1c]) Same subgoal for all cases: (iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) = (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis magicLemma4CaseHyp.1.1 to the system. Deduction rule lp_and_is_true has been applied to formula magicLemma4CaseHyp.1.1 to yield the following formulas, which imply magicLemma4CaseHyp.1.1. magicLemma4CaseHyp.1.1.1: pc ? [wc, p1c] magicLemma4CaseHyp.1.1.2: qc ? [wc, p1c] The system now contains 484 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 4 subgoal for case 1 (out of 2) LP0.1.462: LP0.1.463: % Case 1 LP0.1.464: LP0.1.465: set immunity on The immunity is now `on'. LP0.1.466: prove C (qc, wc) = qc \oplus C (id, wc) Attempting to prove level 5 lemma magicLemma4.2: C(qc, wc) = qc \oplus C(id, wc) Level 5 lemma magicLemma4.2 [] Proved by normalization. Attempting to prove level 4 subgoal for case 1 (out of 2): (iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) = (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) Current subgoal: insert(f ! [wc, p1c], (iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! Bc) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc])))) = insert(f ! [wc, p1c], (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc)) ! Bc) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc])))) The system now contains 485 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 4 subgoal for case 1 (out of 2) LP0.1.467: set immunity off The immunity is now `off'. LP0.1.468: LP0.1.469: set immunity on The immunity is now `on'. LP0.1.470: prove C (f, wc) = f \circ C (id, wc) Attempting to prove level 5 lemma magicLemma4.3: C(f, wc) = f \circ C(id, wc) Level 5 lemma magicLemma4.3 [] Proved by normalization. Attempting to prove level 4 subgoal for case 1 (out of 2) Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2): (iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) = (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) Added hypothesis magicLemma4CaseHyp.1.2 to the system. The system now contains 483 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 4 subgoal for case 2 (out of 2) LP0.1.471: set immunity off The immunity is now `off'. LP0.1.472: LP0.1.473: % Case 2 LP0.1.474: LP0.1.475: set immunity on The immunity is now `on'. LP0.1.476: prove C (qc, wc) = qc \oplus C (id, wc) Attempting to prove level 5 lemma magicLemma4.2: C(qc, wc) = qc \oplus C(id, wc) Level 5 lemma magicLemma4.2 [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) The system now contains 484 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 4 subgoal for case 2 (out of 2) LP0.1.477: set immunity off The immunity is now `off'. LP0.1.478: LP0.1.479: set immunity on The immunity is now `on'. LP0.1.480: prove C (f, wc) = f \circ C (id, wc) Attempting to prove level 5 lemma magicLemma4.3: C(f, wc) = f \circ C(id, wc) Level 5 lemma magicLemma4.3 [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2): (iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) = (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc)) ! insert(p1c, Bc)) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) Current subgoal: (iterate(C(pc, wc) & (qc \oplus C(id, wc)), C(f, wc)) ! Bc) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) = (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc)) ! Bc) \U ((iterate(qc, f) ! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac)) \U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))) Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal 2 (induction step) for proof by induction on B: (iterate(C(p, w) & C(q, w), C(f, w)) ! insert(p1, Bc)) \U (iterate(q, f) ! (join(p, id) ! [Ac, insert(p1, Bc)])) = (iterate(C(p, w) & (q \oplus C(id, w)), f \circ C(id, w)) ! insert(p1, Bc)) \U (iterate(q, f) ! (join(p, id) ! [Ac, insert(p1, Bc)])) [] Proved by cases (p & q) ? [w, p1]. Level 2 subgoal 2 (induction step) for proof by induction on A: join(p & q, f) ! [insert(w, Ac), B] = iterate(q, f) ! (join(p, id) ! [insert(w, Ac), B]) [] Proved by structural induction on `B:bag[pair[T1, V]]'. Conjecture magicLemma4.1: join(p & q, f) ! [A, B] = iterate(q, f) ! (join(p, id) ! [A, B]) [] Proved by structural induction on `A:bag[W]'. The system now contains 481 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.481: set immunity off The immunity is now `off'. LP0.1.482: LP0.1.483: qed All conjectures have been proved. LP0.1.484: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.485: % ---------------------------------------------------------- LP0.1.486: LP0.1.487: % ---------------------------------------------------------- LP0.1.488: set name magicLemma5a The name-prefix is now `magicLemma5a'. LP0.1.489: declare variables p: pred [pair [W, pair [T1, V]]], A: bag [W], B: bag [pair [T1, V]], f: fun [pair [W, pair [T1, V]], pair [W, pair [T1, V]]], X, Y, Z: bag [pair [W, pair [T1, V]]] .. LP0.1.490: LP0.1.491: prove X \U Y = Y \U X by induction on X Attempting to prove conjecture magicLemma5a.1: X \U Y = Y \U X Creating subgoals for proof by structural induction on `X' Basis subgoal: Subgoal 1: {} \U Y = Y \U {} Induction constant: Xc Induction hypothesis: magicLemma5aInductHyp.1: Xc \U Y = Y \U Xc Induction subgoal: Subgoal 2: insert(p1, Xc) \U Y = Y \U insert(p1, Xc) Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on X Level 2 subgoal 1 (basis step) for proof by induction on X [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on X Added hypothesis magicLemma5aInductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on X LP0.1.492: resume by induction on Y Creating subgoals for proof by structural induction on `Y' Basis subgoal: Subgoal 1: insert(p1, Xc \U {}) = insert(p1, {} \U Xc) Induction constant: Yc Induction hypothesis: magicLemma5aInductHyp.2: insert(p1, Xc \U Yc) = insert(p1, Yc \U Xc) Induction subgoal: Subgoal 2: insert(p1, Xc \U insert(p2, Yc)) = insert(p1, insert(p2, Yc) \U Xc) Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on Y Level 3 subgoal 1 (basis step) for proof by induction on Y [] Proved by normalization. Attempting to prove level 3 subgoal 2 (induction step) for proof by induction on Y Added hypothesis magicLemma5aInductHyp.2 to the system. Normalization of the term insert(p1, Xc \U insert(p2, Yc)) = insert(p1, insert(p2, Yc) \U Xc) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to insert(p1, insert(p2, Xc \U Yc)) = insert(p2, insert(p1, Yc \U Xc)) Normalization of the term insert(p1, insert(p2, Xc \U Yc)) = insert(p2, insert(p1, Yc \U Xc)) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to insert(p2, insert(p1, Xc \U Yc)) = insert(p2, insert(p1, Yc \U Xc)) The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal 2 (induction step) for proof by induction on Y LP0.1.493: resume by contradiction Creating subgoals for proof by contradiction New constants: p2c, p1c Hypothesis: magicLemma5aContraHyp.1: ~(insert(p2c, insert(p1c, Xc \U Yc)) = insert(p2c, insert(p1c, Yc \U Xc))) Only subgoal: false Attempting to prove level 4 subgoal for proof by contradiction Added hypothesis magicLemma5aContraHyp.1 to the system. Normalization of the term ~(insert(p2c, insert(p1c, Xc \U Yc)) = insert(p2c, insert(p1c, Yc \U Xc))) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to ~(insert(p1c, insert(p2c, Xc \U Yc)) = insert(p2c, insert(p1c, Yc \U Xc))) The formulas cannot be ordered using the current ordering. Suspending proof of level 4 subgoal for proof by contradiction LP0.1.494: crit-pairs *Contra* with *Induct* The following equations are critical pairs between rewrite rules magicLemma5aContraHyp.1 and magicLemma5aInductHyp.2. magicLemma5a.2: false The system now contains 2 formulas and 483 rewrite rules. The rewriting system is NOT guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Formula magicLemma5a.2, false, is inconsistent. Level 4 subgoal for proof by contradiction [] Proved by detecting an inconsistency. Level 3 subgoal 2 (induction step) for proof by induction on Y: insert(p1, Xc \U insert(p2, Yc)) = insert(p1, insert(p2, Yc) \U Xc) [] Proved by contradiction. Level 2 subgoal 2 (induction step) for proof by induction on X: insert(p1, Xc) \U Y = Y \U insert(p1, Xc) [] Proved by structural induction on `Y'. Conjecture magicLemma5a.1: X \U Y = Y \U X [] Proved by structural induction on `X'. The formulas cannot be ordered using the current ordering. LP0.1.495: qed All conjectures have been proved. LP0.1.496: % ---------------------------------------------------------- LP0.1.497: LP0.1.498: % ---------------------------------------------------------- LP0.1.499: set name magicLemma5b The name-prefix is now `magicLemma5b'. LP0.1.500: prove X \U (Y \U Z) = (X \U Z) \U Y Attempting to prove conjecture magicLemma5b.1: X \U (Y \U Z) = X \U Z \U Y The formulas cannot be ordered using the current ordering. Suspending proof of conjecture magicLemma5b.1 LP0.1.501: resume by induction on X Creating subgoals for proof by structural induction on `X' Basis subgoal: Subgoal 1: {} \U (Y \U Z) = {} \U Z \U Y Induction constant: Xc Induction hypothesis: magicLemma5bInductHyp.1: Xc \U (Y \U Z) = Xc \U Z \U Y Induction subgoal: Subgoal 2: insert(p1, Xc) \U (Y \U Z) = insert(p1, Xc) \U Z \U Y Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on X The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 1 (basis step) for proof by induction on X LP0.1.502: resume by induction on Y Creating subgoals for proof by structural induction on `Y' Basis subgoal: Subgoal 1: {} \U Z = Z \U {} Induction constant: Yc Induction hypothesis: magicLemma5bInductHyp.1: Yc \U Z = Z \U Yc Induction subgoal: Subgoal 2: insert(p1, Yc) \U Z = Z \U insert(p1, Yc) Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on Y Level 3 subgoal 1 (basis step) for proof by induction on Y [] Proved by normalization. Attempting to prove level 3 subgoal 2 (induction step) for proof by induction on Y Added hypothesis magicLemma5bInductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal 2 (induction step) for proof by induction on Y LP0.1.503: resume by induction on Z Creating subgoals for proof by structural induction on `Z' Basis subgoal: Subgoal 1: insert(p1, Yc \U {}) = insert(p1, {} \U Yc) Induction constant: Zc Induction hypothesis: magicLemma5bInductHyp.2: insert(p1, Yc \U Zc) = insert(p1, Zc \U Yc) Induction subgoal: Subgoal 2: insert(p1, Yc \U insert(p2, Zc)) = insert(p1, insert(p2, Zc) \U Yc) Attempting to prove level 4 subgoal 1 (basis step) for proof by induction on Z Level 4 subgoal 1 (basis step) for proof by induction on Z [] Proved by normalization. Attempting to prove level 4 subgoal 2 (induction step) for proof by induction on Z Added hypothesis magicLemma5bInductHyp.2 to the system. Normalization of the term insert(p1, Yc \U insert(p2, Zc)) = insert(p1, insert(p2, Zc) \U Yc) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to insert(p1, insert(p2, Yc \U Zc)) = insert(p2, insert(p1, Zc \U Yc)) Normalization of the term insert(p1, insert(p2, Yc \U Zc)) = insert(p2, insert(p1, Zc \U Yc)) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to insert(p2, insert(p1, Yc \U Zc)) = insert(p2, insert(p1, Zc \U Yc)) The formulas cannot be ordered using the current ordering. Suspending proof of level 4 subgoal 2 (induction step) for proof by induction on Z LP0.1.504: resume by contradiction Creating subgoals for proof by contradiction New constants: p2c, p1c Hypothesis: magicLemma5bContraHyp.1: ~(insert(p2c, insert(p1c, Yc \U Zc)) = insert(p2c, insert(p1c, Zc \U Yc))) Only subgoal: false Attempting to prove level 5 subgoal for proof by contradiction Added hypothesis magicLemma5bContraHyp.1 to the system. Normalization of the term ~(insert(p2c, insert(p1c, Yc \U Zc)) = insert(p2c, insert(p1c, Zc \U Yc))) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to ~(insert(p1c, insert(p2c, Yc \U Zc)) = insert(p2c, insert(p1c, Zc \U Yc))) The formulas cannot be ordered using the current ordering. Suspending proof of level 5 subgoal for proof by contradiction LP0.1.505: crit-pairs *Contra* with *Induct* The following equations are critical pairs between rewrite rules magicLemma5bContraHyp.1 and magicLemma5bInductHyp.2. magicLemma5b.2: false The system now contains 3 formulas and 483 rewrite rules. The rewriting system is NOT guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Formula magicLemma5b.2, false, is inconsistent. Level 5 subgoal for proof by contradiction [] Proved by detecting an inconsistency. Level 4 subgoal 2 (induction step) for proof by induction on Z: insert(p1, Yc \U insert(p2, Zc)) = insert(p1, insert(p2, Zc) \U Yc) [] Proved by contradiction. Level 3 subgoal 2 (induction step) for proof by induction on Y: insert(p1, Yc) \U Z = Z \U insert(p1, Yc) [] Proved by structural induction on `Z'. Level 2 subgoal 1 (basis step) for proof by induction on X: {} \U (Y \U Z) = {} \U Z \U Y [] Proved by structural induction on `Y'. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on X: insert(p1, Xc) \U (Y \U Z) = insert(p1, Xc) \U Z \U Y Added hypothesis magicLemma5bInductHyp.1 to the system. Level 2 subgoal 2 (induction step) for proof by induction on X [] Proved by normalization. Conjecture magicLemma5b.1: X \U (Y \U Z) = X \U Z \U Y [] Proved by structural induction on `X'. The formulas cannot be ordered using the current ordering. LP0.1.506: qed All conjectures have been proved. LP0.1.507: % ---------------------------------------------------------- LP0.1.508: LP0.1.509: % ---------------------------------------------------------- LP0.1.510: set name magicLemma5c The name-prefix is now `magicLemma5c'. LP0.1.511: prove join (p, f:fun [pair [W, pair [T1, V]], pair [W, pair [T1, V]]]) ! [A, B] = join (p, f) ! [A, iterate (ex (p\inv) \oplus \, id) ! B] .. Attempting to prove conjecture magicLemma5c.1: (join(p, f) ! [A, B]):bag[pair[W, pair[T1, V]]] = join(p, f) ! [A, iterate(ex(p\inv) \oplus \, id) ! B] The formulas cannot be ordered using the current ordering. Suspending proof of conjecture magicLemma5c.1 LP0.1.512: resume by induction on A:bag [W] Creating subgoals for proof by structural induction on `A:bag[W]' Basis subgoal: Subgoal 1: (join(p, f) ! [{}, B]):bag[pair[W, pair[T1, V]]] = join(p, f) ! [{}, iterate(ex(p\inv) \oplus \, id) ! B] Induction constant: Ac Induction hypothesis: magicLemma5cInductHyp.1: (join(p, f) ! [Ac, B]):bag[pair[W, pair[T1, V]]] = join(p, f) ! [Ac, iterate(ex(p\inv) \oplus \, id) ! B] Induction subgoal: Subgoal 2: (join(p, f) ! [insert(w, Ac), B]):bag[pair[W, pair[T1, V]]] = join(p, f) ! [insert(w, Ac), iterate(ex(p\inv) \oplus \, id) ! B] Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A Level 2 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on A Added hypothesis magicLemma5cInductHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on A LP0.1.513: LP0.1.514: % Base Case LP0.1.515: % Inductive Case LP0.1.516: LP0.1.517: resume by induction on B:bag[pair [T1, V]] Creating subgoals for proof by structural induction on `B:bag[pair[T1, V]]' Basis subgoal: Subgoal 1: ((iterate(C(p, w), C(f, w)) ! {}) \U (join(p, f) ! [Ac, {}])): bag[pair[W, pair[T1, V]]] = (iterate(C(p, w), C(f, w)) ! (iterate(ex(p\inv) \oplus \, id) ! {})) \U (join(p, f) ! [Ac, iterate(ex(p\inv) \oplus \, id) ! {}]) Induction constant: Bc Induction hypothesis: magicLemma5cInductHyp.2: ((iterate(C(p, w), C(f, w)) ! Bc) \U (join(p, f) ! [Ac, Bc])): bag[pair[W, pair[T1, V]]] = (iterate(C(p, w), C(f, w)) ! (iterate(ex(p\inv) \oplus \, id) ! Bc)) \U (join(p, f) ! [Ac, iterate(ex(p\inv) \oplus \, id) ! Bc]) Induction subgoal: Subgoal 2: ((iterate(C(p, w), C(f, w)) ! insert(p1, Bc)) \U (join(p, f) ! [Ac, insert(p1, Bc)])): bag[pair[W, pair[T1, V]]] = (iterate(C(p, w), C(f, w)) ! (iterate(ex(p\inv) \oplus \, id) ! insert(p1, Bc))) \U (join(p, f) ! [Ac, iterate(ex(p\inv) \oplus \, id) ! insert(p1, Bc)]) Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on B Level 3 subgoal 1 (basis step) for proof by induction on B [] Proved by normalization. Attempting to prove level 3 subgoal 2 (induction step) for proof by induction on B Added hypothesis magicLemma5cInductHyp.2 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 3 subgoal 2 (induction step) for proof by induction on B LP0.1.518: LP0.1.519: % Base Case LP0.1.520: % Inductive Case LP0.1.521: LP0.1.522: resume by cases (ex(p\inv) \oplus \) ? p1 Creating subgoals for proof by cases New constants: pc, wc, p1c Case hypotheses: magicLemma5cCaseHyp.1.1: (ex(pc\inv) \oplus \) ? p1c magicLemma5cCaseHyp.1.2: ~((ex(pc\inv) \oplus \) ? p1c) Same subgoal for all cases: ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! (iterate(ex(pc\inv) \oplus \, id) ! insert(p1c, Bc))) \U (join(pc, f) ! [Ac, iterate(ex(pc\inv) \oplus \, id) ! insert(p1c, Bc)]) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis magicLemma5cCaseHyp.1.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 4 subgoal for case 1 (out of 2) LP0.1.523: LP0.1.524: % Case 1 LP0.1.525: LP0.1.526: resume by cases pc ? [wc, p1c] Creating subgoals for proof by cases Case hypotheses: magicLemma5cCaseHyp.2.1: pc ? [wc, p1c] magicLemma5cCaseHyp.2.2: ~(pc ? [wc, p1c]) Same subgoal for all cases: ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! insert(p1c, iterate(ex(pc\inv) \oplus \, id) ! Bc)) \U (join(pc, f) ! [Ac, iterate(ex(pc\inv) \oplus \, id) ! Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac) Attempting to prove level 5 subgoal for case 1 (out of 2) Added hypothesis magicLemma5cCaseHyp.2.1 to the system. Level 5 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 5 subgoal for case 2 (out of 2) Added hypothesis magicLemma5cCaseHyp.2.2 to the system. Level 5 subgoal for case 2 (out of 2) [] Proved by normalization. Level 4 subgoal for case 1 (out of 2): ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! (iterate(ex(pc\inv) \oplus \, id) ! insert(p1c, Bc))) \U (join(pc, f) ! [Ac, iterate(ex(pc\inv) \oplus \, id) ! insert(p1c, Bc)]) [] Proved by cases pc ? [wc, p1c]. Attempting to prove level 4 subgoal for case 2 (out of 2): ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! (iterate(ex(pc\inv) \oplus \, id) ! insert(p1c, Bc))) \U (join(pc, f) ! [Ac, iterate(ex(pc\inv) \oplus \, id) ! insert(p1c, Bc)]) Added hypothesis magicLemma5cCaseHyp.1.2 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 4 subgoal for case 2 (out of 2) LP0.1.527: LP0.1.528: % Case 2 LP0.1.529: LP0.1.530: resume by cases pc ? [wc, p1c] Creating subgoals for proof by cases Case hypotheses: magicLemma5cCaseHyp.2.1: pc ? [wc, p1c] magicLemma5cCaseHyp.2.2: ~(pc ? [wc, p1c]) Same subgoal for all cases: ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! Bc) \U (join(pc, f) ! [Ac, Bc]) Attempting to prove level 5 subgoal for case 1 (out of 2) Added hypothesis magicLemma5cCaseHyp.2.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 5 subgoal for case 1 (out of 2) LP0.1.531: % Case 1 LP0.1.532: prove \E y:W (y:W \in insert(wc, Ac) /\ (pc\inv) ? [p1c, y]) by specializing y to wc .. Attempting to prove level 6 lemma magicLemma5c.2: \E y:W (y \in insert(wc, Ac) /\ (pc\inv) ? [p1c, y]) Creating subgoals for proof by specialization Subgoal: wc \in insert(wc, Ac) /\ (pc\inv) ? [p1c, wc] Attempting to prove level 7 subgoal for proof by specialization Level 7 subgoal for proof by specialization [] Proved by normalization. Level 6 lemma magicLemma5c.2 [] Proved by specialization. Attempting to prove level 5 subgoal for case 1 (out of 2) Formula magicLemma5c.2, false, is inconsistent. Level 5 subgoal for case 1 (out of 2): ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! Bc) \U (join(pc, f) ! [Ac, Bc]) [] Proved by impossible case. Attempting to prove level 5 subgoal for case 2 (out of 2): ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! Bc) \U (join(pc, f) ! [Ac, Bc]) Added hypothesis magicLemma5cCaseHyp.2.2 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 5 subgoal for case 2 (out of 2) LP0.1.533: LP0.1.534: % Case 2 LP0.1.535: LP0.1.536: prove (iterate(C(pc\inv, p1c), C(f:fun [pair [W, pair [T1, V]], pair [W, pair [T1, V]]] \circ \, p1c)) ! Ac) = {} by contradiction .. Attempting to prove level 6 lemma magicLemma5c.2: (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac): bag[pair[W, pair[T1, V]]] = {} Creating subgoals for proof by contradiction New constant: fc Hypothesis: magicLemma5cContraHyp.1: ~(iterate(C(pc\inv, p1c), C(fc \circ \, p1c)) ! Ac = {}) Only subgoal: false Attempting to prove level 7 subgoal for proof by contradiction Added hypothesis magicLemma5cContraHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 7 subgoal for proof by contradiction LP0.1.537: LP0.1.538: crit-pairs *Contra* with Bag The following equations are critical pairs between rewrite rules magicLemma5cContraHyp.1 and Bag.49. magicLemma5c.3: \E x:pair[W, pair[T1, V]] \E B:bag[pair[W, pair[T1, V]]] (iterate(C(pc\inv, p1c), C(fc \circ \, p1c)) ! Ac = insert(x, B)) The system now contains 2 formulas and 487 rewrite rules. The rewriting system is NOT guaranteed to terminate. The system now contains 1 formula and 488 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.539: declare operator xc: -> pair [W, pair [T1, V]] LP0.1.540: declare operator Bc: -> bag [pair [W, pair [T1, V]]] LP0.1.541: fix x as xc in *Lemma* A prenex-existential quantifier in formula magicLemma5c.3 has been eliminated to produce formula magicLemma5c.4, \E B:bag[pair[W, pair[T1, V]]] (iterate(C(pc\inv, p1c), C(fc \circ \, p1c)) ! Ac = insert(xc, B)) The formulas cannot be ordered using the current ordering. LP0.1.542: fix B:bag[pair [W, pair [T1, V]]] as Bc in *Lemma* / cont-oper (xc) .. A prenex-existential quantifier in formula magicLemma5c.4 has been eliminated to produce formula magicLemma5c.5, iterate(C(pc\inv, p1c), C(fc \circ \, p1c)) ! Ac = insert(xc, Bc) Deleted formula magicLemma5cContraHyp.1, which reduced to `true'. Deleted formula magicLemma5c.4, which reduced to `true'. The formulas cannot be ordered using the current ordering. LP0.1.543: set order left The ordering-method is now `left-to-right'. LP0.1.544: crit-pairs *Lemma* / cont-op (xc) with *Iterate* Normalization of the term ((join(p, f) ! [A, B]) \U (iterate(C(p, x), C(f, x)):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]] ! B)): bag[pair[W, pair[T1, V]]] has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (iterate(C(p, x), C(f, x)):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]] ! B) \U (join(p, f) ! [A, B]) Normalization of the term ((join(p, f) ! [A, B]) \U (iterate(C((p\inv):pred[pair[pair[T1, V], W]], y), C(f \circ \, y)) ! A)): bag[pair[W, pair[T1, V]]] has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (iterate(C((p\inv):pred[pair[pair[T1, V], W]], y), C(f \circ \, y)) ! A) \U (join(p, f) ! [A, B]) Normalization of the term (B \U {}):bag[pair[W, pair[T1, V]]] = B has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to ({} \U B):bag[pair[W, pair[T1, V]]] = B Normalization of the term (B \U insert(x, A)):bag[pair[W, pair[T1, V]]] = insert(x, A \U B) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (insert(x, A) \U B):bag[pair[W, pair[T1, V]]] = insert(x, A \U B) Normalization of the term ({} \U A):bag[pair[W, pair[T1, V]]] = A has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (A \U {}):bag[pair[W, pair[T1, V]]] = A Normalization of the term (insert(y, B) \U A):bag[pair[W, pair[T1, V]]] = insert(y, A \U B) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (A \U insert(y, B)):bag[pair[W, pair[T1, V]]] = insert(y, A \U B) Normalization of the term x:pair[W, pair[T1, V]] \in (B \U A) = (x:pair[W, pair[T1, V]] \in A \/ x:pair[W, pair[T1, V]] \in B) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to x:pair[W, pair[T1, V]] \in (A \U B) = (x:pair[W, pair[T1, V]] \in A \/ x:pair[W, pair[T1, V]] \in B) Normalization of the term (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (B \U A)):bag[X] = (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! A) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (A \U B)):bag[X] = (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! A) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) Normalization of the term Y \U Z \U X = X \U Z \U Y has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to Y \U Z \U X = Y \U (X \U Z) Normalization of the term ((join(p, f) ! [Ac, iterate(ex(p\inv) \oplus \, id) ! Bc]) \U (iterate(C(p, w), C(f, w)) ! (iterate(ex(p\inv) \oplus \, id) ! Bc))): bag[pair[W, pair[T1, V]]] = (iterate(C(p, w), C(f, w)) ! Bc) \U (join(p, f) ! [Ac, Bc]) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to ((join(p, f) ! [Ac, iterate(ex(p\inv) \oplus \, id) ! Bc]) \U (iterate(C(p, w), C(f, w)) ! (iterate(ex(p\inv) \oplus \, id) ! Bc))): bag[pair[W, pair[T1, V]]] = (join(p, f) ! [Ac, Bc]) \U (iterate(C(p, w), C(f, w)) ! Bc) The following equations are critical pairs between rewrite rules magicLemma5c.5 and Iterate.33. magicLemma5c.6: (e = xc \/ e:pair[W, pair[T1, V]] \in Bc) = \E x:W (e = fc ! [x, p1c] /\ pc ? [x, p1c] /\ x \in Ac) The system now contains 490 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.545: instan e by xc in *Lemma* Formula magicLemma5c.6 has been instantiated to formula magicLemma5c.6.1, \E x:W (xc = fc ! [x, p1c] /\ pc ? [x, p1c] /\ x \in Ac) The system now contains 491 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.546: declare operator zc: -> W LP0.1.547: fix x:W as zc in *Lemma* A prenex-existential quantifier in formula magicLemma5c.6.1 has been eliminated to produce formula magicLemma5c.7, xc = fc ! [zc, p1c] /\ pc ? [zc, p1c] /\ zc \in Ac Deduction rule lp_and_is_true has been applied to formula magicLemma5c.7 to yield the following formulas, which imply magicLemma5c.7. magicLemma5c.7.1: xc = fc ! [zc, p1c] magicLemma5c.7.2: pc ? [zc, p1c] magicLemma5c.7.3: zc \in Ac The system now contains 494 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.548: crit-pairs *Lemma* with *Case* The following equations are critical pairs between rewrite rules magicLemma5c.7.3 and magicLemma5cCaseHyp.1.2. magicLemma5c.8: false The system now contains 1 formula and 494 rewrite rules. The rewriting system is NOT guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Formula magicLemma5c.8, false, is inconsistent. Level 7 subgoal for proof by contradiction: false [] Proved by detecting an inconsistency. Level 6 lemma magicLemma5c.2: (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac): bag[pair[W, pair[T1, V]]] = {} [] Proved by contradiction. Attempting to prove level 5 subgoal for case 2 (out of 2): ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! Bc) \U (join(pc, f) ! [Ac, Bc]) Current subgoal: ((iterate(C(pc, wc), C(f, wc)) ! Bc) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! Bc) \U (join(pc, f) ! [Ac, Bc]) Level 5 subgoal for case 2 (out of 2) [] Proved by normalization. Level 4 subgoal for case 2 (out of 2): ((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc)) \U (join(pc, f) ! [Ac, Bc]) \U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)): bag[pair[W, pair[T1, V]]] = (iterate(C(pc, wc), C(f, wc)) ! (iterate(ex(pc\inv) \oplus \, id) ! insert(p1c, Bc))) \U (join(pc, f) ! [Ac, iterate(ex(pc\inv) \oplus \, id) ! insert(p1c, Bc)]) [] Proved by cases pc ? [wc, p1c]. Level 3 subgoal 2 (induction step) for proof by induction on B: ((iterate(C(p, w), C(f, w)) ! insert(p1, Bc)) \U (join(p, f) ! [Ac, insert(p1, Bc)])): bag[pair[W, pair[T1, V]]] = (iterate(C(p, w), C(f, w)) ! (iterate(ex(p\inv) \oplus \, id) ! insert(p1, Bc))) \U (join(p, f) ! [Ac, iterate(ex(p\inv) \oplus \, id) ! insert(p1, Bc)]) [] Proved by cases (ex(p\inv) \oplus \) ? p1. Level 2 subgoal 2 (induction step) for proof by induction on A: (join(p, f) ! [insert(w, Ac), B]):bag[pair[W, pair[T1, V]]] = join(p, f) ! [insert(w, Ac), iterate(ex(p\inv) \oplus \, id) ! B] [] Proved by structural induction on `B:bag[pair[T1, V]]'. Conjecture magicLemma5c.1: (join(p, f) ! [A, B]):bag[pair[W, pair[T1, V]]] = join(p, f) ! [A, iterate(ex(p\inv) \oplus \, id) ! B] [] Proved by structural induction on `A:bag[W]'. The formulas cannot be ordered using the current ordering. LP0.1.549: LP0.1.550: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.551: qed All conjectures have been proved. LP0.1.552: % ---------------------------------------------------------- LP0.1.553: LP0.1.554: % ---------------------------------------------------------- LP0.1.555: set name magicLemma6 The name-prefix is now `magicLemma6'. LP0.1.556: declare variables p: pred [pair [W, T1]], f: fun [W, W], g: fun [pair [T1, V], T1] .. LP0.1.557: prove (p \oplus (f \times g)) \inv = (p\inv) \oplus (g \times f) Attempting to prove conjecture magicLemma6.1: (p \oplus (f \times g))\inv = (p\inv) \oplus (g \times f) The formulas cannot be ordered using the current ordering. Suspending proof of conjecture magicLemma6.1 LP0.1.558: LP0.1.559: declare operator uc :-> pair [T1, V] LP0.1.560: declare operator vc :-> W LP0.1.561: resume by <=> Creating subgoals for proof of <=> New constants: pc, gc, fc, xc => hypothesis: magicLemma6ImpliesHyp.1: (pc\inv) ? ((gc \times fc) ! xc) => subgoal: ((pc \oplus (fc \times gc))\inv) ? xc <= hypothesis: magicLemma6ImpliesHyp.2: ((pc \oplus (fc \times gc))\inv) ? xc <= subgoal: (pc\inv) ? ((gc \times fc) ! xc) Attempting to prove level 2 subgoal 1 for proof of <=> Added hypothesis magicLemma6ImpliesHyp.1 to the system. The formulas cannot be ordered using the current ordering. Suspending proof of level 2 subgoal 1 for proof of <=> LP0.1.562: LP0.1.563: % => LP0.1.564: LP0.1.565: set immunity on The immunity is now `on'. LP0.1.566: instan pr by xc in Pairs / contains-oper (=:pair [pair [T1, V], W], pair [pair [T1, V], W]->Bool) .. Formula Pairs.13 has been instantiated to formula Pairs.13.1, \E x:pair[T1, V] \E y:W (xc = [x, y]) The formulas cannot be ordered using the current ordering. LP0.1.567: set immunity off The immunity is now `off'. LP0.1.568: fix x:pair[T1, V] as uc in Pairs / contains-oper (xc) A prenex-existential quantifier in formula Pairs.13.1 has been eliminated to produce formula magicLemma6.2, \E y:W (xc = [uc, y]) The formulas cannot be ordered using the current ordering. LP0.1.569: fix y:W as vc in *Lemma* / contains-oper (xc) A prenex-existential quantifier in formula magicLemma6.2 has been eliminated to produce formula magicLemma6.3, xc = [uc, vc] Deleted formula magicLemma6.2, which reduced to `true'. Level 2 subgoal 1 for proof of <=>: ((pc \oplus (fc \times gc))\inv) ? xc [] Proved by normalization. Attempting to prove level 2 subgoal 2 for proof of <=>: (pc\inv) ? ((gc \times fc) ! xc) Added hypothesis magicLemma6ImpliesHyp.2 to the system. The formulas cannot be ordered using the current ordering. LP0.1.570: LP0.1.571: % <= LP0.1.572: LP0.1.573: set immunity on The immunity is now `on'. LP0.1.574: instan pr by xc in Pairs / contains-oper (=:pair [pair [T1, V], W], pair [pair [T1, V], W]->Bool) .. Formula Pairs.13 has been instantiated to formula Pairs.13.1, \E x:pair[T1, V] \E y:W (xc = [x, y]) The formulas cannot be ordered using the current ordering. LP0.1.575: set immunity off The immunity is now `off'. LP0.1.576: fix x:pair[T1, V] as uc in Pairs / contains-oper (xc) A prenex-existential quantifier in formula Pairs.13.1 has been eliminated to produce formula magicLemma6.2, \E y:W (xc = [uc, y]) The formulas cannot be ordered using the current ordering. LP0.1.577: fix y:W as vc in *Lemma* / contains-oper (xc) A prenex-existential quantifier in formula magicLemma6.2 has been eliminated to produce formula magicLemma6.3, xc = [uc, vc] Deleted formula magicLemma6.2, which reduced to `true'. Level 2 subgoal 2 for proof of <=>: (pc\inv) ? ((gc \times fc) ! xc) [] Proved by normalization. Conjecture magicLemma6.1: (p \oplus (f \times g))\inv = (p\inv) \oplus (g \times f) [] Proved <=>. The formulas cannot be ordered using the current ordering. LP0.1.578: LP0.1.579: qed All conjectures have been proved. LP0.1.580: % ---------------------------------------------------------- LP0.1.581: LP0.1.582: % ---------------------------------------------------------- LP0.1.583: set name magicLemma7 The name-prefix is now `magicLemma7'. LP0.1.584: declare variables p: pred [pair [T1, W]], g: fun [W, W], f: fun [pair [T1, V], T1] .. LP0.1.585: set order left The ordering-method is now `left-to-right'. LP0.1.586: prove ex (p \oplus (f \times g)) = ex (p \oplus (id \times g)) \oplus (f \times id) .. Attempting to prove conjecture magicLemma7.1: ex(p \oplus (f \times g)) = ex(p \oplus (id \times g)) \oplus (f \times id) Normalization of the term ((join(p, f) ! [A, B]) \U (iterate(C(p, x), C(f, x)):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]] ! B)): bag[pair[W, pair[T1, V]]] has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (iterate(C(p, x), C(f, x)):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]] ! B) \U (join(p, f) ! [A, B]) Normalization of the term ((join(p, f) ! [A, B]) \U (iterate(C((p\inv):pred[pair[pair[T1, V], W]], y), C(f \circ \, y)) ! A)): bag[pair[W, pair[T1, V]]] has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (iterate(C((p\inv):pred[pair[pair[T1, V], W]], y), C(f \circ \, y)) ! A) \U (join(p, f) ! [A, B]) Normalization of the term (B \U {}):bag[pair[W, pair[T1, V]]] = B has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to ({} \U B):bag[pair[W, pair[T1, V]]] = B Normalization of the term (B \U insert(x, A)):bag[pair[W, pair[T1, V]]] = insert(x, A \U B) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (insert(x, A) \U B):bag[pair[W, pair[T1, V]]] = insert(x, A \U B) Normalization of the term ({} \U A):bag[pair[W, pair[T1, V]]] = A has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (A \U {}):bag[pair[W, pair[T1, V]]] = A Normalization of the term (insert(y, B) \U A):bag[pair[W, pair[T1, V]]] = insert(y, A \U B) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (A \U insert(y, B)):bag[pair[W, pair[T1, V]]] = insert(y, A \U B) Normalization of the term x:pair[W, pair[T1, V]] \in (B \U A) = (x:pair[W, pair[T1, V]] \in A \/ x:pair[W, pair[T1, V]] \in B) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to x:pair[W, pair[T1, V]] \in (A \U B) = (x:pair[W, pair[T1, V]] \in A \/ x:pair[W, pair[T1, V]] \in B) Normalization of the term (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (B \U A)):bag[X] = (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! A) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (A \U B)):bag[X] = (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! A) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) Normalization of the term Y \U Z \U X = X \U Z \U Y has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to Y \U Z \U X = Y \U (X \U Z) The system now contains 485 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of conjecture magicLemma7.1: ex(p \oplus (f \times g)) = ex(p \oplus (id \times g)) \oplus (f \times id) Current subgoal: ex(p \oplus (f \times g)):pred[pair[pair[T1, V], bag[W]]] ? x <=> ex(p \oplus (id \times g)) ? ((f \times id) ! x) LP0.1.587: LP0.1.588: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.589: declare operator uc :-> pair [T1, V] LP0.1.590: declare operator vc :-> bag [W] LP0.1.591: resume by <=> Creating subgoals for proof of <=> New constants: pc, gc, fc, xc => hypothesis: magicLemma7ImpliesHyp.1: ex(pc \oplus (id \times gc)) ? ((fc \times id) ! xc) => subgoal: ex(pc \oplus (fc \times gc)) ? xc <= hypothesis: magicLemma7ImpliesHyp.2: ex(pc \oplus (fc \times gc)) ? xc <= subgoal: ex(pc \oplus (id \times gc)) ? ((fc \times id) ! xc) Attempting to prove level 2 subgoal 1 for proof of <=> Added hypothesis magicLemma7ImpliesHyp.1 to the system. The system now contains 486 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 2 subgoal 1 for proof of <=> LP0.1.592: LP0.1.593: % => LP0.1.594: LP0.1.595: set immunity on The immunity is now `on'. LP0.1.596: instan pr by xc in Pairs / contains-oper (=:pair [pair [T1, V], bag [W]], pair [pair [T1, V], bag [W]]->Bool) .. Formula Pairs.15 has been instantiated to formula Pairs.15.1, \E x:pair[T1, V] \E y:bag[W] (xc = [x, y]) The system now contains 487 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.597: set immunity off The immunity is now `off'. LP0.1.598: fix x:pair[T1, V] as uc in Pairs / contains-oper (xc) A prenex-existential quantifier in formula Pairs.15.1 has been eliminated to produce formula magicLemma7.2, \E y:bag[W] (xc = [uc, y]) The system now contains 488 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.599: fix y:bag [W] as vc in *Lemma* / contains-oper (xc) A prenex-existential quantifier in formula magicLemma7.2 has been eliminated to produce formula magicLemma7.3, xc = [uc, vc] Deleted formula magicLemma7.2, which reduced to `true'. Level 2 subgoal 1 for proof of <=>: ex(pc \oplus (fc \times gc)) ? xc [] Proved by normalization. Attempting to prove level 2 subgoal 2 for proof of <=>: ex(pc \oplus (id \times gc)) ? ((fc \times id) ! xc) Added hypothesis magicLemma7ImpliesHyp.2 to the system. The system now contains 486 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.600: LP0.1.601: % <= LP0.1.602: LP0.1.603: set immunity on The immunity is now `on'. LP0.1.604: instan pr by xc in Pairs / contains-oper (=:pair [pair [T1, V], bag [W]], pair [pair [T1, V], bag [W]]->Bool) .. Formula Pairs.15 has been instantiated to formula Pairs.15.1, \E x:pair[T1, V] \E y:bag[W] (xc = [x, y]) The system now contains 487 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.605: set immunity off The immunity is now `off'. LP0.1.606: fix x:pair[T1, V] as uc in Pairs / contains-oper (xc) A prenex-existential quantifier in formula Pairs.15.1 has been eliminated to produce formula magicLemma7.2, \E y:bag[W] (xc = [uc, y]) The system now contains 488 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.607: fix y:bag [W] as vc in *Lemma* / contains-oper (xc) A prenex-existential quantifier in formula magicLemma7.2 has been eliminated to produce formula magicLemma7.3, xc = [uc, vc] Deleted formula magicLemma7.2, which reduced to `true'. Level 2 subgoal 2 for proof of <=>: ex(pc \oplus (id \times gc)) ? ((fc \times id) ! xc) [] Proved by normalization. Conjecture magicLemma7.1: ex(p \oplus (f \times g)) = ex(p \oplus (id \times g)) \oplus (f \times id) [] Proved <=>. Normalization of the term ((join(p, f) ! [A, B]) \U (iterate(C(p, x), C(f, x)):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]] ! B)): bag[pair[W, pair[T1, V]]] has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (iterate(C(p, x), C(f, x)):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]] ! B) \U (join(p, f) ! [A, B]) Normalization of the term ((join(p, f) ! [A, B]) \U (iterate(C((p\inv):pred[pair[pair[T1, V], W]], y), C(f \circ \, y)) ! A)): bag[pair[W, pair[T1, V]]] has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (iterate(C((p\inv):pred[pair[pair[T1, V], W]], y), C(f \circ \, y)) ! A) \U (join(p, f) ! [A, B]) Normalization of the term (B \U {}):bag[pair[W, pair[T1, V]]] = B has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to ({} \U B):bag[pair[W, pair[T1, V]]] = B Normalization of the term (B \U insert(x, A)):bag[pair[W, pair[T1, V]]] = insert(x, A \U B) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (insert(x, A) \U B):bag[pair[W, pair[T1, V]]] = insert(x, A \U B) Normalization of the term ({} \U A):bag[pair[W, pair[T1, V]]] = A has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (A \U {}):bag[pair[W, pair[T1, V]]] = A Normalization of the term (insert(y, B) \U A):bag[pair[W, pair[T1, V]]] = insert(y, A \U B) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (A \U insert(y, B)):bag[pair[W, pair[T1, V]]] = insert(y, A \U B) Normalization of the term x:pair[W, pair[T1, V]] \in (B \U A) = (x:pair[W, pair[T1, V]] \in A \/ x:pair[W, pair[T1, V]] \in B) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to x:pair[W, pair[T1, V]] \in (A \U B) = (x:pair[W, pair[T1, V]] \in A \/ x:pair[W, pair[T1, V]] \in B) Normalization of the term (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (B \U A)):bag[X] = (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! A) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (A \U B)):bag[X] = (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! A) \U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B) Normalization of the term Y \U Z \U X = X \U Z \U Y has been stopped to avoid a potentially infinite rewriting loop. It has been reduced to Y \U Z \U X = Y \U (X \U Z) The system now contains 486 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.608: LP0.1.609: qed All conjectures have been proved. LP0.1.610: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.611: % ---------------------------------------------------------- LP0.1.612: LP0.1.613: % ---------------------------------------------------------- LP0.1.614: set name magicLemma8 The name-prefix is now `magicLemma8'. LP0.1.615: set order manual The ordering-method is now `manual'. LP0.1.616: declare variables p: pred [T1], A: bag [T1], B: bag [T2], q: pred [pair [T1, T2]], g: fun [T2, U], h: fun [bag [U], V] .. LP0.1.617: prove iterate (p \oplus fst, id) ! (njoin (q, g, h) ! [A, B]) = njoin (q, g, h) ! [iterate (p, id) ! A, B] .. Attempting to prove conjecture magicLemma8.1: iterate(p \oplus fst, id) ! (njoin(q, g, h) ! [A, B]) = njoin(q, g, h) ! [iterate(p, id) ! A, B] Suspending proof of conjecture magicLemma8.1 LP0.1.618: LP0.1.619: set order left-to-right The ordering-method is now `left-to-right'. LP0.1.620: resume by induction on A:bag[T1] Creating subgoals for proof by structural induction on `A:bag[T1]' Basis subgoal: Subgoal 1: iterate(p \oplus fst, id) ! (njoin(q, g, h) ! [{}, B]) = njoin(q, g, h) ! [iterate(p, id) ! {}, B] Induction constant: Ac Induction hypothesis: magicLemma8InductHyp.1: iterate(p \oplus fst, id) ! (njoin(q, g, h) ! [Ac, B]) = njoin(q, g, h) ! [iterate(p, id) ! Ac, B] Induction subgoal: Subgoal 2: iterate(p \oplus fst, id) ! (njoin(q, g, h) ! [insert(t, Ac), B]) = njoin(q, g, h) ! [iterate(p, id) ! insert(t, Ac), B] Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A Level 2 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on A Added hypothesis magicLemma8InductHyp.1 to the system. The system now contains 487 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.621: LP0.1.622: % Base Case: Trivial LP0.1.623: % Inductive Case LP0.1.624: LP0.1.625: resume by cases p ? t Creating subgoals for proof by cases New constants: pc, tc Case hypotheses: magicLemma8CaseHyp.1.1: pc ? tc magicLemma8CaseHyp.1.2: ~(pc ? tc) Same subgoal for all cases: iterate(pc \oplus fst, id) ! (njoin(q, g, h) ! [insert(tc, Ac), B]) = njoin(q, g, h) ! [iterate(pc, id) ! insert(tc, Ac), B] Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis magicLemma8CaseHyp.1.1 to the system. The system now contains 488 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 3 subgoal for case 1 (out of 2) LP0.1.626: LP0.1.627: % Case 1 LP0.1.628: resume by cases tc \in Ac Creating subgoals for proof by cases Case hypotheses: magicLemma8CaseHyp.2.1: tc \in Ac magicLemma8CaseHyp.2.2: ~(tc \in Ac) Same subgoal for all cases: iterate(pc \oplus fst, id) ! (njoin(q, g, h) ! [insert(tc, Ac), B]) = njoin(q, g, h) ! [insert(tc, iterate(pc, id) ! Ac), B] Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis magicLemma8CaseHyp.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 magicLemma8CaseHyp.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 tc \in Ac. Attempting to prove level 3 subgoal for case 2 (out of 2): iterate(pc \oplus fst, id) ! (njoin(q, g, h) ! [insert(tc, Ac), B]) = njoin(q, g, h) ! [iterate(pc, id) ! insert(tc, Ac), B] Added hypothesis magicLemma8CaseHyp.1.2 to the system. Suspending proof of level 3 subgoal for case 2 (out of 2) LP0.1.629: LP0.1.630: % Case 2 LP0.1.631: resume by cases tc \in Ac Creating subgoals for proof by cases Case hypotheses: magicLemma8CaseHyp.2.1: tc \in Ac magicLemma8CaseHyp.2.2: ~(tc \in Ac) Same subgoal for all cases: iterate(pc \oplus fst, id) ! (njoin(q, g, h) ! [insert(tc, Ac), B]) = njoin(q, g, h) ! [iterate(pc, id) ! Ac, B] Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis magicLemma8CaseHyp.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 magicLemma8CaseHyp.2.2 to the system. Level 4 subgoal for case 2 (out of 2) [] Proved by normalization. Level 3 subgoal for case 2 (out of 2) [] Proved by cases tc \in Ac. Level 2 subgoal 2 (induction step) for proof by induction on A: iterate(p \oplus fst, id) ! (njoin(q, g, h) ! [insert(t, Ac), B]) = njoin(q, g, h) ! [iterate(p, id) ! insert(t, Ac), B] [] Proved by cases p ? t. Conjecture magicLemma8.1: iterate(p \oplus fst, id) ! (njoin(q, g, h) ! [A, B]) = njoin(q, g, h) ! [iterate(p, id) ! A, B] [] Proved by structural induction on `A:bag[T1]'. The formulas cannot be ordered using the current ordering. LP0.1.632: LP0.1.633: qed All conjectures have been proved. LP0.1.634: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.635: make passive magicLemma8 LP0.1.636: % ---------------------------------------------------------- LP0.1.637: LP0.1.638: % ---------------------------------------------------------- LP0.1.639: set name magicLemma9 The name-prefix is now `magicLemma9'. LP0.1.640: set order left-to-right The ordering-method is now `left-to-right'. LP0.1.641: prove id:fun[T1,T1] \times id:fun[W,W] = id Attempting to prove conjecture magicLemma9.1: id \times id = id The system now contains 487 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of conjecture magicLemma9.1 LP0.1.642: LP0.1.643: resume by contradiction Creating subgoals for proof by contradiction New constant: xc Hypothesis: magicLemma9ContraHyp.1: ~((id \times id) ! xc = xc) Only subgoal: false Attempting to prove level 2 subgoal for proof by contradiction Added hypothesis magicLemma9ContraHyp.1 to the system. The system now contains 488 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 2 subgoal for proof by contradiction LP0.1.644: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.645: declare operators uc: -> T1 LP0.1.646: declare operators vc: -> W LP0.1.647: LP0.1.648: set immunity on The immunity is now `on'. LP0.1.649: instan pr by xc:pair[T1,W] in Pairs / contains-oper (=:pair [T1, W], pair [T1, W]->Bool) .. Formula Pairs.21 has been instantiated to formula Pairs.21.1, \E x:T1 \E y:W (xc = [x, y]) The system now contains 489 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.650: set immunity off The immunity is now `off'. LP0.1.651: fix x:T1 as uc in Pairs / contains-oper (xc) A prenex-existential quantifier in formula Pairs.21.1 has been eliminated to produce formula magicLemma9.2, \E y:W (xc = [uc, y]) The system now contains 490 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.652: fix y:W as vc in *Lemma* / contains-oper (xc) A prenex-existential quantifier in formula magicLemma9.2 has been eliminated to produce formula magicLemma9.3, xc = [uc, vc] Deleted formula magicLemma9.2, which reduced to `true'. Formula magicLemma9ContraHyp.1, false, is inconsistent. Level 2 subgoal for proof by contradiction: false [] Proved by detecting an inconsistency. Conjecture magicLemma9.1: id \times id = id [] Proved by contradiction. The system now contains 488 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.653: LP0.1.654: qed All conjectures have been proved. LP0.1.655: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.656: % ---------------------------------------------------------- LP0.1.657: LP0.1.658: % ---------------------------------------------------------- LP0.1.659: set name magicLemma10 The name-prefix is now `magicLemma10'. LP0.1.660: declare variables p: pred [pair [T1, W]] .. LP0.1.661: prove p \oplus id = p Attempting to prove conjecture magicLemma10.1: p \oplus id = p Conjecture magicLemma10.1 [] Proved by normalization. Deleted formula magicLemma10.1, which reduced to `true'. LP0.1.662: qed All conjectures have been proved. LP0.1.663: % ---------------------------------------------------------- LP0.1.664: LP0.1.665: % ---------------------------------------------------------- LP0.1.666: set name magicLemma11 The name-prefix is now `magicLemma11'. LP0.1.667: declare variables p: pred [pair [T1, bag [W]]], f: fun [pair [pair [T1, V], bag [W]], pair [T1, bag [W]]], g: fun [pair [T1, V], pair [pair [T1, V], bag [W]]] .. LP0.1.668: prove p \oplus f \oplus g:fun [pair [T1, V], pair [pair [T1, V], bag [W]]] = p \oplus (f:fun [pair [pair [T1, V], bag [W]], pair [T1, bag [W]]] \circ g) .. Attempting to prove conjecture magicLemma11.1: (p \oplus f):pred[pair[pair[T1, V], bag[W]]] \oplus g = p:pred[pair[T1, bag[W]]] \oplus (f:fun[pair[pair[T1, V], bag[W]], pair[T1, bag[W]]] \circ g) Conjecture magicLemma11.1 [] Proved by normalization. Deleted formula magicLemma11.1, which reduced to `true'. LP0.1.669: qed All conjectures have been proved. LP0.1.670: % ---------------------------------------------------------- LP0.1.671: LP0.1.672: % ---------------------------------------------------------- LP0.1.673: set name magicLemma12 The name-prefix is now `magicLemma12'. LP0.1.674: declare variables f: fun [pair [T1, V], T1], g: fun [bag [W], bag [W]], h: fun [pair [T1, V], pair [T1, V]], j: fun [pair [T1, V], bag [W]] .. LP0.1.675: prove (f \times g) \circ \ = \ Attempting to prove conjecture magicLemma12.1: (f \times g) \circ \ = \ Conjecture magicLemma12.1 [] Proved by normalization. Deleted formula magicLemma12.1, which reduced to `true'. LP0.1.676: qed All conjectures have been proved. LP0.1.677: % ---------------------------------------------------------- LP0.1.678: LP0.1.679: % ---------------------------------------------------------- LP0.1.680: set name magicLemma13 The name-prefix is now `magicLemma13'. LP0.1.681: declare variables f: fun [pair [T1, V], T1] .. LP0.1.682: prove f \circ id = f Attempting to prove conjecture magicLemma13.1: f \circ id = f Conjecture magicLemma13.1 [] Proved by normalization. Deleted formula magicLemma13.1, which reduced to `true'. LP0.1.683: qed All conjectures have been proved. LP0.1.684: % ---------------------------------------------------------- LP0.1.685: LP0.1.686: % ---------------------------------------------------------- LP0.1.687: set name magicLemma14 The name-prefix is now `magicLemma14'. LP0.1.688: declare variables f: fun [pair [T1, V], bag [W]] .. LP0.1.689: prove id \circ f:fun [pair [T1, V], bag [W]] = f Attempting to prove conjecture magicLemma14.1: (id \circ f):fun[pair[T1, V], bag[W]] = f Conjecture magicLemma14.1 [] Proved by normalization. Deleted formula magicLemma14.1, which reduced to `true'. LP0.1.690: qed All conjectures have been proved. LP0.1.691: % ---------------------------------------------------------- LP0.1.692: LP0.1.693: % ---------------------------------------------------------- LP0.1.694: set name magicLemma15 The name-prefix is now `magicLemma15'. LP0.1.695: declare variables A: bag [W], f: fun [pair [T1, V], T1] .. LP0.1.696: prove \ = \ \circ f Attempting to prove conjecture magicLemma15.1: \ = \ \circ f Conjecture magicLemma15.1 [] Proved by normalization. Deleted formula magicLemma15.1, which reduced to `true'. LP0.1.697: qed All conjectures have been proved. LP0.1.698: % ---------------------------------------------------------- LP0.1.699: LP0.1.700: % ---------------------------------------------------------- LP0.1.701: set name magicLemma16 The name-prefix is now `magicLemma16'. LP0.1.702: declare variables A: bag [W], B: bag [T1], q: pred [pair [W, T1]] .. LP0.1.703: LP0.1.704: prove set ! (iterate (ex (q\inv) \oplus \, id) ! B) = set ! (join (q, snd) ! [A, B]) .. Attempting to prove conjecture magicLemma16.1: set ! (iterate(ex(q\inv) \oplus \, id) ! B) = set ! (join(q, snd) ! [A, B]) Suspending proof of conjecture magicLemma16.1 LP0.1.705: LP0.1.706: declare operator wc: -> W LP0.1.707: resume by <=> Creating subgoals for proof of <=> New constants: xc, Bc, qc, Ac => hypothesis: magicLemma16ImpliesHyp.1: \E y:W (y \in Ac /\ qc ? [y, xc]) /\ xc \in Bc => subgoal: \E x:W (qc ? [x, xc] /\ xc \in Bc /\ x \in Ac) <= hypothesis: magicLemma16ImpliesHyp.2: \E x:W (qc ? [x, xc] /\ xc \in Bc /\ x \in Ac) <= subgoal: \E y:W (y \in Ac /\ qc ? [y, xc]) /\ xc \in Bc Attempting to prove level 2 subgoal 1 for proof of <=> Added hypothesis magicLemma16ImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula magicLemma16ImpliesHyp.1 to yield the following formulas, which imply magicLemma16ImpliesHyp.1. magicLemma16ImpliesHyp.1.1: xc \in Bc magicLemma16ImpliesHyp.1.2: \E y:W (y \in Ac /\ qc ? [y, xc]) Level 2 subgoal 1 for proof of <=> [] Proved by normalization. Attempting to prove level 2 subgoal 2 for proof of <=> Added hypothesis magicLemma16ImpliesHyp.2 to the system. The system now contains 489 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 2 subgoal 2 for proof of <=> LP0.1.708: LP0.1.709: % => Trivial LP0.1.710: % <= LP0.1.711: LP0.1.712: fix x:W as wc in *Impl* A prenex-existential quantifier in formula magicLemma16ImpliesHyp.2 has been eliminated to produce formula magicLemma16.2, qc ? [wc, xc] /\ xc \in Bc /\ wc \in Ac Deduction rule lp_and_is_true has been applied to formula magicLemma16.2 to yield the following formulas, which imply magicLemma16.2. magicLemma16.2.1: qc ? [wc, xc] magicLemma16.2.2: xc \in Bc magicLemma16.2.3: wc \in Ac Level 2 subgoal 2 for proof of <=> [] Proved by normalization. Conjecture magicLemma16.1: set ! (iterate(ex(q\inv) \oplus \, id) ! B) = set ! (join(q, snd) ! [A, B]) [] Proved <=>. LP0.1.713: LP0.1.714: qed All conjectures have been proved. LP0.1.715: LP0.1.716: % L1: Rules Used in Transformation, Magic LP0.1.717: % --------------------------------------- LP0.1.718: LP0.1.719: set name shift The name-prefix is now `shift'. LP0.1.720: declare variables p,q,r: pred [T] .. LP0.1.721: prove p & q & r = p & (q & r) Attempting to prove conjecture shift.1: p & q & r = p & (q & r) Conjecture shift.1 [] Proved by normalization. Deleted formula shift.1, which reduced to `true'. LP0.1.722: qed All conjectures have been proved. LP0.1.723: LP0.1.724: set name nod The name-prefix is now `nod'. LP0.1.725: declare variables p: pred [pair [T1, T2]], f: fun [T2, U], g: fun [bag [U], V], A: bag [T1], B: bag [T2] .. LP0.1.726: prove njoin (p, f, g) ! [set ! A, B] = njoin (p, f, g) ! [A, B] Attempting to prove conjecture nod.1: njoin(p, f, g) ! [set ! A, B] = njoin(p, f, g) ! [A, B] Suspending proof of conjecture nod.1 LP0.1.727: LP0.1.728: resume by induction on A:bag [T1] Creating subgoals for proof by structural induction on `A:bag[T1]' Basis subgoal: Subgoal 1: njoin(p, f, g) ! [set ! {}, B] = njoin(p, f, g) ! [{}, B] Induction constant: Ac Induction hypothesis: nodInductHyp.1: njoin(p, f, g) ! [set ! Ac, B] = njoin(p, f, g) ! [Ac, B] Induction subgoal: Subgoal 2: njoin(p, f, g) ! [set ! insert(t, Ac), B] = njoin(p, f, g) ! [insert(t, Ac), B] Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A Level 2 subgoal 1 (basis step) for proof by induction on A [] Proved by normalization. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on A Added hypothesis nodInductHyp.1 to the system. The system now contains 490 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.729: LP0.1.730: % Base Case: Trivial LP0.1.731: LP0.1.732: % Inductive Case LP0.1.733: LP0.1.734: resume by cases t \in Ac Creating subgoals for proof by cases New constant: tc Case hypotheses: nodCaseHyp.1.1: tc \in Ac nodCaseHyp.1.2: ~(tc \in Ac) Same subgoal for all cases: njoin(p, f, g) ! [if tc \in Ac then set ! Ac else insert(tc, set ! Ac), B] = njoin(p, f, g) ! [insert(tc, Ac), B] Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis nodCaseHyp.1.1 to the system. Level 3 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis nodCaseHyp.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: njoin(p, f, g) ! [set ! insert(t, Ac), B] = njoin(p, f, g) ! [insert(t, Ac), B] [] Proved by cases t \in Ac. Conjecture nod.1: njoin(p, f, g) ! [set ! A, B] = njoin(p, f, g) ! [A, B] [] Proved by structural induction on `A:bag[T1]'. LP0.1.735: LP0.1.736: qed All conjectures have been proved. LP0.1.737: LP0.1.738: set name magic The name-prefix is now `magic'. LP0.1.739: LP0.1.740: declare variables A': bag [T1], B: bag [T2], A: bag [W], p: pred [pair [T1, T2]], g: fun [T2, U], h: fun [bag [U], V], r: pred [pair [W, pair [T1, V]]], f: fun [pair [W, pair [T1, V]], pair [W, pair [T1, V]]], q: pred [pair [W, T1]], x: T1 .. LP0.1.741: LP0.1.742: prove join ((q \oplus (id \times fst)) & r, f:fun [pair [W, pair [T1, V]], X]) ! [A, njoin (p, g, h) ! [A', B]] = join ((q \oplus (id \times fst)) & r, f) ! [A, njoin (p, g, h) ! [set ! (join (q, snd) ! [A, A']), B]] .. Attempting to prove conjecture magic.1: (join((q \oplus (id \times fst)) & r, f) ! [A, njoin(p, g, h) ! [A', B]]): bag[X] = join((q \oplus (id \times fst)) & r, f) ! [A, njoin(p, g, h) ! [set ! (join(q, snd) ! [A, A']), B]] Suspending proof of conjecture magic.1 LP0.1.743: LP0.1.744: set immunity on The immunity is now `on'. LP0.1.745: prove (join (p & q, f) ! [A, B]):bag[X] = iterate (q, f) ! (join (p, id) ! [A, B]) .. Attempting to prove level 2 lemma magic.2: join(p & q, f) ! [A, B] = iterate(q, f) ! (join(p, id) ! [A, B]) Level 2 lemma magic.2 [] Proved by normalization. Attempting to prove conjecture magic.1 Deleted formula magicLemma4.1, which reduced to `true'. Suspending proof of conjecture magic.1 LP0.1.746: LP0.1.747: prove njoin (q, g, h) ! [A, B] = njoin (q, g, h) ! [set ! A, B] Attempting to prove level 2 lemma magic.3: njoin(q, g, h) ! [A, B] = njoin(q, g, h) ! [set ! A, B] Level 2 lemma magic.3 [] Proved by normalization. Attempting to prove conjecture magic.1 Deleted formula nod.1, which reduced to `true'. Suspending proof of conjecture magic.1 LP0.1.748: LP0.1.749: set order left The ordering-method is now `left-to-right'. LP0.1.750: prove ex ((q \oplus (id \times fst))\inv) \oplus \ = ex (q\inv) \oplus \ \oplus fst .. Attempting to prove level 2 lemma magic.4: ex((q \oplus (id \times fst))\inv) \oplus \ = ex(q\inv) \oplus \ \oplus fst Level 2 lemma magic.4 [] Proved by normalization. Attempting to prove conjecture magic.1: (join((q \oplus (id \times fst)) & r, f) ! [A, njoin(p, g, h) ! [A', B]]): bag[X] = join((q \oplus (id \times fst)) & r, f) ! [A, njoin(p, g, h) ! [set ! (join(q, snd) ! [A, A']), B]] Current subgoal: iterate(r, f) ! (join(q \oplus (id \times fst), id) ! [A, njoin(p, g, h) ! [A', B]]) = iterate(r, f) ! (join(q \oplus (id \times fst), id) ! [A, njoin(p, g, h) ! [join(q, snd) ! [A, A'], B]]) The system now contains 491 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of conjecture magic.1 LP0.1.751: set immunity off The immunity is now `off'. LP0.1.752: set order noeq The ordering-method is now `noeq-dsmpos'. LP0.1.753: LP0.1.754: crit-pairs magicLemma5c with magic / contains-oper (fst: -> fun[pair [T1,V],T1]) .. The following equations are critical pairs between rewrite rules magicLemma5c.1 and magic.4. magic.5: (join(q \oplus (id \times fst), f) ! [A, iterate(ex(q\inv) \oplus \ \oplus fst, id) ! B]): bag[pair[W, pair[T1, V]]] = join(q \oplus (id \times fst), f) ! [A, B] The system now contains 1 formula and 491 rewrite rules. The rewriting system is NOT guaranteed to terminate. The system now contains 492 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.755: LP0.1.756: crit-pairs magicLemma8 with magic / contains-oper (fst: -> fun[pair [T1,V],T1]) .. The following equations are critical pairs between rewrite rules magicLemma8.1 and magic.5. magic.6: (join(q \oplus (id \times fst), f) ! [A, njoin(q, g, h) ! [iterate(ex(q\inv) \oplus \, id) ! A, B]]): bag[pair[W, pair[T1, V]]] = join(q \oplus (id \times fst), f) ! [A, njoin(q, g, h) ! [A, B]] The system now contains 1 formula and 492 rewrite rules. The rewriting system is NOT guaranteed to terminate. The system now contains 493 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.757: LP0.1.758: set immunity on The immunity is now `on'. LP0.1.759: prove set ! (iterate (ex (q\inv) \oplus \, id) ! B) = set ! (join (q, snd) ! [A, B]) .. Attempting to prove level 2 lemma magic.7: set ! (iterate(ex(q\inv) \oplus \, id) ! B) = set ! (join(q, snd) ! [A, B]) Level 2 lemma magic.7 [] Proved by normalization. Attempting to prove conjecture magic.1: (join((q \oplus (id \times fst)) & r, f) ! [A, njoin(p, g, h) ! [A', B]]): bag[X] = join((q \oplus (id \times fst)) & r, f) ! [A, njoin(p, g, h) ! [set ! (join(q, snd) ! [A, A']), B]] Current subgoal: iterate(r, f) ! (join(q \oplus (id \times fst), id) ! [A, njoin(p, g, h) ! [A', B]]) = iterate(r, f) ! (join(q \oplus (id \times fst), id) ! [A, njoin(p, g, h) ! [join(q, snd) ! [A, A'], B]]) The system now contains 494 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of conjecture magic.1 LP0.1.760: set immunity off The immunity is now `off'. LP0.1.761: LP0.1.762: LP0.1.763: crit-pairs magic* with magic The following equations are critical pairs between rewrite rules magic.7 and magic.3. magic.8: njoin(q, g, h) ! [iterate(ex(q\inv) \oplus \, id) ! B, B] = njoin(q, g, h) ! [join(q, snd) ! [A, B], B] The system now contains 1 formula and 494 rewrite rules. The rewriting system is NOT guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Conjecture magic.1 [] Proved by normalization. The system now contains 491 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.764: LP0.1.765: qed All conjectures have been proved. LP0.1.766: LP0.1.767: LP0.1.768: % Section 6: SimplifyJoin LP0.1.769: % LP0.1.770: % Proof Scripts for COKO Transformation, LP0.1.771: % LP0.1.772: % TRANSFORMATION SimplifyJoin LP0.1.773: % USES LP0.1.774: % SJ1: join (p OPLUS (f X g), #2) ! [A, B] --> LP0.1.775: % join (p OPLUS (id X g), #2) ! [iterate (K (true), f) ! A, B], LP0.1.776: % SJ2: iterate (p, f) ! (iterate (q, id) ! A) --> iterate (p & q, f) ! A, LP0.1.777: % SJ3: set ! (join (=, #2) ! [A, B]) --> set ! (int (=) ! [A, B]), LP0.1.778: % SJ4: int (=) ! [iterate (p, f) ! A, iterate (K (true), f) ! A] --> LP0.1.779: % iterate (p, f) ! A, LP0.1.780: % SJ5a: f o ID --> f, LP0.1.781: % SJ5b: ID o f --> f, LP0.1.782: % SJ6a: K (true) & p --> p, LP0.1.783: % SJ6b: p & K (true) --> p, LP0.1.784: % SJ7: K (true) OPLUS f --> K (true), LP0.1.785: % SJ8: p OPLUS ID --> p, LP0.1.786: % SJ9: ID X ID --> ID, LP0.1.787: % SJ10: iterate (p, f) ! (join (q, g) ! [A, B]) --> LP0.1.788: % join (q & (p OPLUS g), f o g) ! [A, B], LP0.1.789: % Pushdown LP0.1.790: % BEGIN LP0.1.791: % GIVEN _F ! A DO SJ1 (A); LP0.1.792: % GIVEN _F ! (_F ! [A, _O]) DO SJ2 (A); LP0.1.793: % BU {SJ5a || SJ5b || SJ6a || SJ6b || SJ7 || SJ8 || SJ9}; LP0.1.794: % SJ3; LP0.1.795: % GIVEN _F ! A DO SJ4 (A); LP0.1.796: % BU {SJ5a || SJ5b || SJ6a || SJ6b || SJ7 || SJ8 || SJ9}; LP0.1.797: % TD {SJ10 -> Pushdown} LP0.1.798: % END LP0.1.799: % LP0.1.800: % See Section 5 for proofs of rewrite rules: LP0.1.801: % SJ5a (magicLemma13), SJ5b (magicLemma14), SJ8 (magicLemma10), LP0.1.802: % SJ9 (magicLemma9) LP0.1.803: % LP0.1.804: % See Section 2 for proofs of rewrite rules: LP0.1.805: % SJ6a (simplify) LP0.1.806: % LP0.1.807: % Theorem proving revealed that [CZ98a] has an *incorrect* version of SJ4. LP0.1.808: % The corrected version is shown above and also be found in the updated LP0.1.809: % version of this paper retrievable from: LP0.1.810: % LP0.1.811: % ftp://wilma.cs.brown.edu/u/mfc/sigmod98.ps.Z LP0.1.812: % LP0.1.813: LP0.1.814: clear LP0.1.815: forget Critical pair list cleared. LP0.1.816: unregister registry LP0.1.817: set order manual The ordering-method is now `manual'. LP0.1.818: exec-silently SimpJoin_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/SimpJoin_Aux_Axioms.lp'. LP0.1.819: register height !:fun[pair[T2, U], T2],pair[T2, U]->T2 = !:fun[pair[T2, U], pair[U, T2]],pair[T2, U]->pair[U, T2] = !:fun[pair[U, T2], T2],pair[U, T2]->T2 .. Registry extended. LP0.1.820: register height !:fun[pair[T, T], T],pair[T, T]->T = !:fun[pair[T, T], pair[T, T]],pair[T, T]->pair[T, T] .. Registry extended. LP0.1.821: register height !:fun[pair[T2, T1], V],pair[T2, T1]->V = !:fun[pair[T1, T2], V],pair[T1, T2]->V = !:fun[U, V],U->V .. Registry extended. LP0.1.822: register height !:fun[pair[T2, T1], V],pair[T2, T1]->V >= (!:fun[pair[T2, T1], pair[T1, T2]],pair[T2, T1]->pair[T1, T2], !:fun[pair[T2, T1], T2],pair[T2, T1]->T2, !:fun[pair[T1, T2], T2],pair[T1, T2]->T2, !:fun[pair[T1, T2], U],pair[T1, T2]->U, !:fun[pair[T2, T1], U],pair[T2, T1]->U) .. Re