LP (the Larch Prover), Release 3.1a (95/04/27) logging to
`/pro/oodb/specs/KOLA98/SIGMOD98_Scripts.lplog' on 21 June 1998 18:15:57.
LP0.1.2:
LP0.1.3: % ******************************************************************************
LP0.1.4: % * *
LP0.1.5: % * Script File: SIGMOD98_Scripts *
LP0.1.6: % * -------------------------------------------------------------------------- *
LP0.1.7: % * Scripts Author: Mitch Cherniack (mfc@cs.brandeis.edu) *
LP0.1.8: % * Date: June, 1998 *
LP0.1.9: % * *
LP0.1.10: % * Present Address: Computer Science Department *
LP0.1.11: % * Brandeis University *
LP0.1.12: % * Waltham, MA 02254 *
LP0.1.13: % * -------------------------------------------------------------------------- *
LP0.1.14: % * *
LP0.1.15: % * Proof Scripts Establishing Correctness of Rewrite Rules used in the paper, *
LP0.1.16: % * [CZ98a]: *
LP0.1.17: % * *
LP0.1.18: % * [CZ98a] Changing the Rules: Transformations for Rule-Based Optimizers *
LP0.1.19: % * Mitch Cherniack and Stan Zdonik, In Proceedings of the 1998 ACM *
LP0.1.20: % * SIGMOD International Conference on Management of Data, Seattle, *
LP0.1.21: % * WA, June, 1998. *
LP0.1.22: % * *
LP0.1.23: % * For an up-to-date version of [CZ98a], see: *
LP0.1.24: % * ftp://wilma.cs.brown.edu/u/mfc/sigmod98.ps.Z *
LP0.1.25: % * *
LP0.1.26: % * *
LP0.1.27: % * Instructions: *
LP0.1.28: % * *
LP0.1.29: % * Requires Version 3.1a of the LP Theorem Prover, available from *
LP0.1.30: % * MIT, Laboratory of Computer Science. For software and documentation on *
LP0.1.31: % * LP see: *
LP0.1.32: % * *
LP0.1.33: % * http://www.sds.lcs.mit.edu/spd/larch/LP/overview.html *
LP0.1.34: % * *
LP0.1.35: % * With LP installed in $path, run this theorem prover script by typing *
LP0.1.36: % * *
LP0.1.37: % * $path/lp -c SIGMOD98_Scripts *
LP0.1.38: % * *
LP0.1.39: % ******************************************************************************
LP0.1.40:
LP0.1.41: % Section 1: CNF
LP0.1.42: %
LP0.1.43: % Proof Scripts for COKO Transformations,
LP0.1.44: %
LP0.1.45: % TRANSFORMATION CNFNE
LP0.1.46: % USES
LP0.1.47: % CNFAux
LP0.1.48: % BEGIN
LP0.1.49: % BU {CNFAux}
LP0.1.50: % END
LP0.1.51: %
LP0.1.52: % TRANSFORMATION CNFAux
LP0.1.53: % USES
LP0.1.54: % dist1: p | (q & r) --> (p | q) & (p | r),
LP0.1.55: % dist2: (p & q) | r --> (p | r) & (q | r)
LP0.1.56: % BEGIN
LP0.1.57: % {dist1 || dist2} ->
LP0.1.58: % GIVEN p & q DO {CNFAux (p); CNFAux (q)}
LP0.1.59: % END
LP0.1.60: %
LP0.1.61: % TRANSFORMATION CNF
LP0.1.62: % USES
LP0.1.63: % CNFNE,
LP0.1.64: % involution: ~ (~ (p)) --> p,
LP0.1.65: % deMorgan1: ~ (p & q) --> ~ (p) | ~ (q),
LP0.1.66: % deMorgan2: ~ (p | q) --> ~ (p) & ~ (q)
LP0.1.67: % BEGIN
LP0.1.68: % TD {involution || deMorgan1 || deMorgan2};
LP0.1.69: % BU {involution};
LP0.1.70: % CNFNE
LP0.1.71: % END
LP0.1.72: %
LP0.1.73: % In [CZ98a], CNFNE is called CNF, and CNF (above) is not
LP0.1.74: % described.
LP0.1.75:
LP0.1.76: clear
LP0.1.77: set order manual
The ordering-method is now `manual'.
LP0.1.78: exec-silently CNF_Aux_Axioms
End of input from file `/pro/oodb/specs/KOLA98/CNF_Aux_Axioms.lp'.
LP0.1.79: set order noeq-dsmpos
The ordering-method is now `noeq-dsmpos'.
LP0.1.80: order formulas
The system now contains 5 rewrite rules. The rewriting system is guaranteed to
terminate.
All equations have been oriented into rewrite rules. The rewriting system is
guaranteed to terminate.
LP0.1.81: make immune formulas
LP0.1.82:
LP0.1.83: declare variables
p, q, r: pred [T]
..
LP0.1.84:
LP0.1.85:
LP0.1.86: % L1: Rules Used in CNFAux
LP0.1.87: % ------------------------
LP0.1.88:
LP0.1.89: set name dist1
The name-prefix is now `dist1'.
LP0.1.90: prove (p & q) | r = (p | r) & (q | r)
Attempting to prove conjecture dist1.1: (p & q) | r = (p | r) & (q | r)
Suspending proof of conjecture dist1.1
LP0.1.91:
LP0.1.92: resume by <=>
Creating subgoals for proof of <=>
New constants: pc, xc, rc, qc
=> hypothesis:
dist1ImpliesHyp.1: (pc ? xc \/ rc ? xc) /\ (qc ? xc \/ rc ? xc)
=> subgoal:
(pc ? xc /\ qc ? xc) \/ rc ? xc
<= hypothesis:
dist1ImpliesHyp.2: (pc ? xc /\ qc ? xc) \/ rc ? xc
<= subgoal:
(pc ? xc \/ rc ? xc) /\ (qc ? xc \/ rc ? xc)
Attempting to prove level 2 subgoal 1 for proof of <=>
Added hypothesis dist1ImpliesHyp.1 to the system.
Deduction rule lp_and_is_true has been applied to formula dist1ImpliesHyp.1 to
yield the following formulas, which imply dist1ImpliesHyp.1.
dist1ImpliesHyp.1.1: pc ? xc \/ rc ? xc
dist1ImpliesHyp.1.2: qc ? xc \/ rc ? xc
The system now contains 7 rewrite rules. The rewriting system is guaranteed to
terminate.
Suspending proof of level 2 subgoal 1 for proof of <=>
LP0.1.93:
LP0.1.94: % =>
LP0.1.95: resume by cases (rc ? xc)
Creating subgoals for proof by cases
Case hypotheses:
dist1CaseHyp.1.1: rc ? xc
dist1CaseHyp.1.2: ~(rc ? xc)
Same subgoal for all cases:
(pc ? xc /\ qc ? xc) \/ rc ? xc
Attempting to prove level 3 subgoal for case 1 (out of 2)
Added hypothesis dist1CaseHyp.1.1 to the system.
Level 3 subgoal for case 1 (out of 2)
[] Proved by normalization.
Attempting to prove level 3 subgoal for case 2 (out of 2)
Added hypothesis dist1CaseHyp.1.2 to the system.
Level 3 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 2 subgoal 1 for proof of <=>
[] Proved by cases rc ? xc.
Attempting to prove level 2 subgoal 2 for proof of <=>
Added hypothesis dist1ImpliesHyp.2 to the system.
The system now contains 6 rewrite rules. The rewriting system is guaranteed to
terminate.
Suspending proof of level 2 subgoal 2 for proof of <=>:
(pc ? xc \/ rc ? xc) /\ (qc ? xc \/ rc ? xc)
LP0.1.96:
LP0.1.97: % <=
LP0.1.98: resume by cases (rc ? xc)
Creating subgoals for proof by cases
Case hypotheses:
dist1CaseHyp.1.1: rc ? xc
dist1CaseHyp.1.2: ~(rc ? xc)
Same subgoal for all cases:
(pc ? xc \/ rc ? xc) /\ (qc ? xc \/ rc ? xc)
Attempting to prove level 3 subgoal for case 1 (out of 2)
Added hypothesis dist1CaseHyp.1.1 to the system.
Level 3 subgoal for case 1 (out of 2)
[] Proved by normalization.
Attempting to prove level 3 subgoal for case 2 (out of 2)
Added hypothesis dist1CaseHyp.1.2 to the system.
Deduction rule lp_and_is_true has been applied to formula dist1ImpliesHyp.2 to
yield the following formulas, which imply dist1ImpliesHyp.2.
dist1ImpliesHyp.2.1: pc ? xc
dist1ImpliesHyp.2.2: qc ? xc
Level 3 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 2 subgoal 2 for proof of <=>
[] Proved by cases rc ? xc.
Conjecture dist1.1: (p & q) | r = (p | r) & (q | r)
[] Proved <=>.
LP0.1.99:
LP0.1.100: qed
All conjectures have been proved.
LP0.1.101:
LP0.1.102: set name dist2
The name-prefix is now `dist2'.
LP0.1.103: prove r | (p & q) = (p | r) & (q | r)
Attempting to prove conjecture dist2.1: r | (p & q) = (p | r) & (q | r)
Conjecture dist2.1
[] Proved by normalization.
Deleted formula dist2.1, which reduced to `true'.
LP0.1.104: qed
All conjectures have been proved.
LP0.1.105:
LP0.1.106:
LP0.1.107: % L1: Rules Used in CNF
LP0.1.108: % ---------------------
LP0.1.109:
LP0.1.110: set name involution
The name-prefix is now `involution'.
LP0.1.111: prove ~ (~ (p)) = p
Attempting to prove conjecture involution.1: ~ ~p = p
Conjecture involution.1
[] Proved by normalization.
Deleted formula involution.1, which reduced to `true'.
LP0.1.112: qed
All conjectures have been proved.
LP0.1.113:
LP0.1.114: set name deMorgan1
The name-prefix is now `deMorgan1'.
LP0.1.115: prove ~ (p & q) = (~ (p)) | (~ (q))
Attempting to prove conjecture deMorgan1.1: ~(p & q) = (~p) | (~q)
Suspending proof of conjecture deMorgan1.1
LP0.1.116:
LP0.1.117: resume by <=>
Creating subgoals for proof of <=>
New constants: pc, xc, qc
=> hypothesis:
deMorgan1ImpliesHyp.1: ~(pc ? xc) \/ ~(qc ? xc)
=> subgoal:
~(pc ? xc /\ qc ? xc)
<= hypothesis:
deMorgan1ImpliesHyp.2: ~(pc ? xc /\ qc ? xc)
<= subgoal:
~(pc ? xc) \/ ~(qc ? xc)
Attempting to prove level 2 subgoal 1 for proof of <=>
Added hypothesis deMorgan1ImpliesHyp.1 to the system.
The system now contains 7 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
Suspending proof of level 2 subgoal 1 for proof of <=>
LP0.1.118:
LP0.1.119: % =>
LP0.1.120: resume by cases ~ (pc ? xc)
Creating subgoals for proof by cases
Case hypotheses:
deMorgan1CaseHyp.1.1: ~(pc ? xc)
deMorgan1CaseHyp.1.2: ~(~(pc ? xc))
Same subgoal for all cases:
~(pc ? xc /\ qc ? xc)
Attempting to prove level 3 subgoal for case 1 (out of 2)
Added hypothesis deMorgan1CaseHyp.1.1 to the system.
Level 3 subgoal for case 1 (out of 2)
[] Proved by normalization.
Attempting to prove level 3 subgoal for case 2 (out of 2)
Added hypothesis deMorgan1CaseHyp.1.2 to the system.
Level 3 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 2 subgoal 1 for proof of <=>
[] Proved by cases ~(pc ? xc).
Attempting to prove level 2 subgoal 2 for proof of <=>
Added hypothesis deMorgan1ImpliesHyp.2 to the system.
Suspending proof of level 2 subgoal 2 for proof of <=>
LP0.1.121:
LP0.1.122: % <=
LP0.1.123: resume by contradiction
Creating subgoals for proof by contradiction
Hypothesis:
deMorgan1ContraHyp.1: ~(~(pc ? xc) \/ ~(qc ? xc))
Only subgoal:
false
Attempting to prove level 3 subgoal for proof by contradiction
Added hypothesis deMorgan1ContraHyp.1 to the system.
Deduction rule lp_or_is_false has been applied to formula deMorgan1ContraHyp.1
to yield the following formulas, which imply deMorgan1ContraHyp.1.
deMorgan1ContraHyp.1.1: ~(~(pc ? xc))
deMorgan1ContraHyp.1.2: ~(~(qc ? xc))
Formula deMorgan1ImpliesHyp.2, false, is inconsistent.
Level 3 subgoal for proof by contradiction
[] Proved by detecting an inconsistency.
Level 2 subgoal 2 for proof of <=>: ~(pc ? xc) \/ ~(qc ? xc)
[] Proved by contradiction.
Conjecture deMorgan1.1: ~(p & q) = (~p) | (~q)
[] Proved <=>.
LP0.1.124:
LP0.1.125: qed
All conjectures have been proved.
LP0.1.126:
LP0.1.127: set name deMorgan2
The name-prefix is now `deMorgan2'.
LP0.1.128: prove ~ (p | q) = (~ (p)) & (~ (q))
Attempting to prove conjecture deMorgan2.1: ~(p | q) = (~p) & (~q)
Suspending proof of conjecture deMorgan2.1
LP0.1.129: resume by <=>
Creating subgoals for proof of <=>
New constants: pc, xc, qc
=> hypothesis:
deMorgan2ImpliesHyp.1: ~(pc ? xc) /\ ~(qc ? xc)
=> subgoal:
~(pc ? xc \/ qc ? xc)
<= hypothesis:
deMorgan2ImpliesHyp.2: ~(pc ? xc \/ qc ? xc)
<= subgoal:
~(pc ? xc) /\ ~(qc ? xc)
Attempting to prove level 2 subgoal 1 for proof of <=>
Added hypothesis deMorgan2ImpliesHyp.1 to the system.
Deduction rule lp_and_is_true has been applied to formula deMorgan2ImpliesHyp.1
to yield the following formulas, which imply deMorgan2ImpliesHyp.1.
deMorgan2ImpliesHyp.1.1: ~(pc ? xc)
deMorgan2ImpliesHyp.1.2: ~(qc ? xc)
Level 2 subgoal 1 for proof of <=>
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 for proof of <=>
Added hypothesis deMorgan2ImpliesHyp.2 to the system.
Deduction rule lp_or_is_false has been applied to formula deMorgan2ImpliesHyp.2
to yield the following formulas, which imply deMorgan2ImpliesHyp.2.
deMorgan2ImpliesHyp.2.1: ~(pc ? xc)
deMorgan2ImpliesHyp.2.2: ~(qc ? xc)
Level 2 subgoal 2 for proof of <=>
[] Proved by normalization.
Conjecture deMorgan2.1
[] Proved <=>.
The system now contains 8 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
LP0.1.130: qed
All conjectures have been proved.
LP0.1.131:
LP0.1.132:
LP0.1.133:
LP0.1.134: % Section 2: SNF
LP0.1.135: %
LP0.1.136: % Proof Scripts for COKO Transformations,
LP0.1.137: %
LP0.1.138: % TRANSFORMATION SNF
LP0.1.139: % USES
LP0.1.140: % SimpLits,
LP0.1.141: % CNF,
LP0.1.142: % OrderConjs,
LP0.1.143: % pushneg: ~ (p OPLUS f) --> (~ (p)) OPLUS f,
LP0.1.144: % init: p --> (K (true) OPLUS #1) & (K (true) OPLUS #2) & K (true) & p,
LP0.1.145: % pull: (p OPLUS f) | (q OPLUS f) --> (p | q) OPLUS f,
LP0.1.146: % shift: p & (q & r) --> (p & r) & q,
LP0.1.147: % simplify: K (true) & p --> p
LP0.1.148: % BEGIN
LP0.1.149: % SimpLits;
LP0.1.150: % CNF;
LP0.1.151: % TD {pushneg};
LP0.1.152: % init;
LP0.1.153: % BU {pull || {REPEAT shift}};
LP0.1.154: % OrderConjs;
LP0.1.155: % BU {simplify}
LP0.1.156: % END
LP0.1.157: %
LP0.1.158: % TRANSFORMATION SimpLits
LP0.1.159: % USES
LP0.1.160: % SL1: --> o h,
LP0.1.161: % SL2: --> K ([x, y]),
LP0.1.162: % SL3: --> o f,
LP0.1.163: % SL4: --> o f,
LP0.1.164: % SL5: f o (g o h) --> (f o g) o h,
LP0.1.165: % SL6: f o K (x) --> K (f ! x),
LP0.1.166: % SL7: p OPLUS (f o g) --> p OPLUS f OPLUS g,
LP0.1.167: % SL8: p OPLUS K (x) --> K (p ? x)
LP0.1.168: % BEGIN
LP0.1.169: % BU {{{SL1 || SL2 || SL3 || SL4} ->
LP0.1.170: % {REPEAT {SL5 -> {print "SL5 fired on";
LP0.1.171: % GIVEN f DO print f; print "\n"}}}} ||
LP0.1.172: % SL6 || SL7 || SL8}
LP0.1.173: % END
LP0.1.174: %
LP0.1.175: % TRANSFORMATION OrderConjs
LP0.1.176: % USES
LP0.1.177: % OC1: (p OPLUS #1) & q & r & (r' OPLUS #1) --> ((p & r') OPLUS #1) & q & r,
LP0.1.178: % OC2: p & (q OPLUS #2) & r & (r' OPLUS #2) --> p & ((q & r') OPLUS #2) & r,
LP0.1.179: % OC3: p & q & r & r' --> p & q & (r & r')
LP0.1.180: % BEGIN
LP0.1.181: % BU {OC1 || OC2 || OC3}
LP0.1.182: % END
LP0.1.183: %
LP0.1.184: % In [CZ98a], transformation SNF does not contain the rewrite rule,
LP0.1.185: % pushneg, nor the firing algorithm statement,
LP0.1.186: %
LP0.1.187: % TD {pushneg}
LP0.1.188: %
LP0.1.189:
LP0.1.190:
LP0.1.191: clear
LP0.1.192: set order manual
The ordering-method is now `manual'.
LP0.1.193: exec-silently SNF_Aux_Axioms
End of input from file `/pro/oodb/specs/KOLA98/SNF_Aux_Axioms.lp'.
LP0.1.194: set order noeq-dsmpos
The ordering-method is now `noeq-dsmpos'.
LP0.1.195: order formulas
The system now contains 66 rewrite rules. The rewriting system is guaranteed
to terminate.
All equations have been oriented into rewrite rules. The rewriting system is
guaranteed to terminate.
LP0.1.196: make immune formulas
LP0.1.197:
LP0.1.198: % L1: Rules Used in Transformation, SNF
LP0.1.199: % -------------------------------------
LP0.1.200:
LP0.1.201: set name pushneg
The name-prefix is now `pushneg'.
LP0.1.202: declare variables p: pred [S], f: fun [R, S]
LP0.1.203: prove ~ (p \oplus f) = (~ (p) \oplus f)
Attempting to prove conjecture pushneg.1: ~(p \oplus f) = (~p) \oplus f
Conjecture pushneg.1
[] Proved by normalization.
Deleted formula pushneg.1, which reduced to `true'.
LP0.1.204: qed
All conjectures have been proved.
LP0.1.205:
LP0.1.206: set name init
The name-prefix is now `init'.
LP0.1.207: declare variables p: pred [pair [T, U]]
LP0.1.208: prove p = (K (true) \oplus fst) & (K (true) \oplus snd) & K (true) & p
Attempting to prove conjecture init.1:
p = (K(true) \oplus fst) & (K(true) \oplus snd) & K(true) & p
Conjecture init.1
[] Proved by normalization.
Deleted formula init.1, which reduced to `true'.
LP0.1.209: qed
All conjectures have been proved.
LP0.1.210:
LP0.1.211: set name pull
The name-prefix is now `pull'.
LP0.1.212: declare variables p: pred [S], f: fun [R, S]
LP0.1.213: prove (p \oplus f) | (q \oplus f) = (p | q) \oplus f
Attempting to prove conjecture pull.1:
(p \oplus f) | (q \oplus f) = (p | q) \oplus f
Conjecture pull.1
[] Proved by normalization.
Deleted formula pull.1, which reduced to `true'.
LP0.1.214: qed
All conjectures have been proved.
LP0.1.215:
LP0.1.216: set name shift
The name-prefix is now `shift'.
LP0.1.217: declare variables p, q, r: pred [S]
LP0.1.218: prove p & (q & r) = (p & r) & q
Attempting to prove conjecture shift.1: p & (q & r) = p & r & q
Conjecture shift.1
[] Proved by normalization.
Deleted formula shift.1, which reduced to `true'.
LP0.1.219: qed
All conjectures have been proved.
LP0.1.220:
LP0.1.221: set name simplify
The name-prefix is now `simplify'.
LP0.1.222: declare variables p: pred [S]
LP0.1.223: prove K (true) & p: pred [S] = p
Attempting to prove conjecture simplify.1: (K(true) & p):pred[S] = p
Conjecture simplify.1
[] Proved by normalization.
Deleted formula simplify.1, which reduced to `true'.
LP0.1.224: qed
All conjectures have been proved.
LP0.1.225:
LP0.1.226: % L1: Rules Used in Transformation, SimpLits
LP0.1.227: % ------------------------------------------
LP0.1.228:
LP0.1.229: set name SL1
The name-prefix is now `SL1'.
LP0.1.230: declare variables h: fun [T, U], f: fun [U, V], g: fun [U, W]
LP0.1.231: prove \< f \circ h, g \circ h \> = \< f, g \> \circ h
Attempting to prove conjecture SL1.1:
\ = \ \circ h
Conjecture SL1.1
[] Proved by normalization.
Deleted formula SL1.1, which reduced to `true'.
LP0.1.232: qed
All conjectures have been proved.
LP0.1.233:
LP0.1.234: set name SL2
The name-prefix is now `SL2'.
LP0.1.235: declare variables x: U, y: V
LP0.1.236: prove \< K (x), K (y) \> = K ([x, y])
Attempting to prove conjecture SL2.1: \ = K([x, y])
Conjecture SL2.1
[] Proved by normalization.
Deleted formula SL2.1, which reduced to `true'.
LP0.1.237: qed
All conjectures have been proved.
LP0.1.238:
LP0.1.239: set name SL3
The name-prefix is now `SL3'.
LP0.1.240: declare variables x: V, f: fun [T, U]
LP0.1.241: prove \< f, K (x) \> = \< id, K (x) \> \circ f
Attempting to prove conjecture SL3.1: \ = \ \circ f
Conjecture SL3.1
[] Proved by normalization.
Deleted formula SL3.1, which reduced to `true'.
LP0.1.242: qed
All conjectures have been proved.
LP0.1.243:
LP0.1.244: set name SL4
The name-prefix is now `SL4'.
LP0.1.245: declare variables x: V, f: fun [T, U]
LP0.1.246: prove \< K (x), f \> = \< K (x), id \> \circ f
Attempting to prove conjecture SL4.1: \ = \ \circ f
Conjecture SL4.1
[] Proved by normalization.
Deleted formula SL4.1, which reduced to `true'.
LP0.1.247: qed
All conjectures have been proved.
LP0.1.248:
LP0.1.249: set name SL5
The name-prefix is now `SL5'.
LP0.1.250: declare variables h: fun [T, U], g: fun [U, V], f: fun [V, W]
LP0.1.251: prove f \circ (g \circ h) = (f \circ g) \circ h
Attempting to prove conjecture SL5.1: f \circ (g \circ h) = f \circ g \circ h
Conjecture SL5.1
[] Proved by normalization.
Deleted formula SL5.1, which reduced to `true'.
LP0.1.252: qed
All conjectures have been proved.
LP0.1.253:
LP0.1.254: set name SL6
The name-prefix is now `SL6'.
LP0.1.255: declare variables x: U, f: fun [U, V]
LP0.1.256: prove f:fun [U, V] \circ K (x) = K (f:fun [U, V] ! x)
Attempting to prove conjecture SL6.1:
(f \circ K(x)):fun[T, V] = K(f:fun[U, V] ! x)
Conjecture SL6.1
[] Proved by normalization.
Deleted formula SL6.1, which reduced to `true'.
LP0.1.257: qed
All conjectures have been proved.
LP0.1.258:
LP0.1.259: set name SL7
The name-prefix is now `SL7'.
LP0.1.260: declare variables g: fun [T, U], f: fun [U, V], p: pred [V]
LP0.1.261: prove p \oplus (f \circ g) = (p \oplus f) \oplus g
Attempting to prove conjecture SL7.1:
p \oplus (f \circ g) = p \oplus f \oplus g
Conjecture SL7.1
[] Proved by normalization.
Deleted formula SL7.1, which reduced to `true'.
LP0.1.262: qed
All conjectures have been proved.
LP0.1.263:
LP0.1.264: set name SL8
The name-prefix is now `SL8'.
LP0.1.265: declare variables x: U, p: pred [U]
LP0.1.266: prove p: pred [U] \oplus K (x) = K (p: pred [U] ? x)
Attempting to prove conjecture SL8.1:
(p:pred[U] \oplus K(x)):pred[T] = K(p:pred[U] ? x)
Conjecture SL8.1
[] Proved by normalization.
Deleted formula SL8.1, which reduced to `true'.
LP0.1.267: qed
All conjectures have been proved.
LP0.1.268:
LP0.1.269: % L1: Rules Used in Transformation, OrderConjs
LP0.1.270: % --------------------------------------------
LP0.1.271:
LP0.1.272: set name OC1
The name-prefix is now `OC1'.
LP0.1.273: declare variables
p: pred [T], q: pred [U], r: pred [pair [T, U]], s: pred [T]
..
LP0.1.274: prove
(p \oplus fst) & (q \oplus snd) & r & (s \oplus fst) =
((p & s) \oplus fst) & (q \oplus snd) & r
..
Attempting to prove conjecture OC1.1:
(p \oplus fst) & (q \oplus snd) & r & (s \oplus fst)
= ((p & s) \oplus fst) & (q \oplus snd) & r
Conjecture OC1.1
[] Proved by normalization.
Deleted formula OC1.1, which reduced to `true'.
LP0.1.275: qed
All conjectures have been proved.
LP0.1.276:
LP0.1.277: set name OC2
The name-prefix is now `OC2'.
LP0.1.278: declare variables p: pred [T], q: pred [U], r: pred [pair [T, U]], s: pred [U]
LP0.1.279: prove
(p \oplus fst) & (q \oplus snd) & r & (s \oplus snd) =
(p \oplus fst) & ((q & s) \oplus snd) & r
..
Attempting to prove conjecture OC2.1:
(p \oplus fst) & (q \oplus snd) & r & (s \oplus snd)
= (p \oplus fst) & ((q & s) \oplus snd) & r
Conjecture OC2.1
[] Proved by normalization.
Deleted formula OC2.1, which reduced to `true'.
LP0.1.280: qed
All conjectures have been proved.
LP0.1.281:
LP0.1.282: set name OC3
The name-prefix is now `OC3'.
LP0.1.283: declare variables p: pred [T], q: pred [U], r, s: pred [pair [T, U]]
LP0.1.284: prove
(p \oplus fst) & (q \oplus snd) & r & s =
(p \oplus fst) & (q \oplus snd) & (r & s)
..
Attempting to prove conjecture OC3.1:
(p \oplus fst) & (q \oplus snd) & r & s
= (p \oplus fst) & (q \oplus snd) & (r & s)
Conjecture OC3.1
[] Proved by normalization.
Deleted formula OC3.1, which reduced to `true'.
LP0.1.285: qed
All conjectures have been proved.
LP0.1.286:
LP0.1.287:
LP0.1.288:
LP0.1.289: % Section 3: Predicate Pushdown
LP0.1.290: %
LP0.1.291: % Proof Scripts for COKO Transformation,
LP0.1.292: %
LP0.1.293: % TRANSFORMATION Pushdown
LP0.1.294: % USES
LP0.1.295: % SNF,
LP0.1.296: % push: join ((p OPLUS #1) & (q OPLUS #2) & r, f) ! [A, B] -->
LP0.1.297: % join (r, f) ! [iterate (p, id) ! A, iterate (q, id) ! B],
LP0.1.298: % simp: iterate (K (true), id) ! A --> A
LP0.1.299: %
LP0.1.300: % BEGIN
LP0.1.301: % GIVEN join (p, _F) ! _O DO {
LP0.1.302: % SNF (p);
LP0.1.303: % push;
LP0.1.304: % GIVEN join (_P, _F) ! [A, B] DO {
LP0.1.305: % simp (A);
LP0.1.306: % simp (B)
LP0.1.307: % }
LP0.1.308: % }
LP0.1.309: % END
LP0.1.310: %
LP0.1.311: % In [CZ98a], only rules push and simp are described.
LP0.1.312: %
LP0.1.313:
LP0.1.314: clear
LP0.1.315: forget
Critical pair list cleared.
LP0.1.316: unregister registry
LP0.1.317: set order manual
The ordering-method is now `manual'.
LP0.1.318: exec-silently Pushdown_Aux_Axioms
End of input from file `/pro/oodb/specs/KOLA98/Pushdown_Aux_Axioms.lp'.
LP0.1.319: declare variables
p: pred [T1],
p: pred [T2],
q: pred [T2],
x: T1,
y: T2,
r: pred [pair [T1, T2]],
f: fun [pair [T1, T2], U],
f, g: fun [T2, T2],
A: bag [T1],
B: bag [T2]
..
LP0.1.320:
LP0.1.321:
LP0.1.322: register height [__,__]:T2,T1->pair[T2, T1] = [__,__]:T1,T2->pair[T1, T2]
Registry extended.
LP0.1.323: register height
?:pred[pair[T2, T1]],pair[T2, T1]->Bool =
?:pred[pair[T1, T2]],pair[T1, T2]->Bool
..
Registry extended.
LP0.1.324: register height ?:pred[T1],T1->Bool = ?:pred[pair[T2, T1]],pair[T2, T1]->Bool
Registry extended.
LP0.1.325: register height ?:pred[T1],T1->Bool > [__,__]:T2,T1->pair[T2, T1]
Registry extended.
LP0.1.326: register height ?:pred[T2],T2->Bool = ?:pred[pair[T1, T2]],pair[T1, T2]->Bool
Registry extended.
LP0.1.327: register height ?:pred[T2],T2->Bool > [__,__]:T1,T2->pair[T1, T2]
Registry extended.
LP0.1.328: register height
!:fun[bag[T2], bag[T2]],bag[T2]->bag[T2] =
!:fun[bag[T2], bag[U]],bag[T2]->bag[U]
..
Registry extended.
LP0.1.329: register height
C:pred[pair[T1, T2]],T1->pred[T2] >
(&:pred[T2],pred[T2]->pred[T2],
\circ:fun[bag[T2], bag[U]],fun[bag[T2], bag[T2]]->fun[bag[T2], bag[U]],
iterate:pred[T2],fun[T2, U]->fun[bag[T2], bag[U]],
iterate:pred[T2],fun[T2, T2]->fun[bag[T2], bag[T2]])
..
Registry extended.
LP0.1.330: register height
&:pred[T2],pred[T2]->pred[T2] =
\circ:fun[bag[T2], bag[U]],fun[bag[T2], bag[T2]]->fun[bag[T2], bag[U]] =
iterate:pred[T2],fun[T2, U]->fun[bag[T2], bag[U]]
..
Registry extended.
LP0.1.331: register height
&:pred[T2],pred[T2]->pred[T2] >=
iterate:pred[T2],fun[T2, T2]->fun[bag[T2], bag[T2]]
..
Registry extended.
LP0.1.332: register stat L
=>, !:fun[bag[T2], bag[U]],bag[T2]->bag[U],
!:fun[bag[T2], bag[T2]],bag[T2]->bag[T2], &:pred[T2],pred[T2]->pred[T2],
\circ:fun[bag[T2], bag[U]],fun[bag[T2], bag[T2]]->fun[bag[T2], bag[U]]
..
LP0.1.333: register stat R
iterate:pred[T2],fun[T2, U]->fun[bag[T2], bag[U]]
..
LP0.1.334: register stat multiset /\, \/, <=>
LP0.1.335: register stat L
=>, ?:pred[pair[T1, T2]],pair[T1, T2]->Bool,
?:pred[pair[T2, T1]],pair[T2, T1]->Bool
..
LP0.1.336: register stat multiset /\, \/, <=>, [__,__]:T2,T1->pair[T2, T1]
LP0.1.337:
LP0.1.338:
LP0.1.339: set order noeq-dsmpos
The ordering-method is now `noeq-dsmpos'.
LP0.1.340: order *
The formulas cannot be ordered using the current ordering.
LP0.1.341: make immune formulas
LP0.1.342:
LP0.1.343: % L1: Lemmas for Transformation, Pushdown
LP0.1.344: % ---------------------------------------
LP0.1.345:
LP0.1.346: declare variables
p: pred [T1],
p: pred [T2],
q: pred [T2],
x: T1,
y: T2,
r: pred [pair [T1, T2]],
f: fun [pair [T1, T2], U],
f, g: fun [T2, T2],
A: bag [T1],
B: bag [T2]
..
LP0.1.347:
LP0.1.348: % ----------------------------------------------------------
LP0.1.349: set immunity on
The immunity is now `on'.
LP0.1.350: set name pdLemma1
The name-prefix is now `pdLemma1'.
LP0.1.351: prove C (p & q, x) = (C (p, x) & C (q, x))
Attempting to prove conjecture pdLemma1.1: C(p & q, x) = C(p, x) & C(q, x)
Conjecture pdLemma1.1
[] Proved by normalization.
The formulas cannot be ordered using the current ordering.
LP0.1.352: qed
All conjectures have been proved.
LP0.1.353: % ----------------------------------------------------------
LP0.1.354:
LP0.1.355: % ----------------------------------------------------------
LP0.1.356: set name pdLemma2
The name-prefix is now `pdLemma2'.
LP0.1.357: prove C (p \oplus fst, x) = K (p:pred[T1] ? x)
Attempting to prove conjecture pdLemma2.1:
C(p \oplus fst, x) = K(p:pred[T1] ? x)
Conjecture pdLemma2.1
[] Proved by normalization.
The formulas cannot be ordered using the current ordering.
LP0.1.358: qed
All conjectures have been proved.
LP0.1.359: % ----------------------------------------------------------
LP0.1.360:
LP0.1.361: % ----------------------------------------------------------
LP0.1.362: set name pdLemma3
The name-prefix is now `pdLemma3'.
LP0.1.363: prove C (p \oplus snd, x) = p
Attempting to prove conjecture pdLemma3.1: C(p \oplus snd, x) = p
Conjecture pdLemma3.1
[] Proved by normalization.
The formulas cannot be ordered using the current ordering.
LP0.1.364: qed
All conjectures have been proved.
LP0.1.365: % ----------------------------------------------------------
LP0.1.366:
LP0.1.367: % ----------------------------------------------------------
LP0.1.368: set name pdLemma4
The name-prefix is now `pdLemma4'.
LP0.1.369: prove iterate (p & q, f) = iterate (p, f) \circ iterate (q, id)
Attempting to prove conjecture pdLemma4.1:
iterate(p & q, f) = iterate(p, f) \circ iterate(q, id)
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture pdLemma4.1
LP0.1.370: resume by induction on x:bag[T2]
Creating subgoals for proof by structural induction on `x:bag[T2]'
Basis subgoal:
Subgoal 1: (iterate(p & q, f) ! {}):bag[U]
= iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! {})
Induction constant: xc
Induction hypothesis:
pdLemma4InductHyp.1:
(iterate(p & q, f) ! xc):bag[U] = iterate(p, f) ! (iterate(q, id) ! xc)
Induction subgoal:
Subgoal 2: (iterate(p & q, f) ! insert(t, xc)):bag[U]
= iterate(p, f) ! (iterate(q, id) ! insert(t, xc))
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on x
Level 2 subgoal 1 (basis step) for proof by induction on x
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on x
Added hypothesis pdLemma4InductHyp.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 2 subgoal 2 (induction step) for proof by induction
on x
LP0.1.371: resume by cases q ? t
Creating subgoals for proof by cases
New constants: qc, tc
Case hypotheses:
pdLemma4CaseHyp.1.1: qc ? tc
pdLemma4CaseHyp.1.2: ~(qc ? tc)
Same subgoal for all cases:
(iterate(p & qc, f) ! insert(tc, xc)):bag[U]
= iterate(p, f) ! (iterate(qc, id) ! insert(tc, xc))
Attempting to prove level 3 subgoal for case 1 (out of 2)
Added hypothesis pdLemma4CaseHyp.1.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 3 subgoal for case 1 (out of 2)
LP0.1.372: resume by cases p ? tc
Creating subgoals for proof by cases
New constant: pc
Case hypotheses:
pdLemma4CaseHyp.2.1: pc ? tc
pdLemma4CaseHyp.2.2: ~(pc ? tc)
Same subgoal for all cases:
(iterate(pc & qc, f) ! insert(tc, xc)):bag[U]
= iterate(pc, f) ! insert(tc, iterate(qc, id) ! xc)
Attempting to prove level 4 subgoal for case 1 (out of 2)
Added hypothesis pdLemma4CaseHyp.2.1 to the system.
Level 4 subgoal for case 1 (out of 2)
[] Proved by normalization.
Attempting to prove level 4 subgoal for case 2 (out of 2)
Added hypothesis pdLemma4CaseHyp.2.2 to the system.
Level 4 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 3 subgoal for case 1 (out of 2)
[] Proved by cases p ? tc.
Attempting to prove level 3 subgoal for case 2 (out of 2)
Added hypothesis pdLemma4CaseHyp.1.2 to the system.
Level 3 subgoal for case 2 (out of 2):
(iterate(p & qc, f) ! insert(tc, xc)):bag[U]
= iterate(p, f) ! (iterate(qc, id) ! insert(tc, xc))
[] Proved by normalization.
Level 2 subgoal 2 (induction step) for proof by induction on x:
(iterate(p & q, f) ! insert(t, xc)):bag[U]
= iterate(p, f) ! (iterate(q, id) ! insert(t, xc))
[] Proved by cases q ? t.
Conjecture pdLemma4.1: iterate(p & q, f) = iterate(p, f) \circ iterate(q, id)
[] Proved by structural induction on `x:bag[T2]'.
The formulas cannot be ordered using the current ordering.
LP0.1.373: qed
All conjectures have been proved.
LP0.1.374: % ----------------------------------------------------------
LP0.1.375:
LP0.1.376:
LP0.1.377: % ----------------------------------------------------------
LP0.1.378: set name pdLemma5
The name-prefix is now `pdLemma5'.
LP0.1.379: prove
iterate (q & (p:pred[T2] \oplus g:fun[T2,T2]), f \circ g) ! B =
iterate (p, f:fun[T2,T2]) ! (iterate (q:pred[T2], g) ! B)
..
Attempting to prove conjecture pdLemma5.1:
(iterate(q & (p:pred[T2] \oplus g), f \circ g) ! B):bag[T2]
= iterate(p, f) ! (iterate(q, g) ! B)
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture pdLemma5.1
LP0.1.380: resume by induction on B:bag[T2]
Creating subgoals for proof by structural induction on `B:bag[T2]'
Basis subgoal:
Subgoal 1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! {}):bag[T2]
= iterate(p, f) ! (iterate(q, g) ! {})
Induction constant: Bc
Induction hypothesis:
pdLemma5InductHyp.1:
(iterate(q & (p:pred[T2] \oplus g), f \circ g) ! Bc):bag[T2]
= iterate(p, f) ! (iterate(q, g) ! Bc)
Induction subgoal:
Subgoal 2: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! insert(t, Bc)):
bag[T2]
= iterate(p, f) ! (iterate(q, g) ! insert(t, Bc))
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on B
Level 2 subgoal 1 (basis step) for proof by induction on B
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on B
Added hypothesis pdLemma5InductHyp.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 2 subgoal 2 (induction step) for proof by induction
on B
LP0.1.381: resume by cases q ? t
Creating subgoals for proof by cases
New constants: qc, tc
Case hypotheses:
pdLemma5CaseHyp.1.1: qc ? tc
pdLemma5CaseHyp.1.2: ~(qc ? tc)
Same subgoal for all cases:
(iterate(qc & (p:pred[T2] \oplus g), f \circ g) ! insert(tc, Bc)):bag[T2]
= iterate(p, f) ! (iterate(qc, g) ! insert(tc, Bc))
Attempting to prove level 3 subgoal for case 1 (out of 2)
Added hypothesis pdLemma5CaseHyp.1.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 3 subgoal for case 1 (out of 2)
LP0.1.382: resume by cases p:pred[T2] ? (g ! tc)
Creating subgoals for proof by cases
New constants: pc, gc
Case hypotheses:
pdLemma5CaseHyp.2.1: pc ? (gc ! tc)
pdLemma5CaseHyp.2.2: ~(pc ? (gc ! tc))
Same subgoal for all cases:
(iterate(qc & (pc \oplus gc), f \circ gc) ! insert(tc, Bc)):bag[T2]
= iterate(pc, f) ! insert(gc ! tc, iterate(qc, gc) ! Bc)
Attempting to prove level 4 subgoal for case 1 (out of 2)
Added hypothesis pdLemma5CaseHyp.2.1 to the system.
Level 4 subgoal for case 1 (out of 2)
[] Proved by normalization.
Attempting to prove level 4 subgoal for case 2 (out of 2)
Added hypothesis pdLemma5CaseHyp.2.2 to the system.
Level 4 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 3 subgoal for case 1 (out of 2)
[] Proved by cases p:pred[T2] ? (g ! tc).
Attempting to prove level 3 subgoal for case 2 (out of 2)
Added hypothesis pdLemma5CaseHyp.1.2 to the system.
Level 3 subgoal for case 2 (out of 2):
(iterate(qc & (p:pred[T2] \oplus g), f \circ g) ! insert(tc, Bc)):bag[T2]
= iterate(p, f) ! (iterate(qc, g) ! insert(tc, Bc))
[] Proved by normalization.
Level 2 subgoal 2 (induction step) for proof by induction on B:
(iterate(q & (p:pred[T2] \oplus g), f \circ g) ! insert(t, Bc)):bag[T2]
= iterate(p, f) ! (iterate(q, g) ! insert(t, Bc))
[] Proved by cases q ? t.
Conjecture pdLemma5.1:
(iterate(q & (p:pred[T2] \oplus g), f \circ g) ! B):bag[T2]
= iterate(p, f) ! (iterate(q, g) ! B)
[] Proved by structural induction on `B:bag[T2]'.
The formulas cannot be ordered using the current ordering.
LP0.1.383: qed
All conjectures have been proved.
LP0.1.384: % ----------------------------------------------------------
LP0.1.385:
LP0.1.386:
LP0.1.387: % ----------------------------------------------------------
LP0.1.388: set name pdLemma6
The name-prefix is now `pdLemma6'.
LP0.1.389: prove
iterate (q & (p:pred[T2] \oplus g:fun[T2,T2]), f \circ g) ! B =
iterate (p, f:fun[T2,U]) ! (iterate (q:pred[T2], g) ! B)
..
Attempting to prove conjecture pdLemma6.1:
(iterate(q & (p:pred[T2] \oplus g), f \circ g) ! B):bag[U]
= iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, g) ! B)
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture pdLemma6.1
LP0.1.390: resume by induction on B:bag[T2]
Creating subgoals for proof by structural induction on `B:bag[T2]'
Basis subgoal:
Subgoal 1: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! {}):bag[U]
= iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, g) ! {})
Induction constant: Bc
Induction hypothesis:
pdLemma6InductHyp.1:
(iterate(q & (p:pred[T2] \oplus g), f \circ g) ! Bc):bag[U]
= iterate(p, f) ! (iterate(q, g) ! Bc)
Induction subgoal:
Subgoal 2: (iterate(q & (p:pred[T2] \oplus g), f \circ g) ! insert(t, Bc)):
bag[U]
= iterate(p, f) ! (iterate(q, g) ! insert(t, Bc))
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on B
Level 2 subgoal 1 (basis step) for proof by induction on B
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on B
Added hypothesis pdLemma6InductHyp.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 2 subgoal 2 (induction step) for proof by induction
on B
LP0.1.391: resume by cases q ? t
Creating subgoals for proof by cases
New constants: qc, tc
Case hypotheses:
pdLemma6CaseHyp.1.1: qc ? tc
pdLemma6CaseHyp.1.2: ~(qc ? tc)
Same subgoal for all cases:
(iterate(qc & (p:pred[T2] \oplus g), f \circ g) ! insert(tc, Bc)):bag[U]
= iterate(p, f) ! (iterate(qc, g) ! insert(tc, Bc))
Attempting to prove level 3 subgoal for case 1 (out of 2)
Added hypothesis pdLemma6CaseHyp.1.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 3 subgoal for case 1 (out of 2)
LP0.1.392: resume by cases p:pred[T2] ? (g ! tc)
Creating subgoals for proof by cases
New constants: pc, gc
Case hypotheses:
pdLemma6CaseHyp.2.1: pc ? (gc ! tc)
pdLemma6CaseHyp.2.2: ~(pc ? (gc ! tc))
Same subgoal for all cases:
(iterate(qc & (pc \oplus gc), f \circ gc) ! insert(tc, Bc)):bag[U]
= iterate(pc, f) ! insert(gc ! tc, iterate(qc, gc) ! Bc)
Attempting to prove level 4 subgoal for case 1 (out of 2)
Added hypothesis pdLemma6CaseHyp.2.1 to the system.
Level 4 subgoal for case 1 (out of 2)
[] Proved by normalization.
Attempting to prove level 4 subgoal for case 2 (out of 2)
Added hypothesis pdLemma6CaseHyp.2.2 to the system.
Level 4 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 3 subgoal for case 1 (out of 2)
[] Proved by cases p:pred[T2] ? (g ! tc).
Attempting to prove level 3 subgoal for case 2 (out of 2)
Added hypothesis pdLemma6CaseHyp.1.2 to the system.
Level 3 subgoal for case 2 (out of 2):
(iterate(qc & (p:pred[T2] \oplus g), f \circ g) ! insert(tc, Bc)):bag[U]
= iterate(p, f) ! (iterate(qc, g) ! insert(tc, Bc))
[] Proved by normalization.
Level 2 subgoal 2 (induction step) for proof by induction on B:
(iterate(q & (p:pred[T2] \oplus g), f \circ g) ! insert(t, Bc)):bag[U]
= iterate(p, f) ! (iterate(q, g) ! insert(t, Bc))
[] Proved by cases q ? t.
Conjecture pdLemma6.1:
(iterate(q & (p:pred[T2] \oplus g), f \circ g) ! B):bag[U]
= iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, g) ! B)
[] Proved by structural induction on `B:bag[T2]'.
The formulas cannot be ordered using the current ordering.
LP0.1.393: qed
All conjectures have been proved.
LP0.1.394: % ----------------------------------------------------------
LP0.1.395:
LP0.1.396: % ----------------------------------------------------------
LP0.1.397: set name pdLemma7
The name-prefix is now `pdLemma7'.
LP0.1.398: prove
iterate (p:pred[T2], f:fun[T2,U]) ! (iterate (q:pred[T2],id) ! B) =
iterate (q, f:fun[T2,U]) ! (iterate (p, id) ! B) by induction on B:bag[T2]
..
Attempting to prove conjecture pdLemma7.1:
(iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! B)):bag[U]
= iterate(q, f):fun[bag[T2], bag[U]] ! (iterate(p, id) ! B)
Creating subgoals for proof by structural induction on `B:bag[T2]'
Basis subgoal:
Subgoal 1: (iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! {})):
bag[U]
= iterate(q, f):fun[bag[T2], bag[U]] ! (iterate(p, id) ! {})
Induction constant: Bc
Induction hypothesis:
pdLemma7InductHyp.1:
(iterate(p, f) ! (iterate(q, id) ! Bc)):bag[U]
= iterate(q, f) ! (iterate(p, id) ! Bc)
Induction subgoal:
Subgoal 2: (iterate(p, f) ! (iterate(q, id) ! insert(t, Bc))):bag[U]
= iterate(q, f) ! (iterate(p, id) ! insert(t, Bc))
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on B
Level 2 subgoal 1 (basis step) for proof by induction on B
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on B
Added hypothesis pdLemma7InductHyp.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 2 subgoal 2 (induction step) for proof by induction
on B
LP0.1.399: resume by cases q ? t
Creating subgoals for proof by cases
New constants: qc, tc
Case hypotheses:
pdLemma7CaseHyp.1.1: qc ? tc
pdLemma7CaseHyp.1.2: ~(qc ? tc)
Same subgoal for all cases:
(iterate(p, f) ! (iterate(qc, id) ! insert(tc, Bc))):bag[U]
= iterate(qc, f) ! (iterate(p, id) ! insert(tc, Bc))
Attempting to prove level 3 subgoal for case 1 (out of 2)
Added hypothesis pdLemma7CaseHyp.1.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 3 subgoal for case 1 (out of 2)
LP0.1.400: resume by cases p ? tc
Creating subgoals for proof by cases
New constant: pc
Case hypotheses:
pdLemma7CaseHyp.2.1: pc ? tc
pdLemma7CaseHyp.2.2: ~(pc ? tc)
Same subgoal for all cases:
(iterate(pc, f) ! insert(tc, iterate(qc, id) ! Bc)):bag[U]
= iterate(qc, f) ! (iterate(pc, id) ! insert(tc, Bc))
Attempting to prove level 4 subgoal for case 1 (out of 2)
Added hypothesis pdLemma7CaseHyp.2.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 4 subgoal for case 1 (out of 2)
LP0.1.401: instan p by pc, q by qc, B by Bc in *Induct*
Formula pdLemma7InductHyp.1 has been instantiated to formula
pdLemma7InductHyp.1.1,
(iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U]
= iterate(qc, f) ! (iterate(pc, id) ! Bc)
Level 4 subgoal for case 1 (out of 2)
[] Proved by normalization.
Attempting to prove level 4 subgoal for case 2 (out of 2)
Added hypothesis pdLemma7CaseHyp.2.2 to the system.
The formulas cannot be ordered using the current ordering.
LP0.1.402: instan p by pc, q by qc, B by Bc in *Induct*
Formula pdLemma7InductHyp.1 has been instantiated to formula
pdLemma7InductHyp.1.1,
(iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U]
= iterate(qc, f) ! (iterate(pc, id) ! Bc)
Level 4 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 3 subgoal for case 1 (out of 2):
(iterate(p, f) ! (iterate(qc, id) ! insert(tc, Bc))):bag[U]
= iterate(qc, f) ! (iterate(p, id) ! insert(tc, Bc))
[] Proved by cases p ? tc.
Attempting to prove level 3 subgoal for case 2 (out of 2):
(iterate(p, f) ! (iterate(qc, id) ! insert(tc, Bc))):bag[U]
= iterate(qc, f) ! (iterate(p, id) ! insert(tc, Bc))
Added hypothesis pdLemma7CaseHyp.1.2 to the system.
The formulas cannot be ordered using the current ordering.
LP0.1.403: resume by cases p ? tc
Creating subgoals for proof by cases
New constant: pc
Case hypotheses:
pdLemma7CaseHyp.2.1: pc ? tc
pdLemma7CaseHyp.2.2: ~(pc ? tc)
Same subgoal for all cases:
(iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U]
= iterate(qc, f) ! (iterate(pc, id) ! insert(tc, Bc))
Attempting to prove level 4 subgoal for case 1 (out of 2)
Added hypothesis pdLemma7CaseHyp.2.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 4 subgoal for case 1 (out of 2)
LP0.1.404: instan p by pc, q by qc, B by Bc in *Induct*
Formula pdLemma7InductHyp.1 has been instantiated to formula
pdLemma7InductHyp.1.1,
(iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U]
= iterate(qc, f) ! (iterate(pc, id) ! Bc)
Level 4 subgoal for case 1 (out of 2)
[] Proved by normalization.
Attempting to prove level 4 subgoal for case 2 (out of 2)
Added hypothesis pdLemma7CaseHyp.2.2 to the system.
The formulas cannot be ordered using the current ordering.
LP0.1.405: instan p by pc, q by qc, B by Bc in *Induct*
Formula pdLemma7InductHyp.1 has been instantiated to formula
pdLemma7InductHyp.1.1,
(iterate(pc, f) ! (iterate(qc, id) ! Bc)):bag[U]
= iterate(qc, f) ! (iterate(pc, id) ! Bc)
Level 4 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 3 subgoal for case 2 (out of 2):
(iterate(p, f) ! (iterate(qc, id) ! insert(tc, Bc))):bag[U]
= iterate(qc, f) ! (iterate(p, id) ! insert(tc, Bc))
[] Proved by cases p ? tc.
Level 2 subgoal 2 (induction step) for proof by induction on B:
(iterate(p, f) ! (iterate(q, id) ! insert(t, Bc))):bag[U]
= iterate(q, f) ! (iterate(p, id) ! insert(t, Bc))
[] Proved by cases q ? t.
Conjecture pdLemma7.1:
(iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! B)):bag[U]
= iterate(q, f):fun[bag[T2], bag[U]] ! (iterate(p, id) ! B)
[] Proved by structural induction on `B:bag[T2]'.
The formulas cannot be ordered using the current ordering.
LP0.1.406: qed
All conjectures have been proved.
LP0.1.407: make immune formulas
LP0.1.408: % ----------------------------------------------------------
LP0.1.409:
LP0.1.410: % ----------------------------------------------------------
LP0.1.411: set name pdLemma8
The name-prefix is now `pdLemma8'.
LP0.1.412: prove K (true) & p:pred[T2] = p
Attempting to prove conjecture pdLemma8.1: K(true) & p = p
Conjecture pdLemma8.1
[] Proved by normalization.
The formulas cannot be ordered using the current ordering.
LP0.1.413: qed
All conjectures have been proved.
LP0.1.414: % ----------------------------------------------------------
LP0.1.415:
LP0.1.416: % ----------------------------------------------------------
LP0.1.417: set name pdLemma9
The name-prefix is now `pdLemma9'.
LP0.1.418: prove K (false) & p:pred[T2] = K (false)
Attempting to prove conjecture pdLemma9.1: K(false) & p = K(false)
Conjecture pdLemma9.1
[] Proved by normalization.
The formulas cannot be ordered using the current ordering.
LP0.1.419: qed
All conjectures have been proved.
LP0.1.420: % ----------------------------------------------------------
LP0.1.421:
LP0.1.422: % ----------------------------------------------------------
LP0.1.423: set name pdLemma10
The name-prefix is now `pdLemma10'.
LP0.1.424: prove iterate (K (false), f:fun[T2,U]) ! B = {} by induction on B:bag[T2]
Attempting to prove conjecture pdLemma10.1:
(iterate(K(false), f) ! B):bag[U] = {}
Creating subgoals for proof by structural induction on `B:bag[T2]'
Basis subgoal:
Subgoal 1: (iterate(K(false), f) ! {}):bag[U] = {}
Induction constant: Bc
Induction hypothesis:
pdLemma10InductHyp.1: (iterate(K(false), f) ! Bc):bag[U] = {}
Induction subgoal:
Subgoal 2: (iterate(K(false), f) ! insert(t, Bc)):bag[U] = {}
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on B
Level 2 subgoal 1 (basis step) for proof by induction on B
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on B
Added hypothesis pdLemma10InductHyp.1 to the system.
Level 2 subgoal 2 (induction step) for proof by induction on B
[] Proved by normalization.
Conjecture pdLemma10.1
[] Proved by structural induction on `B:bag[T2]'.
The formulas cannot be ordered using the current ordering.
LP0.1.425: qed
All conjectures have been proved.
LP0.1.426: set immunity off
The immunity is now `off'.
LP0.1.427:
LP0.1.428:
LP0.1.429: % L1: Rules Used in Transformation, Pushdown
LP0.1.430: % ------------------------------------------
LP0.1.431:
LP0.1.432: set name push
The name-prefix is now `push'.
LP0.1.433:
LP0.1.434: make passive formulas
LP0.1.435: set order left
Warning: the rewriting system is known to terminate, but its termination cannot
be verified with the `left-to-right' ordering. When another rewrite rule is
added, the rewriting system will be treated as nonterminating.
The ordering-method is now `left-to-right'.
LP0.1.436:
LP0.1.437: prove
join ((p \oplus fst) & (q \oplus snd) & r, f) ! [A, B] =
join (r, f) ! [iterate (p, id) ! A, iterate (q, id) ! B]
..
Attempting to prove conjecture push.1:
join((p \oplus fst) & (q \oplus snd) & r, f) ! [A, B]
= join(r, f) ! [iterate(p, id) ! A, iterate(q, id) ! B]
The system now contains 173 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
Suspending proof of conjecture push.1
LP0.1.438:
LP0.1.439: resume by induction on A:bag[T1]
Creating subgoals for proof by structural induction on `A:bag[T1]'
Basis subgoal:
Subgoal 1: join((p \oplus fst) & (q \oplus snd) & r, f) ! [{}, B]
= join(r, f) ! [iterate(p, id) ! {}, iterate(q, id) ! B]
Induction constant: Ac
Induction hypothesis:
pushInductHyp.1:
join((p \oplus fst) & (q \oplus snd) & r, f) ! [Ac, B]
= join(r, f) ! [iterate(p, id) ! Ac, iterate(q, id) ! B]
Induction subgoal:
Subgoal 2: join((p \oplus fst) & (q \oplus snd) & r, f) ! [insert(t, Ac), B]
= join(r, f)
! [iterate(p, id) ! insert(t, Ac), iterate(q, id) ! B]
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A
Level 2 subgoal 1 (basis step) for proof by induction on A
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on A
Added hypothesis pushInductHyp.1 to the system.
The system now contains 174 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
Suspending proof of level 2 subgoal 2 (induction step) for proof by induction
on A
LP0.1.440:
LP0.1.441: % Base Case: Trivial
LP0.1.442: % Inductive Case:
LP0.1.443:
LP0.1.444: resume by cases p ? t
Creating subgoals for proof by cases
New constants: pc, tc
Case hypotheses:
pushCaseHyp.1.1: pc ? tc
pushCaseHyp.1.2: ~(pc ? tc)
Same subgoal for all cases:
(iterate(K(pc ? tc) & q & C(r, tc), C(f, tc)) ! B)
\U (join(r, f) ! [iterate(pc, id) ! Ac, iterate(q, id) ! B])
= join(r, f) ! [iterate(pc, id) ! insert(tc, Ac), iterate(q, id) ! B]
Attempting to prove level 3 subgoal for case 1 (out of 2)
Added hypothesis pushCaseHyp.1.1 to the system.
The system now contains 175 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
Suspending proof of level 3 subgoal for case 1 (out of 2)
LP0.1.445:
LP0.1.446: % Case 1: p ? t
LP0.1.447:
LP0.1.448: set order noeq
The ordering-method is now `noeq-dsmpos'.
LP0.1.449:
LP0.1.450: crit-pairs *Lemma* with Composition
The following equations are critical pairs between rewrite rules pdLemma4.1 and
Composition.2.
push.2:
(iterate(p & q, f) ! x):bag[U]
= iterate(p, f):fun[bag[T2], bag[U]] ! (iterate(q, id) ! x)
The system now contains 1 formula and 175 rewrite rules. The rewriting system
is NOT guaranteed to terminate.
The system now contains 176 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
LP0.1.451: norm conjecture
Level 3 subgoal for case 1 (out of 2):
(iterate(K(pc ? tc) & q & C(r, tc), C(f, tc)) ! B)
\U (join(r, f) ! [iterate(pc, id) ! Ac, iterate(q, id) ! B])
= join(r, f) ! [iterate(pc, id) ! insert(tc, Ac), iterate(q, id) ! B]
[] Proved by normalization.
Attempting to prove level 3 subgoal for case 2 (out of 2):
(iterate(K(pc ? tc) & q & C(r, tc), C(f, tc)) ! B)
\U (join(r, f) ! [iterate(pc, id) ! Ac, iterate(q, id) ! B])
= join(r, f) ! [iterate(pc, id) ! insert(tc, Ac), iterate(q, id) ! B]
Added hypothesis pushCaseHyp.1.2 to the system.
Level 3 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 2 subgoal 2 (induction step) for proof by induction on A:
join((p \oplus fst) & (q \oplus snd) & r, f) ! [insert(t, Ac), B]
= join(r, f) ! [iterate(p, id) ! insert(t, Ac), iterate(q, id) ! B]
[] Proved by cases p ? t.
Conjecture push.1:
join((p \oplus fst) & (q \oplus snd) & r, f) ! [A, B]
= join(r, f) ! [iterate(p, id) ! A, iterate(q, id) ! B]
[] Proved by structural induction on `A:bag[T1]'.
The system now contains 174 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
LP0.1.452:
LP0.1.453: % Case 2: ~ (p ? t)
LP0.1.454:
LP0.1.455: qed
All conjectures have been proved.
LP0.1.456: make immune formulas
LP0.1.457: set order noeq
The ordering-method is now `noeq-dsmpos'.
LP0.1.458:
LP0.1.459: set name simp
The name-prefix is now `simp'.
LP0.1.460: prove iterate (K (true), id) ! A = A
Attempting to prove conjecture simp.1: iterate(K(true), id) ! A = A
Suspending proof of conjecture simp.1
LP0.1.461: resume by induction on A:bag[T2]
Creating subgoals for proof by structural induction on `A:bag[T2]'
Basis subgoal:
Subgoal 1: iterate(K(true), id) ! {} = {}
Induction constant: Ac
Induction hypothesis:
simpInductHyp.1: iterate(K(true), id) ! Ac = Ac
Induction subgoal:
Subgoal 2: iterate(K(true), id) ! insert(t, Ac) = insert(t, Ac)
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A
Level 2 subgoal 1 (basis step) for proof by induction on A
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on A
Added hypothesis simpInductHyp.1 to the system.
Level 2 subgoal 2 (induction step) for proof by induction on A
[] Proved by normalization.
Conjecture simp.1
[] Proved by structural induction on `A:bag[T2]'.
The system now contains 175 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
LP0.1.462: qed
All conjectures have been proved.
LP0.1.463:
LP0.1.464:
LP0.1.465: % Section 4: SNF2
LP0.1.466: %
LP0.1.467: % Proof Scripts for COKO Transformations:
LP0.1.468: %
LP0.1.469: % TRANSFORMATION SNF2
LP0.1.470: % USES
LP0.1.471: % SimpLits2,
LP0.1.472: % CNF,
LP0.1.473: % OrderConjs2,
LP0.1.474: % pushneg: ~ (p OPLUS f) --> (~ (p)) OPLUS f,
LP0.1.475: % init: p --> (K (true) OPLUS (id X #1)) &
LP0.1.476: % (K (true) OPLUS (id X #2)) &
LP0.1.477: % K (true) & p,
LP0.1.478: % pull: (p OPLUS f) | (q OPLUS f) --> (p | q) OPLUS f,
LP0.1.479: % shift: p & (q & r) --> (p & r) & q,
LP0.1.480: % simplify: K (true) & p --> p
LP0.1.481: % BEGIN
LP0.1.482: % SimpLits2;
LP0.1.483: % CNF;
LP0.1.484: % TD {pushneg};
LP0.1.485: % init;
LP0.1.486: % BU {pull || {REPEAT shift}};
LP0.1.487: % OrderConjs2;
LP0.1.488: % BU {simplify}
LP0.1.489: % END
LP0.1.490: %
LP0.1.491: % TRANSFORMATION SimpLits2
LP0.1.492: % USES
LP0.1.493: % SL11: --> K ([x, y]),
LP0.1.494: % SL12: f o K (x) --> K (f ! x),
LP0.1.495: % SL13: --> o f,
LP0.1.496: % SL14: --> o f,
LP0.1.497: % SL21: --> o h,
LP0.1.498: % SL22: --> o (id X h),
LP0.1.499: % SL23: --> o (id X h),
LP0.1.500: % SL24: --> o (id X h),
LP0.1.501: % SL25: --> o (id X h),
LP0.1.502: % SL26: --> o #2,
LP0.1.503: % SL27: --> o #2
LP0.1.504: % Shft,
LP0.1.505: % Pr2Times,
LP0.1.506: % PR1: p OPLUS (f o g) --> p OPLUS f OPLUS g,
LP0.1.507: % PR2: p OPLUS K (x) --> K (p ? x)
LP0.1.508: % BEGIN
LP0.1.509: % BU {Pr2Times ||
LP0.1.510: % SL11 || SL12 || {{SL13 || SL14} -> Shft} ||
LP0.1.511: % SL21 || SL22 || SL23 || SL24 || SL25 || SL26 || SL27 ||
LP0.1.512: % Shft};
LP0.1.513: % BU {PR1 || PR2}
LP0.1.514: % END
LP0.1.515: %
LP0.1.516: % TRANSFORMATION Pr2Times
LP0.1.517: % USES
LP0.1.518: % CO1: --> (f X g) o (id X h),
LP0.1.519: % CO2: --> <#2, #1> o (g X f) o (id X h),
LP0.1.520: % CO3: --> (f X g) o #2,
LP0.1.521: % CO4: --> <#2, #1> o (g X f) o #2,
LP0.1.522: % CO5: --> (f X id) o (id X g),
LP0.1.523: % CO6: --> <#2, #1> o (g X id) o (id X f),
LP0.1.524: % CO7: <#1, #2> --> id,
LP0.1.525: % CO8: f o id --> f,
LP0.1.526: % CO9: id o f --> f
LP0.1.527: % BEGIN
LP0.1.528: % CO1 || CO2 || CO3 || CO4 || CO5 || CO6 || CO7 || CO8 || CO9
LP0.1.529: % END
LP0.1.530: %
LP0.1.531: % TRANSFORMATION Shft
LP0.1.532: % USES
LP0.1.533: % SL1: f o #1 o #2 --> f o (#1 o #2),
LP0.1.534: % SL2: f o #2 o #2 --> f o (#2 o #2),
LP0.1.535: % SL3: f o (g o h) --> (f o g) o h
LP0.1.536: % BEGIN
LP0.1.537: % REPEAT SL3;
LP0.1.538: % {SL1 || SL2}
LP0.1.539: % END
LP0.1.540: %
LP0.1.541: % TRANSFORMATION OrderConjs2
LP0.1.542: % USES
LP0.1.543: % OC1: (p OPLUS (id X #1)) & q & r & (r' OPLUS (id X #1)) -->
LP0.1.544: % ((p & r') OPLUS (id X #1)) & q & r,
LP0.1.545: % OC2: p & (q OPLUS (id X #2)) & r & (r' OPLUS (id X #2)) -->
LP0.1.546: % p & ((q & r') OPLUS (id X #2)) & r,
LP0.1.547: % OC3: p & q & r & r' --> p & q & (r & r')
LP0.1.548: % BEGIN
LP0.1.549: % BU {OC1 || OC2 || OC3}
LP0.1.550: % END
LP0.1.551: %
LP0.1.552: % In [CZ98a], the effects of SNF2 are described but the transformations
LP0.1.553: % themselves are not presented. The effect of SNF2 on any predicate, p is
LP0.1.554: % to rewrite p to the form,
LP0.1.555: %
LP0.1.556: % (\rho OPLUS (id \times fst)) & (\sigma OPLUS (id \times snd)) & \tau
LP0.1.557: %
LP0.1.558: % See Section 2 for proofs of rewrite rules:
LP0.1.559: %
LP0.1.560: % pushneg, pull, shift, simplify (from SNF2),
LP0.1.561: % SL11 (SL2 in Section 2), SL12 (SL6 in Section 2), SL13 (SL3 in Section 2),
LP0.1.562: % SL14 (SL4 in Section 2), SL21 (SL1 in Section 2), PR1 (SL7 in Section 2),
LP0.1.563: % and PR2 (SL8 in Section 2) (from SimpLits2), and
LP0.1.564: % OC3 (from OrderConjs2)
LP0.1.565: %
LP0.1.566:
LP0.1.567: clear
LP0.1.568: forget
Critical pair list cleared.
LP0.1.569: unregister registry
LP0.1.570: set order manual
The ordering-method is now `manual'.
LP0.1.571: exec-silently SNF2_Aux_Axioms
End of input from file `/pro/oodb/specs/KOLA98/SNF2_Aux_Axioms.lp'.
LP0.1.572: set order noeq-dsmpos
The ordering-method is now `noeq-dsmpos'.
LP0.1.573: order *
The system now contains 170 rewrite rules. The rewriting system is guaranteed
to terminate.
All equations have been oriented into rewrite rules. The rewriting system is
guaranteed to terminate.
LP0.1.574:
LP0.1.575: % L1: Rules Used in Transformation, SNF2
LP0.1.576: % --------------------------------------
LP0.1.577:
LP0.1.578: set name init
The name-prefix is now `init'.
LP0.1.579: declare variables p: pred [pair [T1, pair [T2, T3]]]
LP0.1.580: prove
p = (K (true) \oplus (id \times fst)) &
(K (true) \oplus (id \times snd)) &
K (true) & p
..
Attempting to prove conjecture init.1:
p
= (K(true) \oplus (id \times fst))
& (K(true) \oplus (id \times snd))
& K(true)
& p
Conjecture init.1
[] Proved by normalization.
Deleted formula init.1, which reduced to `true'.
LP0.1.581: qed
All conjectures have been proved.
LP0.1.582:
LP0.1.583:
LP0.1.584: % L1: Rules Used in Transformation, SimpLits2
LP0.1.585: % -------------------------------------------
LP0.1.586:
LP0.1.587: set name SL22
The name-prefix is now `SL22'.
LP0.1.588: declare variables
f: fun [T1, U],
h: fun [T2, V],
g: fun [pair [T1, V], W]
..
LP0.1.589: prove
\ =
\ \circ (id \times h)
..
Attempting to prove conjecture SL22.1:
\
= \ \circ (id \times h)
Suspending proof of conjecture SL22.1
LP0.1.590: declare operator
one: pair [T1, T2] -> T1,
two: pair [T1, T2] -> T2
..
LP0.1.591: set immunity on
The immunity is now `on'.
LP0.1.592: instan
pr:pair[T1,T2] by x
in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool)
..
Formula Pairs.1 has been instantiated to formula Pairs.1.1,
\E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y])
Deleted rewrite rule Pairs.1, which reduced to `true'.
LP0.1.593: set immunity off
The immunity is now `off'.
LP0.1.594:
LP0.1.595: fix
x:T1 as one (x:pair[T1,T2])
in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool)
..
A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to
produce formula SL22.2,
\E y:T2 (x:pair[T1, T2] = [one(x), y])
The system now contains 171 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.596:
LP0.1.597: fix
y:T2 as two (x:pair[T1,T2])
in SL22 / contains-operator (one: pair [T1, T2] -> T1)
..
A prenex-existential quantifier in formula SL22.2 has been eliminated to
produce formula SL22.3,
x = [one(x), two(x)]
The system now contains 172 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.598:
LP0.1.599: crit-pairs SL22 with ProductsF
The following equations are critical pairs between rewrite rules SL22.3 and
ProductsF.1.
SL22.4: ((f \times g) ! x):pair[T1, V] = [f ! one(x), g ! two(x)]
The system now contains 1 formula and 172 rewrite rules. The rewriting system
is guaranteed to terminate.
LP0.1.600: crit-pairs SL22 with Projection
The following equations are critical pairs between rewrite rules SL22.3 and
Projection.4.
SL22.5: snd ! x = two(x)
The system now contains 2 formulas and 172 rewrite rules. The rewriting system
is guaranteed to terminate.
The following equations are critical pairs between rewrite rules SL22.3 and
Projection.3.
SL22.6: fst:fun[pair[T1, T2], T1] ! x = one(x)
The system now contains 1 formula and 174 rewrite rules. The rewriting system
is guaranteed to terminate.
Critical pair computation abandoned because a theorem has been proved.
Conjecture SL22.1:
\
= \ \circ (id \times h)
[] Proved by normalization.
The system now contains 171 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.601: qed
All conjectures have been proved.
LP0.1.602:
LP0.1.603: set name SL23
The name-prefix is now `SL23'.
LP0.1.604: declare variables
f: fun [pair [T1, V], W],
h: fun [T2, V],
g: fun [T1, U]
..
LP0.1.605: prove
\ =
\ \circ (id \times h)
..
Attempting to prove conjecture SL23.1:
\
= \ \circ (id \times h)
Conjecture SL23.1
[] Proved by normalization.
Deleted formula SL23.1, which reduced to `true'.
LP0.1.606: qed
All conjectures have been proved.
LP0.1.607:
LP0.1.608: set name SL24
The name-prefix is now `SL24'.
LP0.1.609: declare variables
f: fun [V, W],
h: fun [T2, V],
g: fun [pair [T1, V], U]
..
LP0.1.610: prove
\ =
\ \circ (id \times h)
..
Attempting to prove conjecture SL24.1:
\
= \ \circ (id \times h)
Suspending proof of conjecture SL24.1
LP0.1.611: declare operator
one: pair [T1, T2] -> T1,
two: pair [T1, T2] -> T2
..
LP0.1.612: set immunity on
The immunity is now `on'.
LP0.1.613: instan
pr:pair[T1,T2] by x
in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool)
..
Formula Pairs.1 has been instantiated to formula Pairs.1.1,
\E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y])
Deleted rewrite rule Pairs.1, which reduced to `true'.
LP0.1.614: set immunity off
The immunity is now `off'.
LP0.1.615:
LP0.1.616: fix
x:T1 as one (x:pair[T1,T2])
in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool)
..
A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to
produce formula SL24.2,
\E y:T2 (x:pair[T1, T2] = [one(x), y])
The system now contains 172 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.617:
LP0.1.618: fix
y:T2 as two (x:pair[T1,T2])
in SL24 / contains-operator (one: pair [T1, T2] -> T1)
..
A prenex-existential quantifier in formula SL24.2 has been eliminated to
produce formula SL24.3,
x = [one(x), two(x)]
The system now contains 173 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.619:
LP0.1.620: crit-pairs SL24 with ProductsF
The following equations are critical pairs between rewrite rules SL24.3 and
ProductsF.1.
SL24.4: ((f \times g) ! x):pair[T1, V] = [f ! one(x), g ! two(x)]
The system now contains 1 formula and 173 rewrite rules. The rewriting system
is guaranteed to terminate.
LP0.1.621: crit-pairs SL24 with Projection
The following equations are critical pairs between rewrite rules SL24.3 and
Projection.4.
SL24.5: snd ! x = two(x)
The system now contains 2 formulas and 173 rewrite rules. The rewriting system
is guaranteed to terminate.
Critical pair computation abandoned because a theorem has been proved.
Conjecture SL24.1:
\
= \ \circ (id \times h)
[] Proved by normalization.
The system now contains 172 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.622: qed
All conjectures have been proved.
LP0.1.623:
LP0.1.624: set name SL25
The name-prefix is now `SL25'.
LP0.1.625: declare variables
f: fun [pair [T1, V], W],
h: fun [T2, V],
g: fun [pair [T1, V], U]
..
LP0.1.626: prove
\ =
\ \circ (id \times h)
..
Attempting to prove conjecture SL25.1:
\
= \ \circ (id \times h)
Conjecture SL25.1
[] Proved by normalization.
Deleted formula SL25.1, which reduced to `true'.
LP0.1.627: qed
All conjectures have been proved.
LP0.1.628:
LP0.1.629: set name SL26
The name-prefix is now `SL26'.
LP0.1.630: declare variables
f: fun [U, W],
h: fun [T2, V],
g: fun [T2, U]
..
LP0.1.631: prove
\ =
\ \circ snd
..
Attempting to prove conjecture SL26.1:
\
= \ \circ snd
Conjecture SL26.1
[] Proved by normalization.
Deleted formula SL26.1, which reduced to `true'.
LP0.1.632: qed
All conjectures have been proved.
LP0.1.633:
LP0.1.634: set name SL27
The name-prefix is now `SL27'.
LP0.1.635: declare variables
f: fun [T2, W],
h: fun [U, V],
g: fun [T2, U]
..
LP0.1.636: prove
\ =
\ \circ snd
..
Attempting to prove conjecture SL27.1:
\ = \ \circ snd
Conjecture SL27.1
[] Proved by normalization.
Deleted formula SL27.1, which reduced to `true'.
LP0.1.637: qed
All conjectures have been proved.
LP0.1.638:
LP0.1.639:
LP0.1.640:
LP0.1.641: % L1: Rules Used in Transformation, Pr2Times
LP0.1.642: % ------------------------------------------
LP0.1.643:
LP0.1.644: set name CO1
The name-prefix is now `CO1'.
LP0.1.645: declare variables
f: fun [T1, U],
h: fun [T2, V],
g: fun [V, W]
..
LP0.1.646: prove
\ =
(f \times g) \circ (id \times h)
..
Attempting to prove conjecture CO1.1:
\ = (f \times g) \circ (id \times h)
Suspending proof of conjecture CO1.1
LP0.1.647: declare operator
one: pair [T1, T2] -> T1,
two: pair [T1, T2] -> T2
..
LP0.1.648: set immunity on
The immunity is now `on'.
LP0.1.649: instan
pr:pair[T1,T2] by x
in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool)
..
Formula Pairs.1 has been instantiated to formula Pairs.1.1,
\E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y])
Deleted rewrite rule Pairs.1, which reduced to `true'.
LP0.1.650: set immunity off
The immunity is now `off'.
LP0.1.651:
LP0.1.652: fix
x:T1 as one (x:pair[T1,T2])
in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool)
..
A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to
produce formula CO1.2,
\E y:T2 (x:pair[T1, T2] = [one(x), y])
The system now contains 173 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.653:
LP0.1.654: fix
y:T2 as two (x:pair[T1,T2])
in CO1 / contains-operator (one: pair [T1, T2] -> T1)
..
A prenex-existential quantifier in formula CO1.2 has been eliminated to produce
formula CO1.3,
x = [one(x), two(x)]
The system now contains 174 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.655:
LP0.1.656: crit-pairs CO1 with ProductsF
The following equations are critical pairs between rewrite rules CO1.3 and
ProductsF.1.
CO1.4: ((f \times g) ! x):pair[T1, V] = [f ! one(x), g ! two(x)]
The system now contains 1 formula and 174 rewrite rules. The rewriting system
is guaranteed to terminate.
Deduction rule lp_and_is_true has been applied to formula ProductsF.1 to yield
the following formulas, which imply ProductsF.1.
ProductsF.1.1: (f:fun[T1, T1] ! x):T1 = f ! one([x, y])
ProductsF.1.2: (g:fun[T2, V] ! y):V = g ! two([x, y])
Critical pair computation abandoned because a theorem has been proved.
Conjecture CO1.1:
\ = (f \times g) \circ (id \times h)
[] Proved by normalization.
The system now contains 173 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.657: qed
All conjectures have been proved.
LP0.1.658:
LP0.1.659: set name CO2
The name-prefix is now `CO2'.
LP0.1.660: declare variables
f: fun [V, W],
h: fun [T2, V],
g: fun [T1, U]
..
LP0.1.661: prove
\ =
\ \circ (g \times f) \circ (id \times h)
..
Attempting to prove conjecture CO2.1:
\
= \ \circ (g \times f) \circ (id \times h)
Conjecture CO2.1
[] Proved by normalization.
Deleted formula CO2.1, which reduced to `true'.
LP0.1.662: qed
All conjectures have been proved.
LP0.1.663:
LP0.1.664: set name CO3
The name-prefix is now `CO3'.
LP0.1.665: declare variables
f: fun [T2, V],
g: fun [T4, U]
..
LP0.1.666: prove
\ =
(f:fun [T2, V] \times g:fun [T4, U]) \circ snd
..
Attempting to prove conjecture CO3.1:
\ = (f \times g) \circ snd
Suspending proof of conjecture CO3.1
LP0.1.667: declare operator
one: pair [pair [T1, T3], pair[T2, T4]] -> pair[T1, T3],
two: pair [pair [T1, T3], pair[T2, T4]] -> pair[T2, T4],
one: pair [T1, T3] -> T1,
two: pair [T1, T3] -> T3,
one: pair [T2, T4] -> T2,
two: pair [T2, T4] -> T4
..
LP0.1.668: set immunity on
The immunity is now `on'.
LP0.1.669: instan
pr:pair [pair [T1, T3], pair[T2, T4]] by x
in Pairs / contains-oper (=:pair [pair [T1,T3], pair[T2,T4]],
pair [pair [T1,T3], pair[T2,T4]] -> Bool)
..
Formula Pairs.13 has been instantiated to formula Pairs.13.1,
\E x:pair[T1, T3] \E y:pair[T2, T4]
(x:pair[pair[T1, T3], pair[T2, T4]] = [x, y])
Deleted rewrite rule Pairs.13, which reduced to `true'.
LP0.1.670: set immunity off
The immunity is now `off'.
LP0.1.671: fix
x as one (x:pair [pair [T1, T3], pair[T2, T4]])
in Pairs / contains-oper (=:pair [pair [T1,T3], pair[T2,T4]],
pair [pair [T1,T3], pair[T2,T4]] -> Bool)
..
A prenex-existential quantifier in formula Pairs.13.1 has been eliminated to
produce formula CO3.2,
\E y:pair[T2, T4] (x:pair[pair[T1, T3], pair[T2, T4]] = [one(x), y])
The system now contains 174 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.672: fix
y as two (x:pair [pair [T1, T3], pair[T2, T4]])
in CO3 / contains-oper (one: pair [pair [T1,T3], pair[T2,T4]] ->
pair [T1,T3])
..
A prenex-existential quantifier in formula CO3.2 has been eliminated to produce
formula CO3.3,
x:pair[pair[T1, T3], pair[T2, T4]] = [one(x), two(x)]
The system now contains 175 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.673:
LP0.1.674: set immunity on
The immunity is now `on'.
LP0.1.675: instan
pr:pair[T1,T3] by x
in Pairs / contains-operator (=:pair[T1,T3],pair[T1,T3]->Bool)
..
Formula Pairs.5 has been instantiated to formula Pairs.5.1,
\E x:T1 \E y:T3 (x:pair[T1, T3] = [x, y])
Deleted rewrite rule Pairs.5, which reduced to `true'.
LP0.1.676: set immunity off
The immunity is now `off'.
LP0.1.677:
LP0.1.678: fix
x:T1 as one (x:pair[T1,T3])
in Pairs / contains-operator (=:pair[T1, T3],pair[T1, T3]->Bool)
..
A prenex-existential quantifier in formula Pairs.5.1 has been eliminated to
produce formula CO3.4,
\E y:T3 (x:pair[T1, T3] = [one(x), y])
The system now contains 176 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.679:
LP0.1.680: fix
y as two (x:pair[T1,T3])
in CO3 / contains-operator (one: pair [T1, T3] -> T1)
..
A prenex-existential quantifier in formula CO3.4 has been eliminated to produce
formula CO3.5,
x:pair[T1, T3] = [one(x), two(x)]
The system now contains 177 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.681:
LP0.1.682: set immunity on
The immunity is now `on'.
LP0.1.683: instan
pr:pair[T2,T4] by x
in Pairs / contains-operator (=:pair[T2,T4],pair[T2,T4]->Bool)
..
Formula Pairs.7 has been instantiated to formula Pairs.7.1,
\E x:T2 \E y:T4 (x:pair[T2, T4] = [x, y])
Deleted rewrite rule Pairs.7, which reduced to `true'.
LP0.1.684: set immunity off
The immunity is now `off'.
LP0.1.685:
LP0.1.686: fix
x:T2 as one (x:pair[T2,T4])
in Pairs / contains-operator (=:pair[T2, T4],pair[T2, T4]->Bool)
..
A prenex-existential quantifier in formula Pairs.7.1 has been eliminated to
produce formula CO3.6,
\E y:T4 (x:pair[T2, T4] = [one(x), y])
The system now contains 178 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.687:
LP0.1.688: fix
y:T4 as two (x:pair[T2,T4])
in CO3 / contains-operator (one: pair [T2, T4] -> T2)
..
A prenex-existential quantifier in formula CO3.6 has been eliminated to produce
formula CO3.7,
x:pair[T2, T4] = [one(x), two(x)]
The system now contains 179 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.689:
LP0.1.690: crit-pairs CO3 with Projection
The following equations are critical pairs between rewrite rules CO3.3 and
Projection.16.
CO3.8: (snd ! x):pair[T2, T4] = two(x)
The system now contains 1 formula and 179 rewrite rules. The rewriting system
is guaranteed to terminate.
The following equations are critical pairs between rewrite rules CO3.3 and
Projection.15.
CO3.9: (fst ! x):pair[T1, T3] = one(x)
The system now contains 1 formula and 180 rewrite rules. The rewriting system
is guaranteed to terminate.
The following equations are critical pairs between rewrite rules CO3.7 and
Projection.8.
CO3.10: (snd ! x):T4 = two(x)
The system now contains 1 formula and 181 rewrite rules. The rewriting system
is guaranteed to terminate.
The following equations are critical pairs between rewrite rules CO3.7 and
Projection.7.
CO3.11: (fst:fun[pair[T2, T4], T2] ! x):T2 = one(x)
The system now contains 1 formula and 182 rewrite rules. The rewriting system
is guaranteed to terminate.
The system now contains 183 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.691: crit-pairs CO3 with ProductsF
The following equations are critical pairs between rewrite rules CO3.7 and
ProductsF.2.
CO3.12: ((f \times g) ! x):pair[V, U] = [f ! one(x), g ! two(x)]
The system now contains 1 formula and 183 rewrite rules. The rewriting system
is guaranteed to terminate.
Critical pair computation abandoned because a theorem has been proved.
Conjecture CO3.1:
\ = (f \times g) \circ snd
[] Proved by normalization.
The system now contains 174 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.692: qed
All conjectures have been proved.
LP0.1.693:
LP0.1.694:
LP0.1.695: set name CO4
The name-prefix is now `CO4'.
LP0.1.696: declare variables
g: fun [T2, V],
f: fun [T4, U]
..
LP0.1.697: prove
\ =
\ \circ (g:fun [T2, V] \times f:fun [T4, U]) \circ snd
..
Attempting to prove conjecture CO4.1:
\
= \ \circ (g \times f) \circ snd
Conjecture CO4.1
[] Proved by normalization.
Deleted formula CO4.1, which reduced to `true'.
LP0.1.698: qed
All conjectures have been proved.
LP0.1.699:
LP0.1.700: set name CO5
The name-prefix is now `CO5'.
LP0.1.701: declare variables
g: fun [T2, V],
f: fun [T1, U]
..
LP0.1.702: prove \ = (f \times id) \circ (id \times g)
Attempting to prove conjecture CO5.1:
\ = (f \times id) \circ (id \times g)
Suspending proof of conjecture CO5.1
LP0.1.703: declare operator
one: pair [T1, T2] -> T1,
two: pair [T1, T2] -> T2
..
LP0.1.704: set immunity on
The immunity is now `on'.
LP0.1.705: instan
pr:pair[T1,T2] by x
in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool)
..
Formula Pairs.1 has been instantiated to formula Pairs.1.1,
\E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y])
Deleted rewrite rule Pairs.1, which reduced to `true'.
LP0.1.706: set immunity off
The immunity is now `off'.
LP0.1.707:
LP0.1.708: fix
x:T1 as one (x:pair[T1,T2])
in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool)
..
A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to
produce formula CO5.2,
\E y:T2 (x:pair[T1, T2] = [one(x), y])
The system now contains 175 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.709:
LP0.1.710: fix
y:T2 as two (x:pair[T1,T2])
in CO5 / contains-operator (one: pair [T1, T2] -> T1)
..
A prenex-existential quantifier in formula CO5.2 has been eliminated to produce
formula CO5.3,
x = [one(x), two(x)]
The system now contains 176 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.711:
LP0.1.712: crit-pairs CO5 with ProductsF
The following equations are critical pairs between rewrite rules CO5.3 and
ProductsF.1.
CO5.4: ((f \times g) ! x):pair[T1, V] = [f ! one(x), g ! two(x)]
The system now contains 1 formula and 176 rewrite rules. The rewriting system
is guaranteed to terminate.
Deduction rule lp_and_is_true has been applied to formula ProductsF.1 to yield
the following formulas, which imply ProductsF.1.
ProductsF.1.1: (f:fun[T1, T1] ! x):T1 = f ! one([x, y])
ProductsF.1.2: (g:fun[T2, V] ! y):V = g ! two([x, y])
Deleted formula CO1.1, which reduced to `true'.
The system now contains 177 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.713: crit-pairs CO5 with Projection
The following equations are critical pairs between rewrite rules CO5.3 and
Projection.4.
CO5.5: snd ! x = two(x)
The system now contains 1 formula and 177 rewrite rules. The rewriting system
is guaranteed to terminate.
Critical pair computation abandoned because a theorem has been proved.
Conjecture CO5.1:
\ = (f \times id) \circ (id \times g)
[] Proved by normalization.
The system now contains 175 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.714: qed
All conjectures have been proved.
LP0.1.715:
LP0.1.716: set name CO6
The name-prefix is now `CO6'.
LP0.1.717: declare variables
f: fun [T2, V],
g: fun [T1, U]
..
LP0.1.718: prove
\ =
\ \circ (g \times id) \circ (id \times f)
..
Attempting to prove conjecture CO6.1:
\
= \ \circ (g \times id) \circ (id \times f)
Conjecture CO6.1
[] Proved by normalization.
Deleted formula CO6.1, which reduced to `true'.
LP0.1.719: qed
All conjectures have been proved.
LP0.1.720:
LP0.1.721: set name CO7
The name-prefix is now `CO7'.
LP0.1.722: prove \ = id
Attempting to prove conjecture CO7.1: \ = id
Suspending proof of conjecture CO7.1
LP0.1.723: declare operator
one: pair [T1, T2] -> T1,
two: pair [T1, T2] -> T2
..
LP0.1.724: set immunity on
The immunity is now `on'.
LP0.1.725: instan
pr:pair[T1,T2] by x
in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool)
..
Formula Pairs.1 has been instantiated to formula Pairs.1.1,
\E x:T1 \E y:T2 (x:pair[T1, T2] = [x, y])
Deleted rewrite rule Pairs.1, which reduced to `true'.
LP0.1.726: set immunity off
The immunity is now `off'.
LP0.1.727: fix
x:T1 as one (x:pair[T1,T2])
in Pairs / contains-operator (=:pair[T1,T2],pair[T1,T2]->Bool)
..
A prenex-existential quantifier in formula Pairs.1.1 has been eliminated to
produce formula CO7.2,
\E y:T2 (x:pair[T1, T2] = [one(x), y])
The system now contains 176 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.728: fix
y:T2 as two (x:pair[T1,T2])
in CO7 / contains-operator (one: pair [T1, T2] -> T1)
..
A prenex-existential quantifier in formula CO7.2 has been eliminated to produce
formula CO7.3,
x = [one(x), two(x)]
The system now contains 177 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.729: crit-pairs CO7 with Projection
The following equations are critical pairs between rewrite rules CO7.3 and
Projection.4.
CO7.4: snd ! x = two(x)
The system now contains 1 formula and 177 rewrite rules. The rewriting system
is guaranteed to terminate.
The following equations are critical pairs between rewrite rules CO7.3 and
Projection.3.
CO7.5: fst:fun[pair[T1, T2], T1] ! x = one(x)
The system now contains 1 formula and 178 rewrite rules. The rewriting system
is guaranteed to terminate.
Critical pair computation abandoned because a theorem has been proved.
Conjecture CO7.1: \ = id
[] Proved by normalization.
The system now contains 176 rewrite rules. The rewriting system is guaranteed
to terminate.
LP0.1.730: qed
All conjectures have been proved.
LP0.1.731:
LP0.1.732: set name CO8
The name-prefix is now `CO8'.
LP0.1.733: declare variables f: fun [T2, V]
LP0.1.734: prove f \circ id = f
Attempting to prove conjecture CO8.1: f \circ id = f
Conjecture CO8.1
[] Proved by normalization.
Deleted formula CO8.1, which reduced to `true'.
LP0.1.735: qed
All conjectures have been proved.
LP0.1.736:
LP0.1.737: set name CO9
The name-prefix is now `CO9'.
LP0.1.738: declare variables f: fun [T2, V]
LP0.1.739: prove id \circ f = f
Attempting to prove conjecture CO9.1: id \circ f = f
Conjecture CO9.1
[] Proved by normalization.
Deleted formula CO9.1, which reduced to `true'.
LP0.1.740: qed
All conjectures have been proved.
LP0.1.741:
LP0.1.742:
LP0.1.743: % L1: Rules Used in Transformation, Shft
LP0.1.744: % --------------------------------------
LP0.1.745:
LP0.1.746: set name SL1
The name-prefix is now `SL1'.
LP0.1.747: declare variables
f: fun [T2, V]
..
LP0.1.748: prove f \circ fst \circ snd = f \circ (fst \circ snd)
Attempting to prove conjecture SL1.1:
f \circ fst \circ snd = f \circ (fst \circ snd)
Conjecture SL1.1
[] Proved by normalization.
Deleted formula SL1.1, which reduced to `true'.
LP0.1.749: qed
All conjectures have been proved.
LP0.1.750:
LP0.1.751: set name SL2
The name-prefix is now `SL2'.
LP0.1.752: declare variables
f: fun [T4, V]
..
LP0.1.753: prove f \circ snd \circ snd = f \circ (snd \circ snd)
Attempting to prove conjecture SL2.1:
f \circ snd \circ snd = f \circ (snd \circ snd)
Conjecture SL2.1
[] Proved by normalization.
Deleted formula SL2.1, which reduced to `true'.
LP0.1.754: qed
All conjectures have been proved.
LP0.1.755:
LP0.1.756: set name SL3
The name-prefix is now `SL3'.
LP0.1.757: declare variables
h: fun [T2, U],
g: fun [U, V],
f: fun [V, W]
..
LP0.1.758: prove f \circ (g:fun [U, V] \circ h) = (f \circ g) \circ h
Attempting to prove conjecture SL3.1:
f \circ (g:fun[U, V] \circ h) = f \circ g \circ h
Conjecture SL3.1
[] Proved by normalization.
Deleted formula SL3.1, which reduced to `true'.
LP0.1.759: qed
All conjectures have been proved.
LP0.1.760:
LP0.1.761:
LP0.1.762: % L1: Rules Used in Transformation, OrderConjs2
LP0.1.763: % ---------------------------------------------
LP0.1.764:
LP0.1.765: set name OC1
The name-prefix is now `OC1'.
LP0.1.766: declare variables
p, r': pred [pair [T1, T2]],
q, r: pred [pair [T1, pair [T2, T3]]]
..
LP0.1.767: prove
(p \oplus (id \times fst)) & q & r & (r' \oplus (id \times fst)) =
((p & r') \oplus (id \times fst)) & q & r
..
Attempting to prove conjecture OC1.1:
(p \oplus (id \times fst)) & q & r & (r' \oplus (id \times fst))
= ((p & r') \oplus (id \times fst)) & q & r
Conjecture OC1.1
[] Proved by normalization.
Deleted formula OC1.1, which reduced to `true'.
LP0.1.768: qed
All conjectures have been proved.
LP0.1.769:
LP0.1.770: set name OC2
The name-prefix is now `OC2'.
LP0.1.771: declare variables
q, r': pred [pair [T1, T3]],
p, r: pred [pair [T1, pair [T2, T3]]]
..
LP0.1.772: prove
p & (q \oplus (id \times snd)) & r & (r' \oplus (id \times snd)) =
p & ((q & r') \oplus (id \times snd)) & r
..
Attempting to prove conjecture OC2.1:
p & (q \oplus (id \times snd)) & r & (r' \oplus (id \times snd))
= p & ((q & r') \oplus (id \times snd)) & r
Conjecture OC2.1
[] Proved by normalization.
Deleted formula OC2.1, which reduced to `true'.
LP0.1.773: qed
All conjectures have been proved.
LP0.1.774:
LP0.1.775:
LP0.1.776: % Section 5: Magic
LP0.1.777: %
LP0.1.778: % Proof Scripts for COKO Transformation,
LP0.1.779: %
LP0.1.780: % TRANSFORMATION Magic
LP0.1.781: % USES
LP0.1.782: % SNF2,
LP0.1.783: % Pushdown,
LP0.1.784: % SimplifyJoin,
LP0.1.785: % shift: p & q & r --> p & (q & r),
LP0.1.786: % nod: njoin (p, f, g) ! [set ! A, B] --> njoin (p, f, g) ! [A, B],
LP0.1.787: %
LP0.1.788: % magic: join (q OPLUS (id X #1) & r, f) !
LP0.1.789: % [A, njoin (p, g, h) ! [A', B]] -->
LP0.1.790: % join (q OPLUS (id X #1) & r, f) !
LP0.1.791: % [A, njoin (p, g, h) ! [set ! (join (q, #2) ! [A, A']), B]]
LP0.1.792: %
LP0.1.793: % BEGIN
LP0.1.794: % Pushdown;
LP0.1.795: %
LP0.1.796: % GIVEN join (p, _F) ! _O DO {
LP0.1.797: % SNF2 (p);
LP0.1.798: % shift (p);
LP0.1.799: % magic
LP0.1.800: % };
LP0.1.801: %
LP0.1.802: % GIVEN _F ! [_O, A], A = _F ! [B, _O] DO {
LP0.1.803: % SimplifyJoin (B);
LP0.1.804: % nod (A)
LP0.1.805: % }
LP0.1.806: %
LP0.1.807: % END
LP0.1.808: %
LP0.1.809: % In [CZ98a], only rule magic is described.
LP0.1.810: %
LP0.1.811:
LP0.1.812: clear
LP0.1.813: forget
Critical pair list cleared.
LP0.1.814: unregister registry
LP0.1.815: set order manual
The ordering-method is now `manual'.
LP0.1.816: exec-silently Magic_Aux_Axioms
End of input from file `/pro/oodb/specs/KOLA98/Magic_Aux_Axioms.lp'.
LP0.1.817: set order noeq-dsmpos
The ordering-method is now `noeq-dsmpos'.
LP0.1.818: order *
The formulas cannot be ordered using the current ordering.
LP0.1.819:
LP0.1.820: % L1: Lemmas for Transformation, Magic
LP0.1.821: % ------------------------------------
LP0.1.822:
LP0.1.823: set name magicLemma1
The name-prefix is now `magicLemma1'.
LP0.1.824:
LP0.1.825: declare variables
q: pred [pair [W, pair [T1, V]]],
f: fun [pair [W, pair [T1, V]], X],
A, B: bag [pair [W, pair [T1, V]]]
..
LP0.1.826: prove
iterate (p, f:fun [pair [W, pair [T1, V]], X]) ! (A \U B) =
(iterate (p, f:fun [pair [W, pair [T1, V]], X]) ! A) \U
(iterate (p, f:fun [pair [W, pair [T1, V]], X]) ! B)
..
Attempting to prove conjecture magicLemma1.1:
(iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (A \U B)):bag[X]
= (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! A)
\U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B)
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture magicLemma1.1
LP0.1.827:
LP0.1.828: resume by induction on A: bag [pair [W, pair [T1, V]]]
Creating subgoals for proof by structural induction on
`A:bag[pair[W, pair[T1, V]]]'
Basis subgoal:
Subgoal 1: (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]]
! ({} \U B)):
bag[X]
= (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! {})
\U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]]
! B)
Induction constant: Ac
Induction hypothesis:
magicLemma1InductHyp.1:
iterate(p, f) ! (Ac \U B)
= (iterate(p, f) ! Ac)
\U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B)
Induction subgoal:
Subgoal 2: iterate(p, f) ! (insert(p1, Ac) \U B)
= (iterate(p, f) ! insert(p1, Ac))
\U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]]
! B)
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A
Level 2 subgoal 1 (basis step) for proof by induction on A
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on A
Added hypothesis magicLemma1InductHyp.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 2 subgoal 2 (induction step) for proof by induction
on A
LP0.1.829:
LP0.1.830: % Base Case: Trivial
LP0.1.831: % Inductive Case
LP0.1.832: resume by cases p ? p1
Creating subgoals for proof by cases
New constants: pc, p1c
Case hypotheses:
magicLemma1CaseHyp.1.1: pc ? p1c
magicLemma1CaseHyp.1.2: ~(pc ? p1c)
Same subgoal for all cases:
iterate(pc, f) ! insert(p1c, Ac \U B)
= (iterate(pc, f) ! insert(p1c, Ac)) \U (iterate(pc, f) ! B)
Attempting to prove level 3 subgoal for case 1 (out of 2)
Added hypothesis magicLemma1CaseHyp.1.1 to the system.
Level 3 subgoal for case 1 (out of 2)
[] Proved by normalization.
Attempting to prove level 3 subgoal for case 2 (out of 2)
Added hypothesis magicLemma1CaseHyp.1.2 to the system.
Level 3 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 2 subgoal 2 (induction step) for proof by induction on A:
iterate(p, f) ! (insert(p1, Ac) \U B)
= (iterate(p, f) ! insert(p1, Ac))
\U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B)
[] Proved by cases p ? p1.
Conjecture magicLemma1.1:
(iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! (A \U B)):bag[X]
= (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! A)
\U (iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]] ! B)
[] Proved by structural induction on `A:bag[pair[W, pair[T1, V]]]'.
The formulas cannot be ordered using the current ordering.
LP0.1.833:
LP0.1.834: qed
All conjectures have been proved.
LP0.1.835: % ----------------------------------------------------------
LP0.1.836:
LP0.1.837: % ----------------------------------------------------------
LP0.1.838: set name magicLemma2
The name-prefix is now `magicLemma2'.
LP0.1.839: set immunity on
The immunity is now `on'.
LP0.1.840: declare variables
p, q: pred [pair [W, pair [T1, V]]],
x: W
..
LP0.1.841: prove C (p & q, x) = (C (p, x:W) & C (q, x:W))
Attempting to prove conjecture magicLemma2.1: C(p & q, x) = C(p, x) & C(q, x)
Conjecture magicLemma2.1
[] Proved by normalization.
The formulas cannot be ordered using the current ordering.
LP0.1.842: set immunity off
The immunity is now `off'.
LP0.1.843: qed
All conjectures have been proved.
LP0.1.844: % ----------------------------------------------------------
LP0.1.845:
LP0.1.846: % ----------------------------------------------------------
LP0.1.847: set name magicLemma3
The name-prefix is now `magicLemma3'.
LP0.1.848:
LP0.1.849: declare variables
q: pred [pair [T1, V]],
g: fun [pair [T1, V], pair [W, pair [T1, V]]],
p: pred [pair [W, pair [T1, V]]],
f: fun [pair [W, pair [T1, V]], X],
A: bag [pair [T1, V]]
..
LP0.1.850: prove
iterate (p, f:fun [pair [W, pair [T1, V]], X]) !
(iterate (q, g:fun [pair [T1, V], pair [W, pair [T1, V]]]) ! A) =
iterate (q & (p:pred [pair [W, pair [T1, V]]] \oplus g), f \circ g) ! A
..
Attempting to prove conjecture magicLemma3.1:
iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]]
! (iterate(q, g):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]] ! A)
= iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! A
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture magicLemma3.1
LP0.1.851:
LP0.1.852: resume by induction on A:bag [pair [T1, V]]
Creating subgoals for proof by structural induction on `A:bag[pair[T1, V]]'
Basis subgoal:
Subgoal 1: iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]]
! (iterate(q,
g):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]]
! {})
= iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g),
f \circ g)
! {}
Induction constant: Ac
Induction hypothesis:
magicLemma3InductHyp.1:
iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]]
! (iterate(q, g) ! Ac)
= iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! Ac
Induction subgoal:
Subgoal 2: iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]]
! (iterate(q, g) ! insert(p1, Ac))
= iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g),
f \circ g)
! insert(p1, Ac)
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A
Level 2 subgoal 1 (basis step) for proof by induction on A
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on A
Added hypothesis magicLemma3InductHyp.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 2 subgoal 2 (induction step) for proof by induction
on A
LP0.1.853:
LP0.1.854: % Base Case: Trivial
LP0.1.855: % Inductive Case
LP0.1.856:
LP0.1.857: resume by cases
(q & (p \oplus g:fun [pair [T1, V], pair [W, pair [T1, V]]])) ? p1
..
Creating subgoals for proof by cases
New constants: qc, pc, gc, p1c
Case hypotheses:
magicLemma3CaseHyp.1.1: (qc & (pc \oplus gc)) ? p1c
magicLemma3CaseHyp.1.2: ~((qc & (pc \oplus gc)) ? p1c)
Same subgoal for all cases:
iterate(pc, f) ! (iterate(qc, gc) ! insert(p1c, Ac))
= iterate(qc & (pc \oplus gc), f \circ gc) ! insert(p1c, Ac)
Attempting to prove level 3 subgoal for case 1 (out of 2)
Added hypothesis magicLemma3CaseHyp.1.1 to the system.
Deduction rule lp_and_is_true has been applied to formula
magicLemma3CaseHyp.1.1 to yield the following formulas, which imply
magicLemma3CaseHyp.1.1.
magicLemma3CaseHyp.1.1.1: qc ? p1c
magicLemma3CaseHyp.1.1.2: pc ? (gc ! p1c)
Level 3 subgoal for case 1 (out of 2)
[] Proved by normalization.
Attempting to prove level 3 subgoal for case 2 (out of 2)
Added hypothesis magicLemma3CaseHyp.1.2 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 3 subgoal for case 2 (out of 2)
LP0.1.858:
LP0.1.859: % Case 1: Trivial
LP0.1.860: % Case 2:
LP0.1.861: resume by cases qc ? p1c
Creating subgoals for proof by cases
Case hypotheses:
magicLemma3CaseHyp.2.1: qc ? p1c
magicLemma3CaseHyp.2.2: ~(qc ? p1c)
Same subgoal for all cases:
iterate(pc, f) ! (iterate(qc, gc) ! insert(p1c, Ac))
= iterate(qc & (pc \oplus gc), f \circ gc) ! Ac
Attempting to prove level 4 subgoal for case 1 (out of 2)
Added hypothesis magicLemma3CaseHyp.2.1 to the system.
Level 4 subgoal for case 1 (out of 2)
[] Proved by normalization.
Attempting to prove level 4 subgoal for case 2 (out of 2)
Added hypothesis magicLemma3CaseHyp.2.2 to the system.
Level 4 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 3 subgoal for case 2 (out of 2):
iterate(pc, f) ! (iterate(qc, gc) ! insert(p1c, Ac))
= iterate(qc & (pc \oplus gc), f \circ gc) ! insert(p1c, Ac)
[] Proved by cases qc ? p1c.
Level 2 subgoal 2 (induction step) for proof by induction on A:
iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]]
! (iterate(q, g) ! insert(p1, Ac))
= iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g)
! insert(p1, Ac)
[] Proved by cases (q & (p:pred[pair[W, pair[T1, V]]] \oplus g)) ? p1.
Conjecture magicLemma3.1:
iterate(p, f):fun[bag[pair[W, pair[T1, V]]], bag[X]]
! (iterate(q, g):fun[bag[pair[T1, V]], bag[pair[W, pair[T1, V]]]] ! A)
= iterate(q & (p:pred[pair[W, pair[T1, V]]] \oplus g), f \circ g) ! A
[] Proved by structural induction on `A:bag[pair[T1, V]]'.
The formulas cannot be ordered using the current ordering.
LP0.1.862: qed
All conjectures have been proved.
LP0.1.863: % ----------------------------------------------------------
LP0.1.864:
LP0.1.865:
LP0.1.866: % ----------------------------------------------------------
LP0.1.867: set name magicLemma4
The name-prefix is now `magicLemma4'.
LP0.1.868:
LP0.1.869: declare variables
p, q: pred [pair [W, pair [T1, V]]],
A: bag [W],
B: bag [pair [T1, V]],
f: fun [pair [W, pair [T1, V]], X],
w: W
..
LP0.1.870:
LP0.1.871: set order left-to-right
Warning: the rewriting system is known to terminate, but its termination cannot
be verified with the `left-to-right' ordering. When another rewrite rule is
added, the rewriting system will be treated as nonterminating.
The ordering-method is now `left-to-right'.
LP0.1.872: prove
(join (p & q, f) ! [A, B]):bag[X] =
iterate (q, f) ! (join (p, id) ! [A, B])
..
Attempting to prove conjecture magicLemma4.1:
join(p & q, f) ! [A, B] = iterate(q, f) ! (join(p, id) ! [A, B])
The system now contains 480 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
Suspending proof of conjecture magicLemma4.1
LP0.1.873: resume by induction on A: bag [W]
Creating subgoals for proof by structural induction on `A:bag[W]'
Basis subgoal:
Subgoal 1: join(p & q, f) ! [{}, B] = iterate(q, f) ! (join(p, id) ! [{}, B])
Induction constant: Ac
Induction hypothesis:
magicLemma4InductHyp.1:
join(p & q, f) ! [Ac, B] = iterate(q, f) ! (join(p, id) ! [Ac, B])
Induction subgoal:
Subgoal 2: join(p & q, f) ! [insert(w, Ac), B]
= iterate(q, f) ! (join(p, id) ! [insert(w, Ac), B])
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A
Level 2 subgoal 1 (basis step) for proof by induction on A
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on A
Added hypothesis magicLemma4InductHyp.1 to the system.
The system now contains 481 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
Suspending proof of level 2 subgoal 2 (induction step) for proof by induction
on A
LP0.1.874:
LP0.1.875: % Base Case: Trivial
LP0.1.876: % Inductive Case
LP0.1.877:
LP0.1.878: resume by induction on B:bag [pair [T1, V]]
Creating subgoals for proof by structural induction on `B:bag[pair[T1, V]]'
Basis subgoal:
Subgoal 1: (iterate(C(p, w) & C(q, w), C(f, w)) ! {})
\U (iterate(q, f) ! (join(p, id) ! [Ac, {}]))
= (iterate(C(p, w) & (q \oplus C(id, w)), f \circ C(id, w))
! {})
\U (iterate(q, f) ! (join(p, id) ! [Ac, {}]))
Induction constant: Bc
Induction hypothesis:
magicLemma4InductHyp.2:
(iterate(C(p, w) & C(q, w), C(f, w)) ! Bc)
\U (iterate(q, f) ! (join(p, id) ! [Ac, Bc]))
= (iterate(C(p, w) & (q \oplus C(id, w)), f \circ C(id, w)) ! Bc)
\U (iterate(q, f) ! (join(p, id) ! [Ac, Bc]))
Induction subgoal:
Subgoal 2: (iterate(C(p, w) & C(q, w), C(f, w)) ! insert(p1, Bc))
\U (iterate(q, f) ! (join(p, id) ! [Ac, insert(p1, Bc)]))
= (iterate(C(p, w) & (q \oplus C(id, w)), f \circ C(id, w))
! insert(p1, Bc))
\U (iterate(q, f) ! (join(p, id) ! [Ac, insert(p1, Bc)]))
Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on B
Level 3 subgoal 1 (basis step) for proof by induction on B
[] Proved by normalization.
Attempting to prove level 3 subgoal 2 (induction step) for proof by induction
on B
Added hypothesis magicLemma4InductHyp.2 to the system.
The system now contains 482 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
Suspending proof of level 3 subgoal 2 (induction step) for proof by induction
on B
LP0.1.879:
LP0.1.880: % Base Case: Trivial
LP0.1.881: % Inductive Case
LP0.1.882:
LP0.1.883: set order noeq-dsmpos
The ordering-method is now `noeq-dsmpos'.
LP0.1.884: resume by cases (p & q) ? [w, p1]
Creating subgoals for proof by cases
New constants: pc, qc, wc, p1c
Case hypotheses:
magicLemma4CaseHyp.1.1: (pc & qc) ? [wc, p1c]
magicLemma4CaseHyp.1.2: ~((pc & qc) ? [wc, p1c])
Same subgoal for all cases:
(iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! insert(p1c, Bc))
\U ((iterate(qc, f)
! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac))
\U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc])))
= (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc))
! insert(p1c, Bc))
\U ((iterate(qc, f)
! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac))
\U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc])))
Attempting to prove level 4 subgoal for case 1 (out of 2)
Added hypothesis magicLemma4CaseHyp.1.1 to the system.
Deduction rule lp_and_is_true has been applied to formula
magicLemma4CaseHyp.1.1 to yield the following formulas, which imply
magicLemma4CaseHyp.1.1.
magicLemma4CaseHyp.1.1.1: pc ? [wc, p1c]
magicLemma4CaseHyp.1.1.2: qc ? [wc, p1c]
The system now contains 484 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
Suspending proof of level 4 subgoal for case 1 (out of 2)
LP0.1.885:
LP0.1.886: % Case 1
LP0.1.887:
LP0.1.888: set immunity on
The immunity is now `on'.
LP0.1.889: prove C (qc, wc) = qc \oplus C (id, wc)
Attempting to prove level 5 lemma magicLemma4.2:
C(qc, wc) = qc \oplus C(id, wc)
Level 5 lemma magicLemma4.2
[] Proved by normalization.
Attempting to prove level 4 subgoal for case 1 (out of 2):
(iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! insert(p1c, Bc))
\U ((iterate(qc, f)
! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac))
\U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc])))
= (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc))
! insert(p1c, Bc))
\U ((iterate(qc, f)
! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac))
\U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc])))
Current subgoal:
insert(f ! [wc, p1c],
(iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! Bc)
\U ((iterate(qc, f)
! (iterate(C(pc\inv, p1c), C(id \circ \, p1c))
! Ac))
\U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))))
= insert(f ! [wc, p1c],
(iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc))
! Bc)
\U ((iterate(qc, f)
! (iterate(C(pc\inv, p1c),
C(id \circ \, p1c))
! Ac))
\U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc]))))
The system now contains 485 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
Suspending proof of level 4 subgoal for case 1 (out of 2)
LP0.1.890: set immunity off
The immunity is now `off'.
LP0.1.891:
LP0.1.892: set immunity on
The immunity is now `on'.
LP0.1.893: prove C (f, wc) = f \circ C (id, wc)
Attempting to prove level 5 lemma magicLemma4.3: C(f, wc) = f \circ C(id, wc)
Level 5 lemma magicLemma4.3
[] Proved by normalization.
Attempting to prove level 4 subgoal for case 1 (out of 2)
Level 4 subgoal for case 1 (out of 2)
[] Proved by normalization.
Attempting to prove level 4 subgoal for case 2 (out of 2):
(iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! insert(p1c, Bc))
\U ((iterate(qc, f)
! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac))
\U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc])))
= (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc))
! insert(p1c, Bc))
\U ((iterate(qc, f)
! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac))
\U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc])))
Added hypothesis magicLemma4CaseHyp.1.2 to the system.
The system now contains 483 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
Suspending proof of level 4 subgoal for case 2 (out of 2)
LP0.1.894: set immunity off
The immunity is now `off'.
LP0.1.895:
LP0.1.896: % Case 2
LP0.1.897:
LP0.1.898: set immunity on
The immunity is now `on'.
LP0.1.899: prove C (qc, wc) = qc \oplus C (id, wc)
Attempting to prove level 5 lemma magicLemma4.2:
C(qc, wc) = qc \oplus C(id, wc)
Level 5 lemma magicLemma4.2
[] Proved by normalization.
Attempting to prove level 4 subgoal for case 2 (out of 2)
The system now contains 484 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
Suspending proof of level 4 subgoal for case 2 (out of 2)
LP0.1.900: set immunity off
The immunity is now `off'.
LP0.1.901:
LP0.1.902: set immunity on
The immunity is now `on'.
LP0.1.903: prove C (f, wc) = f \circ C (id, wc)
Attempting to prove level 5 lemma magicLemma4.3: C(f, wc) = f \circ C(id, wc)
Level 5 lemma magicLemma4.3
[] Proved by normalization.
Attempting to prove level 4 subgoal for case 2 (out of 2):
(iterate(C(pc, wc) & C(qc, wc), C(f, wc)) ! insert(p1c, Bc))
\U ((iterate(qc, f)
! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac))
\U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc])))
= (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc))
! insert(p1c, Bc))
\U ((iterate(qc, f)
! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac))
\U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc])))
Current subgoal:
(iterate(C(pc, wc) & (qc \oplus C(id, wc)), C(f, wc)) ! Bc)
\U ((iterate(qc, f)
! (iterate(C(pc\inv, p1c), C(id \circ \, p1c)) ! Ac))
\U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc])))
= (iterate(C(pc, wc) & (qc \oplus C(id, wc)), f \circ C(id, wc)) ! Bc)
\U ((iterate(qc, f)
! (iterate(C(pc\inv, p1c), C(id \circ \, p1c))
! Ac))
\U (iterate(qc, f) ! (join(pc, id) ! [Ac, Bc])))
Level 4 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 3 subgoal 2 (induction step) for proof by induction on B:
(iterate(C(p, w) & C(q, w), C(f, w)) ! insert(p1, Bc))
\U (iterate(q, f) ! (join(p, id) ! [Ac, insert(p1, Bc)]))
= (iterate(C(p, w) & (q \oplus C(id, w)), f \circ C(id, w))
! insert(p1, Bc))
\U (iterate(q, f) ! (join(p, id) ! [Ac, insert(p1, Bc)]))
[] Proved by cases (p & q) ? [w, p1].
Level 2 subgoal 2 (induction step) for proof by induction on A:
join(p & q, f) ! [insert(w, Ac), B]
= iterate(q, f) ! (join(p, id) ! [insert(w, Ac), B])
[] Proved by structural induction on `B:bag[pair[T1, V]]'.
Conjecture magicLemma4.1:
join(p & q, f) ! [A, B] = iterate(q, f) ! (join(p, id) ! [A, B])
[] Proved by structural induction on `A:bag[W]'.
The system now contains 481 rewrite rules. The rewriting system is NOT
guaranteed to terminate.
LP0.1.904: set immunity off
The immunity is now `off'.
LP0.1.905:
LP0.1.906: qed
All conjectures have been proved.
LP0.1.907: set order noeq-dsmpos
The ordering-method is now `noeq-dsmpos'.
LP0.1.908: % ----------------------------------------------------------
LP0.1.909:
LP0.1.910: % ----------------------------------------------------------
LP0.1.911: set name magicLemma5a
The name-prefix is now `magicLemma5a'.
LP0.1.912: declare variables
p: pred [pair [W, pair [T1, V]]],
A: bag [W],
B: bag [pair [T1, V]],
f: fun [pair [W, pair [T1, V]], pair [W, pair [T1, V]]],
X, Y, Z: bag [pair [W, pair [T1, V]]]
..
LP0.1.913:
LP0.1.914: prove X \U Y = Y \U X by induction on X
Attempting to prove conjecture magicLemma5a.1: X \U Y = Y \U X
Creating subgoals for proof by structural induction on `X'
Basis subgoal:
Subgoal 1: {} \U Y = Y \U {}
Induction constant: Xc
Induction hypothesis:
magicLemma5aInductHyp.1: Xc \U Y = Y \U Xc
Induction subgoal:
Subgoal 2: insert(p1, Xc) \U Y = Y \U insert(p1, Xc)
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on X
Level 2 subgoal 1 (basis step) for proof by induction on X
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on X
Added hypothesis magicLemma5aInductHyp.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 2 subgoal 2 (induction step) for proof by induction
on X
LP0.1.915: resume by induction on Y
Creating subgoals for proof by structural induction on `Y'
Basis subgoal:
Subgoal 1: insert(p1, Xc \U {}) = insert(p1, {} \U Xc)
Induction constant: Yc
Induction hypothesis:
magicLemma5aInductHyp.2: insert(p1, Xc \U Yc) = insert(p1, Yc \U Xc)
Induction subgoal:
Subgoal 2: insert(p1, Xc \U insert(p2, Yc))
= insert(p1, insert(p2, Yc) \U Xc)
Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on Y
Level 3 subgoal 1 (basis step) for proof by induction on Y
[] Proved by normalization.
Attempting to prove level 3 subgoal 2 (induction step) for proof by induction
on Y
Added hypothesis magicLemma5aInductHyp.2 to the system.
Normalization of the term
insert(p1, Xc \U insert(p2, Yc)) = insert(p1, insert(p2, Yc) \U Xc)
has been stopped to avoid a potentially infinite rewriting loop. It has been
reduced to
insert(p1, insert(p2, Xc \U Yc)) = insert(p2, insert(p1, Yc \U Xc))
Normalization of the term
insert(p1, insert(p2, Xc \U Yc)) = insert(p2, insert(p1, Yc \U Xc))
has been stopped to avoid a potentially infinite rewriting loop. It has been
reduced to
insert(p2, insert(p1, Xc \U Yc)) = insert(p2, insert(p1, Yc \U Xc))
The formulas cannot be ordered using the current ordering.
Suspending proof of level 3 subgoal 2 (induction step) for proof by induction
on Y
LP0.1.916: resume by contradiction
Creating subgoals for proof by contradiction
New constants: p2c, p1c
Hypothesis:
magicLemma5aContraHyp.1:
~(insert(p2c, insert(p1c, Xc \U Yc)) = insert(p2c, insert(p1c, Yc \U Xc)))
Only subgoal:
false
Attempting to prove level 4 subgoal for proof by contradiction
Added hypothesis magicLemma5aContraHyp.1 to the system.
Normalization of the term
~(insert(p2c, insert(p1c, Xc \U Yc)) = insert(p2c, insert(p1c, Yc \U Xc)))
has been stopped to avoid a potentially infinite rewriting loop. It has been
reduced to
~(insert(p1c, insert(p2c, Xc \U Yc)) = insert(p2c, insert(p1c, Yc \U Xc)))
The formulas cannot be ordered using the current ordering.
Suspending proof of level 4 subgoal for proof by contradiction
LP0.1.917: crit-pairs *Contra* with *Induct*
The following equations are critical pairs between rewrite rules
magicLemma5aContraHyp.1 and magicLemma5aInductHyp.2.
magicLemma5a.2: false
The system now contains 2 formulas and 483 rewrite rules. The rewriting system
is NOT guaranteed to terminate.
Critical pair computation abandoned because a theorem has been proved.
Formula magicLemma5a.2, false, is inconsistent.
Level 4 subgoal for proof by contradiction
[] Proved by detecting an inconsistency.
Level 3 subgoal 2 (induction step) for proof by induction on Y:
insert(p1, Xc \U insert(p2, Yc)) = insert(p1, insert(p2, Yc) \U Xc)
[] Proved by contradiction.
Level 2 subgoal 2 (induction step) for proof by induction on X:
insert(p1, Xc) \U Y = Y \U insert(p1, Xc)
[] Proved by structural induction on `Y'.
Conjecture magicLemma5a.1: X \U Y = Y \U X
[] Proved by structural induction on `X'.
The formulas cannot be ordered using the current ordering.
LP0.1.918: qed
All conjectures have been proved.
LP0.1.919: % ----------------------------------------------------------
LP0.1.920:
LP0.1.921: % ----------------------------------------------------------
LP0.1.922: set name magicLemma5b
The name-prefix is now `magicLemma5b'.
LP0.1.923: prove X \U (Y \U Z) = (X \U Z) \U Y
Attempting to prove conjecture magicLemma5b.1: X \U (Y \U Z) = X \U Z \U Y
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture magicLemma5b.1
LP0.1.924: resume by induction on X
Creating subgoals for proof by structural induction on `X'
Basis subgoal:
Subgoal 1: {} \U (Y \U Z) = {} \U Z \U Y
Induction constant: Xc
Induction hypothesis:
magicLemma5bInductHyp.1: Xc \U (Y \U Z) = Xc \U Z \U Y
Induction subgoal:
Subgoal 2: insert(p1, Xc) \U (Y \U Z) = insert(p1, Xc) \U Z \U Y
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on X
The formulas cannot be ordered using the current ordering.
Suspending proof of level 2 subgoal 1 (basis step) for proof by induction on X
LP0.1.925: resume by induction on Y
Creating subgoals for proof by structural induction on `Y'
Basis subgoal:
Subgoal 1: {} \U Z = Z \U {}
Induction constant: Yc
Induction hypothesis:
magicLemma5bInductHyp.1: Yc \U Z = Z \U Yc
Induction subgoal:
Subgoal 2: insert(p1, Yc) \U Z = Z \U insert(p1, Yc)
Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on Y
Level 3 subgoal 1 (basis step) for proof by induction on Y
[] Proved by normalization.
Attempting to prove level 3 subgoal 2 (induction step) for proof by induction
on Y
Added hypothesis magicLemma5bInductHyp.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 3 subgoal 2 (induction step) for proof by induction
on Y
LP0.1.926: resume by induction on Z
Creating subgoals for proof by structural induction on `Z'
Basis subgoal:
Subgoal 1: insert(p1, Yc \U {}) = insert(p1, {} \U Yc)
Induction constant: Zc
Induction hypothesis:
magicLemma5bInductHyp.2: insert(p1, Yc \U Zc) = insert(p1, Zc \U Yc)
Induction subgoal:
Subgoal 2: insert(p1, Yc \U insert(p2, Zc))
= insert(p1, insert(p2, Zc) \U Yc)
Attempting to prove level 4 subgoal 1 (basis step) for proof by induction on Z
Level 4 subgoal 1 (basis step) for proof by induction on Z
[] Proved by normalization.
Attempting to prove level 4 subgoal 2 (induction step) for proof by induction
on Z
Added hypothesis magicLemma5bInductHyp.2 to the system.
Normalization of the term
insert(p1, Yc \U insert(p2, Zc)) = insert(p1, insert(p2, Zc) \U Yc)
has been stopped to avoid a potentially infinite rewriting loop. It has been
reduced to
insert(p1, insert(p2, Yc \U Zc)) = insert(p2, insert(p1, Zc \U Yc))
Normalization of the term
insert(p1, insert(p2, Yc \U Zc)) = insert(p2, insert(p1, Zc \U Yc))
has been stopped to avoid a potentially infinite rewriting loop. It has been
reduced to
insert(p2, insert(p1, Yc \U Zc)) = insert(p2, insert(p1, Zc \U Yc))
The formulas cannot be ordered using the current ordering.
Suspending proof of level 4 subgoal 2 (induction step) for proof by induction
on Z
LP0.1.927: resume by contradiction
Creating subgoals for proof by contradiction
New constants: p2c, p1c
Hypothesis:
magicLemma5bContraHyp.1:
~(insert(p2c, insert(p1c, Yc \U Zc)) = insert(p2c, insert(p1c, Zc \U Yc)))
Only subgoal:
false
Attempting to prove level 5 subgoal for proof by contradiction
Added hypothesis magicLemma5bContraHyp.1 to the system.
Normalization of the term
~(insert(p2c, insert(p1c, Yc \U Zc)) = insert(p2c, insert(p1c, Zc \U Yc)))
has been stopped to avoid a potentially infinite rewriting loop. It has been
reduced to
~(insert(p1c, insert(p2c, Yc \U Zc)) = insert(p2c, insert(p1c, Zc \U Yc)))
The formulas cannot be ordered using the current ordering.
Suspending proof of level 5 subgoal for proof by contradiction
LP0.1.928: crit-pairs *Contra* with *Induct*
The following equations are critical pairs between rewrite rules
magicLemma5bContraHyp.1 and magicLemma5bInductHyp.2.
magicLemma5b.2: false
The system now contains 3 formulas and 483 rewrite rules. The rewriting system
is NOT guaranteed to terminate.
Critical pair computation abandoned because a theorem has been proved.
Formula magicLemma5b.2, false, is inconsistent.
Level 5 subgoal for proof by contradiction
[] Proved by detecting an inconsistency.
Level 4 subgoal 2 (induction step) for proof by induction on Z:
insert(p1, Yc \U insert(p2, Zc)) = insert(p1, insert(p2, Zc) \U Yc)
[] Proved by contradiction.
Level 3 subgoal 2 (induction step) for proof by induction on Y:
insert(p1, Yc) \U Z = Z \U insert(p1, Yc)
[] Proved by structural induction on `Z'.
Level 2 subgoal 1 (basis step) for proof by induction on X:
{} \U (Y \U Z) = {} \U Z \U Y
[] Proved by structural induction on `Y'.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on X: insert(p1, Xc) \U (Y \U Z) = insert(p1, Xc) \U Z \U Y
Added hypothesis magicLemma5bInductHyp.1 to the system.
Level 2 subgoal 2 (induction step) for proof by induction on X
[] Proved by normalization.
Conjecture magicLemma5b.1: X \U (Y \U Z) = X \U Z \U Y
[] Proved by structural induction on `X'.
The formulas cannot be ordered using the current ordering.
LP0.1.929: qed
All conjectures have been proved.
LP0.1.930: % ----------------------------------------------------------
LP0.1.931:
LP0.1.932: % ----------------------------------------------------------
LP0.1.933: set name magicLemma5c
The name-prefix is now `magicLemma5c'.
LP0.1.934: prove
join (p, f:fun [pair [W, pair [T1, V]], pair [W, pair [T1, V]]]) ! [A, B] =
join (p, f) ! [A, iterate (ex (p\inv) \oplus \, id) ! B]
..
Attempting to prove conjecture magicLemma5c.1:
(join(p, f) ! [A, B]):bag[pair[W, pair[T1, V]]]
= join(p, f) ! [A, iterate(ex(p\inv) \oplus \, id) ! B]
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture magicLemma5c.1
LP0.1.935: resume by induction on A:bag [W]
Creating subgoals for proof by structural induction on `A:bag[W]'
Basis subgoal:
Subgoal 1: (join(p, f) ! [{}, B]):bag[pair[W, pair[T1, V]]]
= join(p, f)
! [{}, iterate(ex(p\inv) \oplus \, id) ! B]
Induction constant: Ac
Induction hypothesis:
magicLemma5cInductHyp.1:
(join(p, f) ! [Ac, B]):bag[pair[W, pair[T1, V]]]
= join(p, f) ! [Ac, iterate(ex(p\inv) \oplus \, id) ! B]
Induction subgoal:
Subgoal 2: (join(p, f) ! [insert(w, Ac), B]):bag[pair[W, pair[T1, V]]]
= join(p, f)
! [insert(w, Ac),
iterate(ex(p\inv) \oplus \, id)
! B]
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A
Level 2 subgoal 1 (basis step) for proof by induction on A
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on A
Added hypothesis magicLemma5cInductHyp.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 2 subgoal 2 (induction step) for proof by induction
on A
LP0.1.936:
LP0.1.937: % Base Case
LP0.1.938: % Inductive Case
LP0.1.939:
LP0.1.940: resume by induction on B:bag[pair [T1, V]]
Creating subgoals for proof by structural induction on `B:bag[pair[T1, V]]'
Basis subgoal:
Subgoal 1: ((iterate(C(p, w), C(f, w)) ! {}) \U (join(p, f) ! [Ac, {}])):
bag[pair[W, pair[T1, V]]]
= (iterate(C(p, w), C(f, w))
! (iterate(ex(p\inv) \oplus \, id)
! {}))
\U (join(p, f)
! [Ac,
iterate(ex(p\inv) \oplus \,
id)
! {}])
Induction constant: Bc
Induction hypothesis:
magicLemma5cInductHyp.2:
((iterate(C(p, w), C(f, w)) ! Bc) \U (join(p, f) ! [Ac, Bc])):
bag[pair[W, pair[T1, V]]]
= (iterate(C(p, w), C(f, w))
! (iterate(ex(p\inv) \oplus \, id) ! Bc))
\U (join(p, f)
! [Ac,
iterate(ex(p\inv) \oplus \, id)
! Bc])
Induction subgoal:
Subgoal 2: ((iterate(C(p, w), C(f, w)) ! insert(p1, Bc))
\U (join(p, f) ! [Ac, insert(p1, Bc)])):
bag[pair[W, pair[T1, V]]]
= (iterate(C(p, w), C(f, w))
! (iterate(ex(p\inv) \oplus \, id)
! insert(p1, Bc)))
\U (join(p, f)
! [Ac,
iterate(ex(p\inv) \oplus \,
id)
! insert(p1, Bc)])
Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on B
Level 3 subgoal 1 (basis step) for proof by induction on B
[] Proved by normalization.
Attempting to prove level 3 subgoal 2 (induction step) for proof by induction
on B
Added hypothesis magicLemma5cInductHyp.2 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 3 subgoal 2 (induction step) for proof by induction
on B
LP0.1.941:
LP0.1.942: % Base Case
LP0.1.943: % Inductive Case
LP0.1.944:
LP0.1.945: resume by cases (ex(p\inv) \oplus \) ? p1
Creating subgoals for proof by cases
New constants: pc, wc, p1c
Case hypotheses:
magicLemma5cCaseHyp.1.1: (ex(pc\inv) \oplus \) ? p1c
magicLemma5cCaseHyp.1.2:
~((ex(pc\inv) \oplus \) ? p1c)
Same subgoal for all cases:
((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc))
\U (join(pc, f) ! [Ac, Bc])
\U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)):
bag[pair[W, pair[T1, V]]]
= (iterate(C(pc, wc), C(f, wc))
! (iterate(ex(pc\inv) \oplus \, id)
! insert(p1c, Bc)))
\U (join(pc, f)
! [Ac,
iterate(ex(pc\inv) \oplus \, id)
! insert(p1c, Bc)])
Attempting to prove level 4 subgoal for case 1 (out of 2)
Added hypothesis magicLemma5cCaseHyp.1.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 4 subgoal for case 1 (out of 2)
LP0.1.946:
LP0.1.947: % Case 1
LP0.1.948:
LP0.1.949: resume by cases pc ? [wc, p1c]
Creating subgoals for proof by cases
Case hypotheses:
magicLemma5cCaseHyp.2.1: pc ? [wc, p1c]
magicLemma5cCaseHyp.2.2: ~(pc ? [wc, p1c])
Same subgoal for all cases:
((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc))
\U (join(pc, f) ! [Ac, Bc])
\U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)):
bag[pair[W, pair[T1, V]]]
= (iterate(C(pc, wc), C(f, wc))
! insert(p1c,
iterate(ex(pc\inv) \oplus \, id)
! Bc))
\U (join(pc, f)
! [Ac,
iterate(ex(pc\inv) \oplus \, id)
! Bc])
\U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)
Attempting to prove level 5 subgoal for case 1 (out of 2)
Added hypothesis magicLemma5cCaseHyp.2.1 to the system.
Level 5 subgoal for case 1 (out of 2)
[] Proved by normalization.
Attempting to prove level 5 subgoal for case 2 (out of 2)
Added hypothesis magicLemma5cCaseHyp.2.2 to the system.
Level 5 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 4 subgoal for case 1 (out of 2):
((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc))
\U (join(pc, f) ! [Ac, Bc])
\U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)):
bag[pair[W, pair[T1, V]]]
= (iterate(C(pc, wc), C(f, wc))
! (iterate(ex(pc\inv) \oplus \, id)
! insert(p1c, Bc)))
\U (join(pc, f)
! [Ac,
iterate(ex(pc\inv) \oplus \, id)
! insert(p1c, Bc)])
[] Proved by cases pc ? [wc, p1c].
Attempting to prove level 4 subgoal for case 2 (out of 2):
((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc))
\U (join(pc, f) ! [Ac, Bc])
\U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)):
bag[pair[W, pair[T1, V]]]
= (iterate(C(pc, wc), C(f, wc))
! (iterate(ex(pc\inv) \oplus \, id)
! insert(p1c, Bc)))
\U (join(pc, f)
! [Ac,
iterate(ex(pc\inv) \oplus \, id)
! insert(p1c, Bc)])
Added hypothesis magicLemma5cCaseHyp.1.2 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 4 subgoal for case 2 (out of 2)
LP0.1.950:
LP0.1.951: % Case 2
LP0.1.952:
LP0.1.953: resume by cases pc ? [wc, p1c]
Creating subgoals for proof by cases
Case hypotheses:
magicLemma5cCaseHyp.2.1: pc ? [wc, p1c]
magicLemma5cCaseHyp.2.2: ~(pc ? [wc, p1c])
Same subgoal for all cases:
((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc))
\U (join(pc, f) ! [Ac, Bc])
\U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)):
bag[pair[W, pair[T1, V]]]
= (iterate(C(pc, wc), C(f, wc)) ! Bc) \U (join(pc, f) ! [Ac, Bc])
Attempting to prove level 5 subgoal for case 1 (out of 2)
Added hypothesis magicLemma5cCaseHyp.2.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 5 subgoal for case 1 (out of 2)
LP0.1.954: % Case 1
LP0.1.955: prove
\E y:W (y:W \in insert(wc, Ac) /\ (pc\inv) ? [p1c, y])
by specializing y to wc
..
Attempting to prove level 6 lemma magicLemma5c.2:
\E y:W (y \in insert(wc, Ac) /\ (pc\inv) ? [p1c, y])
Creating subgoals for proof by specialization
Subgoal:
wc \in insert(wc, Ac) /\ (pc\inv) ? [p1c, wc]
Attempting to prove level 7 subgoal for proof by specialization
Level 7 subgoal for proof by specialization
[] Proved by normalization.
Level 6 lemma magicLemma5c.2
[] Proved by specialization.
Attempting to prove level 5 subgoal for case 1 (out of 2)
Formula magicLemma5c.2, false, is inconsistent.
Level 5 subgoal for case 1 (out of 2):
((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc))
\U (join(pc, f) ! [Ac, Bc])
\U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)):
bag[pair[W, pair[T1, V]]]
= (iterate(C(pc, wc), C(f, wc)) ! Bc) \U (join(pc, f) ! [Ac, Bc])
[] Proved by impossible case.
Attempting to prove level 5 subgoal for case 2 (out of 2):
((iterate(C(pc, wc), C(f, wc)) ! insert(p1c, Bc))
\U (join(pc, f) ! [Ac, Bc])
\U (iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac)):
bag[pair[W, pair[T1, V]]]
= (iterate(C(pc, wc), C(f, wc)) ! Bc) \U (join(pc, f) ! [Ac, Bc])
Added hypothesis magicLemma5cCaseHyp.2.2 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 5 subgoal for case 2 (out of 2)
LP0.1.956:
LP0.1.957: % Case 2
LP0.1.958:
LP0.1.959: prove
(iterate(C(pc\inv, p1c),
C(f:fun [pair [W, pair [T1, V]], pair [W, pair [T1, V]]]
\circ \, p1c)) ! Ac) =
{} by contradiction
..
Attempting to prove level 6 lemma magicLemma5c.2:
(iterate(C(pc\inv, p1c), C(f \circ \, p1c)) ! Ac):
bag[pair[W, pair[T1, V]]]
= {}
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.960:
LP0.1.961: 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.962: declare operator xc: -> pair [W, pair [T1, V]]
LP0.1.963: declare operator Bc: -> bag [pair [W, pair [T1, V]]]
LP0.1.964: 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.965: 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.966: set order left
The ordering-method is now `left-to-right'.
LP0.1.967: 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.968: 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.969: declare operator zc: -> W
LP0.1.970: 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.971: 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.972:
LP0.1.973: set order noeq
The ordering-method is now `noeq-dsmpos'.
LP0.1.974: qed
All conjectures have been proved.
LP0.1.975: % ----------------------------------------------------------
LP0.1.976:
LP0.1.977: % ----------------------------------------------------------
LP0.1.978: set name magicLemma6
The name-prefix is now `magicLemma6'.
LP0.1.979: declare variables
p: pred [pair [W, T1]],
f: fun [W, W],
g: fun [pair [T1, V], T1]
..
LP0.1.980: 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.981:
LP0.1.982: declare operator uc :-> pair [T1, V]
LP0.1.983: declare operator vc :-> W
LP0.1.984: 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.985:
LP0.1.986: % =>
LP0.1.987:
LP0.1.988: set immunity on
The immunity is now `on'.
LP0.1.989: 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.990: set immunity off
The immunity is now `off'.
LP0.1.991: 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.992: 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.993:
LP0.1.994: % <=
LP0.1.995:
LP0.1.996: set immunity on
The immunity is now `on'.
LP0.1.997: 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.998: set immunity off
The immunity is now `off'.
LP0.1.999: 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.1000: 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.1001:
LP0.1.1002: qed
All conjectures have been proved.
LP0.1.1003: % ----------------------------------------------------------
LP0.1.1004:
LP0.1.1005: % ----------------------------------------------------------
LP0.1.1006: set name magicLemma7
The name-prefix is now `magicLemma7'.
LP0.1.1007: declare variables
p: pred [pair [T1, W]],
g: fun [W, W],
f: fun [pair [T1, V], T1]
..
LP0.1.1008: set order left
The ordering-method is now `left-to-right'.
LP0.1.1009: 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.1010:
LP0.1.1011: set order noeq
The ordering-method is now `noeq-dsmpos'.
LP0.1.1012: declare operator uc :-> pair [T1, V]
LP0.1.1013: declare operator vc :-> bag [W]
LP0.1.1014: 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.1015:
LP0.1.1016: % =>
LP0.1.1017:
LP0.1.1018: set immunity on
The immunity is now `on'.
LP0.1.1019: 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.1020: set immunity off
The immunity is now `off'.
LP0.1.1021: 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.1022: 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.1023:
LP0.1.1024: % <=
LP0.1.1025:
LP0.1.1026: set immunity on
The immunity is now `on'.
LP0.1.1027: 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.1028: set immunity off
The immunity is now `off'.
LP0.1.1029: 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.1030: 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.1031:
LP0.1.1032: qed
All conjectures have been proved.
LP0.1.1033: set order noeq
The ordering-method is now `noeq-dsmpos'.
LP0.1.1034: % ----------------------------------------------------------
LP0.1.1035:
LP0.1.1036: % ----------------------------------------------------------
LP0.1.1037: set name magicLemma8
The name-prefix is now `magicLemma8'.
LP0.1.1038: set order manual
The ordering-method is now `manual'.
LP0.1.1039: 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.1040: 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.1041:
LP0.1.1042: set order left-to-right
The ordering-method is now `left-to-right'.
LP0.1.1043: 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.1044:
LP0.1.1045: % Base Case: Trivial
LP0.1.1046: % Inductive Case
LP0.1.1047:
LP0.1.1048: 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.1049:
LP0.1.1050: % Case 1
LP0.1.1051: 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.1052:
LP0.1.1053: % Case 2
LP0.1.1054: 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.1055:
LP0.1.1056: qed
All conjectures have been proved.
LP0.1.1057: set order noeq
The ordering-method is now `noeq-dsmpos'.
LP0.1.1058: make passive magicLemma8
LP0.1.1059: % ----------------------------------------------------------
LP0.1.1060:
LP0.1.1061: % ----------------------------------------------------------
LP0.1.1062: set name magicLemma9
The name-prefix is now `magicLemma9'.
LP0.1.1063: set order left-to-right
The ordering-method is now `left-to-right'.
LP0.1.1064: 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.1065:
LP0.1.1066: 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.1067: set order noeq
The ordering-method is now `noeq-dsmpos'.
LP0.1.1068: declare operators uc: -> T1
LP0.1.1069: declare operators vc: -> W
LP0.1.1070:
LP0.1.1071: set immunity on
The immunity is now `on'.
LP0.1.1072: 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.1073: set immunity off
The immunity is now `off'.
LP0.1.1074: 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.1075: 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.1076:
LP0.1.1077: qed
All conjectures have been proved.
LP0.1.1078: set order noeq
The ordering-method is now `noeq-dsmpos'.
LP0.1.1079: % ----------------------------------------------------------
LP0.1.1080:
LP0.1.1081: % ----------------------------------------------------------
LP0.1.1082: set name magicLemma10
The name-prefix is now `magicLemma10'.
LP0.1.1083: declare variables
p: pred [pair [T1, W]]
..
LP0.1.1084: 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.1085: qed
All conjectures have been proved.
LP0.1.1086: % ----------------------------------------------------------
LP0.1.1087:
LP0.1.1088: % ----------------------------------------------------------
LP0.1.1089: set name magicLemma11
The name-prefix is now `magicLemma11'.
LP0.1.1090: 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.1091: 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.1092: qed
All conjectures have been proved.
LP0.1.1093: % ----------------------------------------------------------
LP0.1.1094:
LP0.1.1095: % ----------------------------------------------------------
LP0.1.1096: set name magicLemma12
The name-prefix is now `magicLemma12'.
LP0.1.1097: 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.1098: 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.1099: qed
All conjectures have been proved.
LP0.1.1100: % ----------------------------------------------------------
LP0.1.1101:
LP0.1.1102: % ----------------------------------------------------------
LP0.1.1103: set name magicLemma13
The name-prefix is now `magicLemma13'.
LP0.1.1104: declare variables
f: fun [pair [T1, V], T1]
..
LP0.1.1105: 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.1106: qed
All conjectures have been proved.
LP0.1.1107: % ----------------------------------------------------------
LP0.1.1108:
LP0.1.1109: % ----------------------------------------------------------
LP0.1.1110: set name magicLemma14
The name-prefix is now `magicLemma14'.
LP0.1.1111: declare variables
f: fun [pair [T1, V], bag [W]]
..
LP0.1.1112: 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.1113: qed
All conjectures have been proved.
LP0.1.1114: % ----------------------------------------------------------
LP0.1.1115:
LP0.1.1116: % ----------------------------------------------------------
LP0.1.1117: set name magicLemma15
The name-prefix is now `magicLemma15'.
LP0.1.1118: declare variables
A: bag [W],
f: fun [pair [T1, V], T1]
..
LP0.1.1119: 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.1120: qed
All conjectures have been proved.
LP0.1.1121: % ----------------------------------------------------------
LP0.1.1122:
LP0.1.1123: % ----------------------------------------------------------
LP0.1.1124: set name magicLemma16
The name-prefix is now `magicLemma16'.
LP0.1.1125: declare variables
A: bag [W],
B: bag [T1],
q: pred [pair [W, T1]]
..
LP0.1.1126:
LP0.1.1127: 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.1128:
LP0.1.1129: declare operator wc: -> W
LP0.1.1130: 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.1131:
LP0.1.1132: % => Trivial
LP0.1.1133: % <=
LP0.1.1134:
LP0.1.1135: 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.1136:
LP0.1.1137: qed
All conjectures have been proved.
LP0.1.1138:
LP0.1.1139: % L1: Rules Used in Transformation, Magic
LP0.1.1140: % ---------------------------------------
LP0.1.1141:
LP0.1.1142: set name shift
The name-prefix is now `shift'.
LP0.1.1143: declare variables
p,q,r: pred [T]
..
LP0.1.1144: 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.1145: qed
All conjectures have been proved.
LP0.1.1146:
LP0.1.1147: set name nod
The name-prefix is now `nod'.
LP0.1.1148: declare variables
p: pred [pair [T1, T2]],
f: fun [T2, U],
g: fun [bag [U], V],
A: bag [T1],
B: bag [T2]
..
LP0.1.1149: 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.1150:
LP0.1.1151: 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.1152:
LP0.1.1153: % Base Case: Trivial
LP0.1.1154:
LP0.1.1155: % Inductive Case
LP0.1.1156:
LP0.1.1157: 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.1158:
LP0.1.1159: qed
All conjectures have been proved.
LP0.1.1160:
LP0.1.1161: set name magic
The name-prefix is now `magic'.
LP0.1.1162:
LP0.1.1163: 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.1164:
LP0.1.1165: 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.1166:
LP0.1.1167: set immunity on
The immunity is now `on'.
LP0.1.1168: 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.1169:
LP0.1.1170: 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.1171:
LP0.1.1172: set order left
The ordering-method is now `left-to-right'.
LP0.1.1173: 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.1174: set immunity off
The immunity is now `off'.
LP0.1.1175: set order noeq
The ordering-method is now `noeq-dsmpos'.
LP0.1.1176:
LP0.1.1177: 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.1178:
LP0.1.1179: 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.1180:
LP0.1.1181: set immunity on
The immunity is now `on'.
LP0.1.1182: 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.1183: set immunity off
The immunity is now `off'.
LP0.1.1184:
LP0.1.1185:
LP0.1.1186: 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.1187:
LP0.1.1188: qed
All conjectures have been proved.
LP0.1.1189:
LP0.1.1190:
LP0.1.1191: % Section 6: SimplifyJoin
LP0.1.1192: %
LP0.1.1193: % Proof Scripts for COKO Transformation,
LP0.1.1194: %
LP0.1.1195: % TRANSFORMATION SimplifyJoin
LP0.1.1196: % USES
LP0.1.1197: % SJ1: join (p OPLUS (f X g), #2) ! [A, B] -->
LP0.1.1198: % join (p OPLUS (id X g), #2) ! [iterate (K (true), f) ! A, B],
LP0.1.1199: % SJ2: iterate (p, f) ! (iterate (q, id) ! A) --> iterate (p & q, f) ! A,
LP0.1.1200: % SJ3: set ! (join (=, #2) ! [A, B]) --> set ! (int (=) ! [A, B]),
LP0.1.1201: % SJ4: int (=) ! [iterate (p, f) ! A, iterate (K (true), f) ! A] -->
LP0.1.1202: % iterate (p, f) ! A,
LP0.1.1203: % SJ5a: f o ID --> f,
LP0.1.1204: % SJ5b: ID o f --> f,
LP0.1.1205: % SJ6a: K (true) & p --> p,
LP0.1.1206: % SJ6b: p & K (true) --> p,
LP0.1.1207: % SJ7: K (true) OPLUS f --> K (true),
LP0.1.1208: % SJ8: p OPLUS ID --> p,
LP0.1.1209: % SJ9: ID X ID --> ID,
LP0.1.1210: % SJ10: iterate (p, f) ! (join (q, g) ! [A, B]) -->
LP0.1.1211: % join (q & (p OPLUS g), f o g) ! [A, B],
LP0.1.1212: % Pushdown
LP0.1.1213: % BEGIN
LP0.1.1214: % GIVEN _F ! A DO SJ1 (A);
LP0.1.1215: % GIVEN _F ! (_F ! [A, _O]) DO SJ2 (A);
LP0.1.1216: % BU {SJ5a || SJ5b || SJ6a || SJ6b || SJ7 || SJ8 || SJ9};
LP0.1.1217: % SJ3;
LP0.1.1218: % GIVEN _F ! A DO SJ4 (A);
LP0.1.1219: % BU {SJ5a || SJ5b || SJ6a || SJ6b || SJ7 || SJ8 || SJ9};
LP0.1.1220: % TD {SJ10 -> Pushdown}
LP0.1.1221: % END
LP0.1.1222: %
LP0.1.1223: % See Section 5 for proofs of rewrite rules:
LP0.1.1224: % SJ5a (magicLemma13), SJ5b (magicLemma14), SJ8 (magicLemma10),
LP0.1.1225: % SJ9 (magicLemma9)
LP0.1.1226: %
LP0.1.1227: % See Section 2 for proofs of rewrite rules:
LP0.1.1228: % SJ6a (simplify)
LP0.1.1229: %
LP0.1.1230: % Theorem proving revealed that [CZ98a] has an *incorrect* version of SJ4.
LP0.1.1231: % The corrected version is shown above and also be found in the updated
LP0.1.1232: % version of this paper retrievable from:
LP0.1.1233: %
LP0.1.1234: % ftp://wilma.cs.brown.edu/u/mfc/sigmod98.ps.Z
LP0.1.1235: %
LP0.1.1236:
LP0.1.1237: clear
LP0.1.1238: forget
Critical pair list cleared.
LP0.1.1239: unregister registry
LP0.1.1240: set order manual
The ordering-method is now `manual'.
LP0.1.1241: exec-silently SimpJoin_Aux_Axioms
End of input from file `/pro/oodb/specs/KOLA98/SimpJoin_Aux_Axioms.lp'.
LP0.1.1242: 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.1243: 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.1244: 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.1245: 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)
..
Registry extended.
LP0.1.1246: register height
!: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
..
Registry extended.
LP0.1.1247:
LP0.1.1248: register height
!:fun[pair[T1, T2], U],pair[T1, T2]->U =
!:fun[pair[T2, T1], U],pair[T2, T1]->U
..
Registry extended.
LP0.1.1249:
LP0.1.1250: register height
!:fun[pair[T1, T2], U],pair[T1, T2]->U >=
(!: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)
..
Registry extended.
LP0.1.1251: register stat L
=>, !:fun[pair[T1, T2], T2],pair[T1, T2]->T2,
!:fun[pair[T2, T1], T2],pair[T2, T1]->T2,
!:fun[pair[T2, T1], pair[T1, T2]],pair[T2, T1]->pair[T1, T2],
!:fun[pair[U, T2], T2],pair[U, T2]->T2,
!:fun[pair[T2, U], T2],pair[T2, U]->T2,
!:fun[pair[T2, U], pair[U, T2]],pair[T2, U]->pair[U, T2],
!:fun[pair[T, T], T],pair[T, T]->T,
!:fun[pair[T, T], pair[T, T]],pair[T, T]->pair[T, T],
!:fun[pair[T1, T2], U],pair[T1, T2]->U, !:fun[U, V],U->V,
!:fun[pair[T2, T1], U],pair[T2, T1]->U,
!:fun[pair[T1, T2], V],pair[T1, T2]->V,
!:fun[pair[T2, T1], V],pair[T2, T1]->V
..
LP0.1.1252: register stat multiset /\, \/, <=>
LP0.1.1253: set order noeq-dsmpos
The ordering-method is now `noeq-dsmpos'.
LP0.1.1254: order *
The formulas cannot be ordered using the current ordering.
LP0.1.1255: make immune formulas
LP0.1.1256:
LP0.1.1257: % L1: Lemmas for Transformation, SimplifyJoin
LP0.1.1258: % -------------------------------------------
LP0.1.1259:
LP0.1.1260: set name SJLemma
The name-prefix is now `SJLemma'.
LP0.1.1261:
LP0.1.1262: set immunity on
The immunity is now `on'.
LP0.1.1263: % set order left
LP0.1.1264: prove C (snd, x:T1) = id:fun[T2,T2]
Attempting to prove conjecture SJLemma.1:
C(snd:fun[pair[T1, T2], T2], x):fun[T2, T2] = id
Conjecture SJLemma.1
[] Proved by normalization.
The formulas cannot be ordered using the current ordering.
LP0.1.1265: qed
All conjectures have been proved.
LP0.1.1266: % ----------------------------------------------------------
LP0.1.1267:
LP0.1.1268: % ----------------------------------------------------------
LP0.1.1269: prove C (snd, x:U) = id:fun[T2,T2]
Attempting to prove conjecture SJLemma.2:
C(snd:fun[pair[U, T2], T2], x):fun[T2, T2] = id
Conjecture SJLemma.2
[] Proved by normalization.
The formulas cannot be ordered using the current ordering.
LP0.1.1270: qed
All conjectures have been proved.
LP0.1.1271: % ----------------------------------------------------------
LP0.1.1272:
LP0.1.1273: % ----------------------------------------------------------
LP0.1.1274: prove
C (p:pred[pair [U,V]] \oplus (f:fun [T1, U] \times g:fun [T2, V]), x) =
C (p \oplus (id \times g), f:fun [T1, U] ! x)
..
Attempting to prove conjecture SJLemma.3:
C((p \oplus (f \times g)):pred[pair[T1, T2]], x)
= C(p \oplus (id \times g), f:fun[T1, U] ! x)
Conjecture SJLemma.3
[] Proved by normalization.
The formulas cannot be ordered using the current ordering.
LP0.1.1275: qed
All conjectures have been proved.
LP0.1.1276: set immunity off
The immunity is now `off'.
LP0.1.1277: % ----------------------------------------------------------
LP0.1.1278:
LP0.1.1279: % ----------------------------------------------------------
LP0.1.1280: declare variables
A: bag [T1],
B: bag [T2],
q: pred [pair [T1, T2]],
g: fun [pair [T1, T2], U]
p: pred [U],
q: pred [T2],
f: fun [U, V],
g: fun [T2,U]
..
LP0.1.1281:
LP0.1.1282: prove
iterate (p, f:fun [U, V]) ! (A:bag[U] \U B) =
(iterate (p, f:fun [U, V]) ! A) \U (iterate (p, f:fun [U, V]) ! B)
..
Attempting to prove conjecture SJLemma.4:
(iterate(p, f):fun[bag[U], bag[V]] ! (A \U B)):bag[V]
= (iterate(p, f):fun[bag[U], bag[V]] ! A)
\U (iterate(p, f):fun[bag[U], bag[V]] ! B)
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture SJLemma.4
LP0.1.1283:
LP0.1.1284: resume by induction on A:bag[U]
Creating subgoals for proof by structural induction on `A:bag[U]'
Basis subgoal:
Subgoal 1: (iterate(p, f):fun[bag[U], bag[V]] ! ({} \U B)):bag[V]
= (iterate(p, f):fun[bag[U], bag[V]] ! {})
\U (iterate(p, f):fun[bag[U], bag[V]] ! B)
Induction constant: Ac
Induction hypothesis:
SJLemmaInductHyp.1:
(iterate(p, f) ! (Ac \U B)):bag[V]
= (iterate(p, f) ! Ac) \U (iterate(p, f):fun[bag[U], bag[V]] ! B)
Induction subgoal:
Subgoal 2: (iterate(p, f) ! (insert(u, Ac) \U B)):bag[V]
= (iterate(p, f) ! insert(u, Ac))
\U (iterate(p, f):fun[bag[U], bag[V]] ! 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 SJLemmaInductHyp.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.1285:
LP0.1.1286: % Base Case: Trivial
LP0.1.1287: % Trivial Case
LP0.1.1288:
LP0.1.1289: resume by induction on B:bag[U]
Creating subgoals for proof by structural induction on `B:bag[U]'
Basis subgoal:
Subgoal 1: (iterate(p, f) ! insert(u, Ac \U {})):bag[V]
= (iterate(p, f) ! insert(u, Ac))
\U (iterate(p, f):fun[bag[U], bag[V]] ! {})
Induction constant: Bc
Induction hypothesis:
SJLemmaInductHyp.2:
(iterate(p, f) ! insert(u, Ac \U Bc)):bag[V]
= (iterate(p, f) ! insert(u, Ac)) \U (iterate(p, f) ! Bc)
Induction subgoal:
Subgoal 2: (iterate(p, f) ! insert(u, Ac \U insert(u1, Bc))):bag[V]
= (iterate(p, f) ! insert(u, Ac))
\U (iterate(p, f) ! insert(u1, 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 SJLemmaInductHyp.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.1290:
LP0.1.1291: % Base Case: Trivial
LP0.1.1292: % Trivial Case
LP0.1.1293:
LP0.1.1294: resume by cases p ? u1
Creating subgoals for proof by cases
New constants: pc, u1c
Case hypotheses:
SJLemmaCaseHyp.1.1: pc ? u1c
SJLemmaCaseHyp.1.2: ~(pc ? u1c)
Same subgoal for all cases:
(iterate(pc, f) ! insert(u, insert(u1c, Ac \U Bc))):bag[V]
= (iterate(pc, f) ! insert(u, Ac)) \U (iterate(pc, f) ! insert(u1c, Bc))
Attempting to prove level 4 subgoal for case 1 (out of 2)
Added hypothesis SJLemmaCaseHyp.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.1295:
LP0.1.1296: % Case 1
LP0.1.1297: resume by cases pc ? u
Creating subgoals for proof by cases
New constant: uc
Case hypotheses:
SJLemmaCaseHyp.2.1: pc ? uc
SJLemmaCaseHyp.2.2: ~(pc ? uc)
Same subgoal for all cases:
(iterate(pc, f) ! insert(uc, insert(u1c, Ac \U Bc))):bag[V]
= insert(f ! u1c,
(iterate(pc, f) ! insert(uc, Ac)) \U (iterate(pc, f) ! Bc))
Attempting to prove level 5 subgoal for case 1 (out of 2)
Added hypothesis SJLemmaCaseHyp.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.1298: normalize conjecture
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 SJLemmaCaseHyp.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(pc, f) ! insert(u, insert(u1c, Ac \U Bc))):bag[V]
= (iterate(pc, f) ! insert(u, Ac)) \U (iterate(pc, f) ! insert(u1c, Bc))
[] Proved by cases pc ? u.
Attempting to prove level 4 subgoal for case 2 (out of 2):
(iterate(pc, f) ! insert(u, insert(u1c, Ac \U Bc))):bag[V]
= (iterate(pc, f) ! insert(u, Ac)) \U (iterate(pc, f) ! insert(u1c, Bc))
Added hypothesis SJLemmaCaseHyp.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)
The formulas cannot be ordered using the current ordering.
LP0.1.1299:
LP0.1.1300: % Case 2
LP0.1.1301: resume by cases pc ? u
Creating subgoals for proof by cases
New constant: uc
Case hypotheses:
SJLemmaCaseHyp.2.1: pc ? uc
SJLemmaCaseHyp.2.2: ~(pc ? uc)
Same subgoal for all cases:
(iterate(pc, f) ! insert(uc, insert(u1c, Ac \U Bc))):bag[V]
= (iterate(pc, f) ! insert(uc, Ac)) \U (iterate(pc, f) ! Bc)
Attempting to prove level 5 subgoal for case 1 (out of 2)
Added hypothesis SJLemmaCaseHyp.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 SJLemmaCaseHyp.2.2 to the system.
Level 5 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 4 subgoal for case 2 (out of 2)
[] Proved by cases pc ? u.
Level 3 subgoal 2 (induction step) for proof by induction on B:
(iterate(p, f) ! insert(u, Ac \U insert(u1, Bc))):bag[V]
= (iterate(p, f) ! insert(u, Ac)) \U (iterate(p, f) ! insert(u1, Bc))
[] Proved by cases p ? u1.
Level 2 subgoal 2 (induction step) for proof by induction on A:
(iterate(p, f) ! (insert(u, Ac) \U B)):bag[V]
= (iterate(p, f) ! insert(u, Ac))
\U (iterate(p, f):fun[bag[U], bag[V]] ! B)
[] Proved by structural induction on `B:bag[U]'.
Conjecture SJLemma.4:
(iterate(p, f):fun[bag[U], bag[V]] ! (A \U B)):bag[V]
= (iterate(p, f):fun[bag[U], bag[V]] ! A)
\U (iterate(p, f):fun[bag[U], bag[V]] ! B)
[] Proved by structural induction on `A:bag[U]'.
The formulas cannot be ordered using the current ordering.
LP0.1.1302:
LP0.1.1303: qed
All conjectures have been proved.
LP0.1.1304: % ----------------------------------------------------------
LP0.1.1305:
LP0.1.1306:
LP0.1.1307: % ----------------------------------------------------------
LP0.1.1308: prove
iterate (p, f:fun [U, V]) ! (iterate (q, g:fun[T2,U]) ! B) =
iterate (q:pred [T2] & (p \oplus g:fun[T2,U]),
f:fun [U, V] \circ g:fun[T2,U]) ! B
..
Attempting to prove conjecture SJLemma.5:
iterate(p, f):fun[bag[U], bag[V]] ! (iterate(q, g):fun[bag[T2], bag[U]] ! B)
= iterate(q & (p \oplus g), f \circ g) ! B
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture SJLemma.5
LP0.1.1309:
LP0.1.1310: resume by induction on B:bag[T2]
Creating subgoals for proof by structural induction on `B:bag[T2]'
Basis subgoal:
Subgoal 1: iterate(p, f):fun[bag[U], bag[V]]
! (iterate(q, g):fun[bag[T2], bag[U]] ! {})
= iterate(q & (p \oplus g), f \circ g) ! {}
Induction constant: Bc
Induction hypothesis:
SJLemmaInductHyp.1:
iterate(p, f):fun[bag[U], bag[V]] ! (iterate(q, g) ! Bc)
= iterate(q & (p \oplus g), f \circ g) ! Bc
Induction subgoal:
Subgoal 2: iterate(p, f):fun[bag[U], bag[V]]
! (iterate(q, g) ! insert(t, Bc))
= iterate(q & (p \oplus g), f \circ g) ! insert(t, Bc)
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on B
Level 2 subgoal 1 (basis step) for proof by induction on B
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on B
Added hypothesis SJLemmaInductHyp.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 2 subgoal 2 (induction step) for proof by induction
on B
LP0.1.1311:
LP0.1.1312: % Base Case: Trivial
LP0.1.1313: % Inductive Case
LP0.1.1314:
LP0.1.1315: resume by cases q ? t
Creating subgoals for proof by cases
New constants: qc, tc
Case hypotheses:
SJLemmaCaseHyp.1.1: qc ? tc
SJLemmaCaseHyp.1.2: ~(qc ? tc)
Same subgoal for all cases:
iterate(p, f):fun[bag[U], bag[V]] ! (iterate(qc, g) ! insert(tc, Bc))
= iterate(qc & (p \oplus g), f \circ g) ! insert(tc, Bc)
Attempting to prove level 3 subgoal for case 1 (out of 2)
Added hypothesis SJLemmaCaseHyp.1.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 3 subgoal for case 1 (out of 2)
LP0.1.1316:
LP0.1.1317: % Case 1
LP0.1.1318: resume by cases p:pred [U] ? (g ! tc)
Creating subgoals for proof by cases
New constants: pc, gc
Case hypotheses:
SJLemmaCaseHyp.2.1: pc ? (gc ! tc)
SJLemmaCaseHyp.2.2: ~(pc ? (gc ! tc))
Same subgoal for all cases:
iterate(pc, f) ! insert(gc ! tc, iterate(qc, gc) ! Bc)
= iterate(qc & (pc \oplus gc), f \circ gc) ! insert(tc, Bc)
Attempting to prove level 4 subgoal for case 1 (out of 2)
Added hypothesis SJLemmaCaseHyp.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 SJLemmaCaseHyp.2.2 to the system.
Level 4 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 3 subgoal for case 1 (out of 2)
[] Proved by cases p:pred[U] ? (g ! tc).
Attempting to prove level 3 subgoal for case 2 (out of 2):
iterate(p, f):fun[bag[U], bag[V]] ! (iterate(qc, g) ! insert(tc, Bc))
= iterate(qc & (p \oplus g), f \circ g) ! insert(tc, Bc)
Added hypothesis SJLemmaCaseHyp.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 B:
iterate(p, f):fun[bag[U], bag[V]] ! (iterate(q, g) ! insert(t, Bc))
= iterate(q & (p \oplus g), f \circ g) ! insert(t, Bc)
[] Proved by cases q ? t.
Conjecture SJLemma.5:
iterate(p, f):fun[bag[U], bag[V]] ! (iterate(q, g):fun[bag[T2], bag[U]] ! B)
= iterate(q & (p \oplus g), f \circ g) ! B
[] Proved by structural induction on `B:bag[T2]'.
The formulas cannot be ordered using the current ordering.
LP0.1.1319:
LP0.1.1320: % Case 2
LP0.1.1321:
LP0.1.1322: qed
All conjectures have been proved.
LP0.1.1323: % ----------------------------------------------------------
LP0.1.1324:
LP0.1.1325:
LP0.1.1326: % ----------------------------------------------------------
LP0.1.1327: set immunity on
The immunity is now `on'.
LP0.1.1328: prove
C (p:pred[pair [T1,T2]] & q, x:T1) =
C (p:pred[pair [T1,T2]], x) & C (q:pred[pair [T1,T2]], x)
..
Attempting to prove conjecture SJLemma.6:
C(p & q, x) = C(p:pred[pair[T1, T2]], x) & C(q:pred[pair[T1, T2]], x)
Conjecture SJLemma.6
[] Proved by normalization.
The formulas cannot be ordered using the current ordering.
LP0.1.1329: qed
All conjectures have been proved.
LP0.1.1330: set immunity off
The immunity is now `off'.
LP0.1.1331: % ----------------------------------------------------------
LP0.1.1332:
LP0.1.1333: % ----------------------------------------------------------
LP0.1.1334: set immunity on
The immunity is now `on'.
LP0.1.1335: prove C (f:fun [U, V] \circ g:fun [pair [T1, T2],U], x) = f \circ C (g, x)
Attempting to prove conjecture SJLemma.7: C(f \circ g, x) = f \circ C(g, x)
Conjecture SJLemma.7
[] Proved by normalization.
The formulas cannot be ordered using the current ordering.
LP0.1.1336: qed
All conjectures have been proved.
LP0.1.1337: set immunity off
The immunity is now `off'.
LP0.1.1338: % ----------------------------------------------------------
LP0.1.1339:
LP0.1.1340: % ----------------------------------------------------------
LP0.1.1341: set immunity on
The immunity is now `on'.
LP0.1.1342: prove C (p:pred [U] \oplus g:fun [pair [T1, T2],U], x) = p \oplus C (g, x)
Attempting to prove conjecture SJLemma.8:
C((p:pred[U] \oplus g):pred[pair[T1, T2]], x) = p \oplus C(g, x)
Conjecture SJLemma.8
[] Proved by normalization.
The formulas cannot be ordered using the current ordering.
LP0.1.1343: qed
All conjectures have been proved.
LP0.1.1344: set immunity off
The immunity is now `off'.
LP0.1.1345: % ----------------------------------------------------------
LP0.1.1346:
LP0.1.1347: % ----------------------------------------------------------
LP0.1.1348: declare variables
A: bag [T],
A,B: bag [U],
x: U,
p, q: pred [T],
f: fun [T, U]
..
LP0.1.1349:
LP0.1.1350: prove A:bag[U] \I insert (x:U, A) = A
Attempting to prove conjecture SJLemma.9: (A \I insert(x, A)):bag[U] = A
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture SJLemma.9
LP0.1.1351: resume by induction on A:bag[U]
Creating subgoals for proof by structural induction on `A:bag[U]'
Basis subgoal:
Subgoal 1: ({} \I insert(x, {})):bag[U] = {}
Induction constant: Ac
Induction hypothesis:
SJLemmaInductHyp.1: Ac \I insert(x, Ac) = Ac
Induction subgoal:
Subgoal 2: insert(u, Ac) \I insert(x, insert(u, Ac)) = insert(u, Ac)
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A
Level 2 subgoal 1 (basis step) for proof by induction on A
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on A
Added hypothesis SJLemmaInductHyp.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.1352:
LP0.1.1353: % Base Case: Trivial
LP0.1.1354: % Inductive Case
LP0.1.1355:
LP0.1.1356: normalize conjecture
Level 2 subgoal 2 (induction step) for proof by induction on A
[] Proved by normalization.
Conjecture SJLemma.9: (A \I insert(x, A)):bag[U] = A
[] Proved by structural induction on `A:bag[U]'.
The formulas cannot be ordered using the current ordering.
The formulas cannot be ordered using the current ordering.
LP0.1.1357: qed
All conjectures have been proved.
LP0.1.1358: % ----------------------------------------------------------
LP0.1.1359:
LP0.1.1360: % ----------------------------------------------------------
LP0.1.1361: set activity off
Activity is now `off'.
LP0.1.1362: prove A:bag[U] \I B = B \I A
Attempting to prove conjecture SJLemma.10: (A \I B):bag[U] = B \I A
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture SJLemma.10
LP0.1.1363: resume by induction on A:bag[U]
Creating subgoals for proof by structural induction on `A:bag[U]'
Basis subgoal:
Subgoal 1: ({} \I B):bag[U] = B \I {}
Induction constant: Ac
Induction hypothesis:
SJLemmaInductHyp.1: Ac \I B = B \I Ac
Induction subgoal:
Subgoal 2: insert(u, Ac) \I B = B \I insert(u, Ac)
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A
Level 2 subgoal 1 (basis step) for proof by induction on A
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on A
Added hypothesis SJLemmaInductHyp.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.1364:
LP0.1.1365: % Base Case
LP0.1.1366: % Inductive Case
LP0.1.1367:
LP0.1.1368: resume by cases u \in B
Creating subgoals for proof by cases
New constants: uc, Bc
Case hypotheses:
SJLemmaCaseHyp.1.1: uc \in Bc
SJLemmaCaseHyp.1.2: ~(uc \in Bc)
Same subgoal for all cases:
insert(uc, Ac) \I Bc = Bc \I insert(uc, Ac)
Attempting to prove level 3 subgoal for case 1 (out of 2)
Added hypothesis SJLemmaCaseHyp.1.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 3 subgoal for case 1 (out of 2)
LP0.1.1369:
LP0.1.1370: % Case 1
LP0.1.1371: normalize conjecture
Level 3 subgoal for case 1 (out of 2)
[] Proved by normalization.
Attempting to prove level 3 subgoal for case 2 (out of 2)
Added hypothesis SJLemmaCaseHyp.1.2 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 3 subgoal for case 2 (out of 2)
The formulas cannot be ordered using the current ordering.
LP0.1.1372:
LP0.1.1373: % Case 2
LP0.1.1374: normalize conjecture
Level 3 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 2 subgoal 2 (induction step) for proof by induction on A:
insert(u, Ac) \I B = B \I insert(u, Ac)
[] Proved by cases u \in B.
Conjecture SJLemma.10: (A \I B):bag[U] = B \I A
[] Proved by structural induction on `A:bag[U]'.
The formulas cannot be ordered using the current ordering.
The formulas cannot be ordered using the current ordering.
LP0.1.1375:
LP0.1.1376: qed
All conjectures have been proved.
LP0.1.1377: set activity on
Activity is now `on'.
LP0.1.1378: % ----------------------------------------------------------
LP0.1.1379:
LP0.1.1380: % ----------------------------------------------------------
LP0.1.1381: prove x:U \in A => insert (x:U, A - x:U) = A:bag[U]
Attempting to prove conjecture SJLemma.11:
x:U \in A => insert(x, A - x:U):bag[U] = A
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture SJLemma.11
LP0.1.1382: resume by induction on A:bag[U]
Creating subgoals for proof by structural induction on `A:bag[U]'
Basis subgoal:
Subgoal 1: x:U \in {} => insert(x, {} - x:U):bag[U] = {}
Induction constant: Ac
Induction hypothesis:
SJLemmaInductHyp.1: x \in Ac => insert(x, Ac - x:U) = Ac
Induction subgoal:
Subgoal 2: x \in insert(u, Ac)
=> insert(x, insert(u, Ac) - x:U) = insert(u, Ac)
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A
Level 2 subgoal 1 (basis step) for proof by induction on A
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on A
Added hypothesis SJLemmaInductHyp.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.1383:
LP0.1.1384: % Base Case:
LP0.1.1385:
LP0.1.1386: normalize conjecture
The conjecture was not reduced.
The formulas cannot be ordered using the current ordering.
LP0.1.1387:
LP0.1.1388: % Inductive Case
LP0.1.1389:
LP0.1.1390: resume by =>
Creating subgoals for proof of =>
New constants: uc, xc
Hypothesis:
SJLemmaImpliesHyp.1: xc = uc \/ xc \in Ac
Subgoal:
insert(xc, insert(uc, Ac) - xc) = insert(uc, Ac)
Attempting to prove level 3 subgoal for proof of =>
Added hypothesis SJLemmaImpliesHyp.1 to the system.
Level 3 subgoal for proof of =>
[] Proved by normalization.
Level 2 subgoal 2 (induction step) for proof by induction on A:
x \in insert(u, Ac) => insert(x, insert(u, Ac) - x:U) = insert(u, Ac)
[] Proved =>.
Conjecture SJLemma.11: x:U \in A => insert(x, A - x:U):bag[U] = A
[] Proved by structural induction on `A:bag[U]'.
The formulas cannot be ordered using the current ordering.
LP0.1.1391:
LP0.1.1392: qed
All conjectures have been proved.
LP0.1.1393: % ----------------------------------------------------------
LP0.1.1394:
LP0.1.1395: % ----------------------------------------------------------
LP0.1.1396: prove A:bag[U] \I (A:bag[U] \U B) = A:bag[U]
Attempting to prove conjecture SJLemma.12: (A \I (A \U B)):bag[U] = A
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture SJLemma.12
LP0.1.1397: resume by induction on A:bag[U]
Creating subgoals for proof by structural induction on `A:bag[U]'
Basis subgoal:
Subgoal 1: ({} \I ({} \U B)):bag[U] = {}
Induction constant: Ac
Induction hypothesis:
SJLemmaInductHyp.1: Ac \I (Ac \U B) = Ac
Induction subgoal:
Subgoal 2: insert(u, Ac) \I (insert(u, Ac) \U B) = insert(u, Ac)
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A
Level 2 subgoal 1 (basis step) for proof by induction on A
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on A
Added hypothesis SJLemmaInductHyp.1 to the system.
Level 2 subgoal 2 (induction step) for proof by induction on A
[] Proved by normalization.
Conjecture SJLemma.12
[] Proved by structural induction on `A:bag[U]'.
The formulas cannot be ordered using the current ordering.
LP0.1.1398: qed
All conjectures have been proved.
LP0.1.1399: % ----------------------------------------------------------
LP0.1.1400:
LP0.1.1401: % ----------------------------------------------------------
LP0.1.1402: prove
\E B:bag[U] ((iterate (K (true), f:fun[T,U]) ! A) =
(iterate (p, f:fun[T,U]) ! A) \U B)
..
Attempting to prove conjecture SJLemma.13:
\E B:bag[U]
((iterate(K(true), f):fun[bag[T], bag[U]] ! A):bag[U]
= (iterate(p, f):fun[bag[T], bag[U]] ! A) \U B)
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture SJLemma.13
LP0.1.1403:
LP0.1.1404: resume by induction on A:bag[T]
Creating subgoals for proof by structural induction on `A:bag[T]'
Basis subgoal:
Subgoal 1: \E B:bag[U]
((iterate(K(true), f):fun[bag[T], bag[U]] ! {}):bag[U]
= (iterate(p, f):fun[bag[T], bag[U]] ! {}) \U B)
Induction constant: Ac
Induction hypothesis:
SJLemmaInductHyp.1:
\E B:bag[U]
((iterate(K(true), f) ! Ac):bag[U] = (iterate(p, f) ! Ac) \U B)
Induction subgoal:
Subgoal 2: \E B:bag[U]
((iterate(K(true), f) ! insert(t, Ac)):bag[U]
= (iterate(p, f) ! insert(t, Ac)) \U 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 SJLemmaInductHyp.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.1405:
LP0.1.1406: % Base Case: Trivial
LP0.1.1407: % Inductive Case:
LP0.1.1408:
LP0.1.1409: declare operator Bc: pred [T], fun [T, U] -> bag [U]
LP0.1.1410: fix B:bag [U] as Bc (p, f) in *Induct*
A prenex-existential quantifier in formula SJLemmaInductHyp.1 has been
eliminated to produce formula SJLemma.14,
iterate(K(true), f) ! Ac = (iterate(p, f) ! Ac) \U Bc(p, f)
The formulas cannot be ordered using the current ordering.
LP0.1.1411:
LP0.1.1412: resume by cases p ? t
Creating subgoals for proof by cases
New constants: pc, tc
Case hypotheses:
SJLemmaCaseHyp.1.1: pc ? tc
SJLemmaCaseHyp.1.2: ~(pc ? tc)
Same subgoal for all cases:
\E B:bag[U]
(insert(f ! tc, iterate(K(true), f) ! Ac):bag[U]
= (iterate(pc, f) ! insert(tc, Ac)) \U B)
Attempting to prove level 3 subgoal for case 1 (out of 2)
Added hypothesis SJLemmaCaseHyp.1.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 3 subgoal for case 1 (out of 2)
LP0.1.1413:
LP0.1.1414: % Case 1
LP0.1.1415: resume by specializing B to Bc (pc, f)
Creating subgoals for proof by specialization
Subgoal:
insert(f ! tc, iterate(K(true), f) ! Ac)
= insert(f ! tc, (iterate(pc, f) ! Ac) \U Bc(pc, f))
Attempting to prove level 4 subgoal for proof by specialization
Level 4 subgoal for proof by specialization
[] Proved by normalization.
Level 3 subgoal for case 1 (out of 2)
[] Proved by specialization.
Attempting to prove level 3 subgoal for case 2 (out of 2)
Added hypothesis SJLemmaCaseHyp.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.1416:
LP0.1.1417: % Case 2
LP0.1.1418: resume by specializing B to insert (f ! tc, Bc (pc, f))
Creating subgoals for proof by specialization
Subgoal:
insert(f ! tc, iterate(K(true), f) ! Ac)
= (iterate(pc, f) ! Ac) \U insert(f ! tc, Bc(pc, f))
Attempting to prove level 4 subgoal for proof by specialization
Level 4 subgoal for proof by specialization
[] Proved by normalization.
Level 3 subgoal for case 2 (out of 2):
\E B:bag[U]
(insert(f ! tc, iterate(K(true), f) ! Ac):bag[U]
= (iterate(pc, f) ! insert(tc, Ac)) \U B)
[] Proved by specialization.
Level 2 subgoal 2 (induction step) for proof by induction on A:
\E B:bag[U]
((iterate(K(true), f) ! insert(t, Ac)):bag[U]
= (iterate(p, f) ! insert(t, Ac)) \U B)
[] Proved by cases p ? t.
Conjecture SJLemma.13:
\E B:bag[U]
((iterate(K(true), f):fun[bag[T], bag[U]] ! A):bag[U]
= (iterate(p, f):fun[bag[T], bag[U]] ! A) \U B)
[] Proved by structural induction on `A:bag[T]'.
The formulas cannot be ordered using the current ordering.
LP0.1.1419: qed
All conjectures have been proved.
LP0.1.1420:
LP0.1.1421: % L1: Rules Used in Transformation, SimplifyJoin
LP0.1.1422: % ----------------------------------------------
LP0.1.1423:
LP0.1.1424: set order manual
Warning: the rewriting system is known to terminate, but its termination cannot
be verified with the `manual' ordering. When another rewrite rule is added, the
rewriting system will be treated as nonterminating.
The ordering-method is now `manual'.
LP0.1.1425: set name SJ1
The name-prefix is now `SJ1'.
LP0.1.1426: declare variables
A: bag [T1],
B: bag [T2],
p: pred [pair [U, V]],
f: fun [T1, U],
g: fun [T2, V],
t: T,
t2: T2,
u: U
..
LP0.1.1427: prove
join (p \oplus (f \times g), snd:fun[pair [T1,T2],T2]) ! [A, B] =
(join (p \oplus (id \times g), snd) !
[iterate (K (true), f:fun [T1, U]) ! A, B]):bag[T2]
..
Attempting to prove conjecture SJ1.1:
join(p \oplus (f \times g), snd):fun[pair[bag[T1], bag[T2]], bag[T2]]
! [A, B]
= join(p \oplus (id \times g), snd)
! [iterate(K(true), f):fun[bag[T1], bag[U]] ! A, B]
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture SJ1.1
LP0.1.1428:
LP0.1.1429: resume by induction on A:bag[T1]
Creating subgoals for proof by structural induction on `A:bag[T1]'
Basis subgoal:
Subgoal 1: join(p \oplus (f \times g),
snd):fun[pair[bag[T1], bag[T2]], bag[T2]]
! [{}, B]
= join(p \oplus (id \times g), snd)
! [iterate(K(true), f):fun[bag[T1], bag[U]] ! {}, B]
Induction constant: Ac
Induction hypothesis:
SJ1InductHyp.1:
join(p \oplus (f \times g), snd) ! [Ac, B]
= join(p \oplus (id \times g), snd) ! [iterate(K(true), f) ! Ac, B]
Induction subgoal:
Subgoal 2: join(p \oplus (f \times g), snd) ! [insert(t1, Ac), B]
= join(p \oplus (id \times g), snd)
! [iterate(K(true), f) ! insert(t1, 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 SJ1InductHyp.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.1430:
LP0.1.1431: % Base Case: Trivial
LP0.1.1432: % Inductive Case
LP0.1.1433: normalize conjecture
Level 2 subgoal 2 (induction step) for proof by induction on A
[] Proved by normalization.
Conjecture SJ1.1:
join(p \oplus (f \times g), snd):fun[pair[bag[T1], bag[T2]], bag[T2]]
! [A, B]
= join(p \oplus (id \times g), snd)
! [iterate(K(true), f):fun[bag[T1], bag[U]] ! A, B]
[] Proved by structural induction on `A:bag[T1]'.
The formulas cannot be ordered using the current ordering.
The formulas cannot be ordered using the current ordering.
LP0.1.1434:
LP0.1.1435: qed
All conjectures have been proved.
LP0.1.1436: set order noeq
The ordering-method is now `noeq-dsmpos'.
LP0.1.1437:
LP0.1.1438: set name SJ2
The name-prefix is now `SJ2'.
LP0.1.1439: declare variables
A: bag [T],
p, q: pred [T],
f: fun [T, U]
..
LP0.1.1440: prove
iterate (p, f:fun [T, U]) ! (iterate (q, id) ! A:bag[T]) =
iterate (p & q, f:fun [T, U]) ! A
..
Attempting to prove conjecture SJ2.1:
(iterate(p, f):fun[bag[T], bag[U]] ! (iterate(q, id) ! A)):bag[U]
= iterate(p & q, f):fun[bag[T], bag[U]] ! A
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture SJ2.1
LP0.1.1441:
LP0.1.1442: resume by induction on A:bag[T]
Creating subgoals for proof by structural induction on `A:bag[T]'
Basis subgoal:
Subgoal 1: (iterate(p, f):fun[bag[T], bag[U]] ! (iterate(q, id) ! {})):bag[U]
= iterate(p & q, f):fun[bag[T], bag[U]] ! {}
Induction constant: Ac
Induction hypothesis:
SJ2InductHyp.1:
(iterate(p, f) ! (iterate(q, id) ! Ac)):bag[U] = iterate(p & q, f) ! Ac
Induction subgoal:
Subgoal 2: (iterate(p, f) ! (iterate(q, id) ! insert(t, Ac))):bag[U]
= iterate(p & q, f) ! insert(t, Ac)
Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on A
Level 2 subgoal 1 (basis step) for proof by induction on A
[] Proved by normalization.
Attempting to prove level 2 subgoal 2 (induction step) for proof by induction
on A
Added hypothesis SJ2InductHyp.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.1443:
LP0.1.1444: % Base Case: Trivial
LP0.1.1445: % Inductive Case
LP0.1.1446:
LP0.1.1447: resume by cases q ? t
Creating subgoals for proof by cases
New constants: qc, tc
Case hypotheses:
SJ2CaseHyp.1.1: qc ? tc
SJ2CaseHyp.1.2: ~(qc ? tc)
Same subgoal for all cases:
(iterate(p, f) ! (iterate(qc, id) ! insert(tc, Ac))):bag[U]
= iterate(p & qc, f) ! insert(tc, Ac)
Attempting to prove level 3 subgoal for case 1 (out of 2)
Added hypothesis SJ2CaseHyp.1.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 3 subgoal for case 1 (out of 2)
LP0.1.1448:
LP0.1.1449: % Case 1
LP0.1.1450: resume by cases p ? tc
Creating subgoals for proof by cases
New constant: pc
Case hypotheses:
SJ2CaseHyp.2.1: pc ? tc
SJ2CaseHyp.2.2: ~(pc ? tc)
Same subgoal for all cases:
(iterate(pc, f) ! insert(tc, iterate(qc, id) ! Ac)):bag[U]
= iterate(pc & qc, f) ! insert(tc, Ac)
Attempting to prove level 4 subgoal for case 1 (out of 2)
Added hypothesis SJ2CaseHyp.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 SJ2CaseHyp.2.2 to the system.
Level 4 subgoal for case 2 (out of 2)
[] Proved by normalization.
Level 3 subgoal for case 1 (out of 2)
[] Proved by cases p ? tc.
Attempting to prove level 3 subgoal for case 2 (out of 2):
(iterate(p, f) ! (iterate(qc, id) ! insert(tc, Ac))):bag[U]
= iterate(p & qc, f) ! insert(tc, Ac)
Added hypothesis SJ2CaseHyp.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) ! (iterate(q, id) ! insert(t, Ac))):bag[U]
= iterate(p & q, f) ! insert(t, Ac)
[] Proved by cases q ? t.
Conjecture SJ2.1:
(iterate(p, f):fun[bag[T], bag[U]] ! (iterate(q, id) ! A)):bag[U]
= iterate(p & q, f):fun[bag[T], bag[U]] ! A
[] Proved by structural induction on `A:bag[T]'.
The formulas cannot be ordered using the current ordering.
LP0.1.1451:
LP0.1.1452: % Case 2: Trivial
LP0.1.1453:
LP0.1.1454: qed
All conjectures have been proved.
LP0.1.1455:
LP0.1.1456: set name SJ3
The name-prefix is now `SJ3'.
LP0.1.1457: declare variables
A, B: bag [T]
..
LP0.1.1458: prove set ! (join (eq, snd) ! [A, B]) = set ! (int ! [A, B])
Attempting to prove conjecture SJ3.1:
set ! (join(eq, snd) ! [A, B]) = set ! (int ! [A, B])
Conjecture SJ3.1
[] Proved by normalization.
Deleted formula SJ3.1, which reduced to `true'.
The formulas cannot be ordered using the current ordering.
LP0.1.1459: qed
All conjectures have been proved.
LP0.1.1460:
LP0.1.1461: set name SJ4
The name-prefix is now `SJ4'.
LP0.1.1462: prove
int ! [iterate (p, f:fun[T,U]) ! A, iterate (K (true), f:fun[T,U]) ! A] =
iterate (p, f:fun[T,U]) ! A
..
Attempting to prove conjecture SJ4.1:
(int
! [iterate(p, f):fun[bag[T], bag[U]] ! A,
iterate(K(true), f):fun[bag[T], bag[U]] ! A]):
bag[U]
= iterate(p, f):fun[bag[T], bag[U]] ! A
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture SJ4.1
LP0.1.1463:
LP0.1.1464: resume by contradiction
Creating subgoals for proof by contradiction
New constants: pc, fc, Ac
Hypothesis:
SJ4ContraHyp.1:
~((iterate(pc, fc) ! Ac) \I (iterate(K(true), fc) ! Ac)
= iterate(pc, fc) ! Ac)
Only subgoal:
false
Attempting to prove level 2 subgoal for proof by contradiction
Added hypothesis SJ4ContraHyp.1 to the system.
The formulas cannot be ordered using the current ordering.
Suspending proof of level 2 subgoal for proof by contradiction
LP0.1.1465:
LP0.1.1466: set immunity on
The immunity is now `on'.
LP0.1.1467: prove
\E B:bag[U] ((iterate(K(true), fc):fun[bag[T], bag[U]] ! Ac):bag[U] =
(iterate(pc, fc):fun[bag[T], bag[U]] ! Ac) \U B)
..
Attempting to prove level 3 lemma SJ4.2:
\E B:bag[U] (iterate(K(true), fc) ! Ac = (iterate(pc, fc) ! Ac) \U B)
Level 3 lemma SJ4.2
[] Proved by normalization.
Attempting to prove level 2 subgoal for proof by contradiction
The formulas cannot be ordered using the current ordering.
Suspending proof of level 2 subgoal for proof by contradiction
LP0.1.1468: set immunity off
The immunity is now `off'.
LP0.1.1469:
LP0.1.1470: declare operator Bc: pred [T], fun [T, U] -> bag [U]
LP0.1.1471: fix B:bag [U] as Bc (p, f) in SJ4 / cont-op (Ac)
A prenex-existential quantifier in formula SJ4.2 has been eliminated to produce
formula SJ4.3,
iterate(K(true), fc) ! Ac = (iterate(pc, fc) ! Ac) \U Bc(p, f)
The formulas cannot be ordered using the current ordering.
LP0.1.1472: crit-pairs SJ4 with SJLemma*
The following equations are critical pairs between rewrite rules SJ4.3 and
SJLemma.12.
SJ4.4: false
The system now contains 8 formulas and 410 rewrite rules. The rewriting system
is guaranteed to terminate.
Critical pair computation abandoned because a theorem has been proved.
Formula SJ4.4, false, is inconsistent.
Level 2 subgoal for proof by contradiction: false
[] Proved by detecting an inconsistency.
Conjecture SJ4.1:
(int
! [iterate(p, f):fun[bag[T], bag[U]] ! A,
iterate(K(true), f):fun[bag[T], bag[U]] ! A]):
bag[U]
= iterate(p, f):fun[bag[T], bag[U]] ! A
[] Proved by contradiction.
The formulas cannot be ordered using the current ordering.
LP0.1.1473:
LP0.1.1474: qed
All conjectures have been proved.
LP0.1.1475:
LP0.1.1476: set name SJ6b
The name-prefix is now `SJ6b'.
LP0.1.1477: declare variables
p: pred [T]
..
LP0.1.1478: prove p: pred [T] & K (true) = p
Attempting to prove conjecture SJ6b.1: (p & K(true)):pred[T] = p
Conjecture SJ6b.1
[] Proved by normalization.
Deleted formula SJ6b.1, which reduced to `true'.
The formulas cannot be ordered using the current ordering.
LP0.1.1479: qed
All conjectures have been proved.
LP0.1.1480:
LP0.1.1481: set name SJ7
The name-prefix is now `SJ7'.
LP0.1.1482: declare variables
f: fun [T, U]
..
LP0.1.1483: prove K (true) \oplus f = K (true)
Attempting to prove conjecture SJ7.1: K(true) \oplus f = K(true)
Conjecture SJ7.1
[] Proved by normalization.
Deleted formula SJ7.1, which reduced to `true'.
The formulas cannot be ordered using the current ordering.
LP0.1.1484: qed
All conjectures have been proved.
LP0.1.1485:
LP0.1.1486: set name SJ10
The name-prefix is now `SJ10'.
LP0.1.1487: prove
iterate (p, f:fun [U, V]) ! (join (q, g:fun [pair [T1, T2], U]) ! [A, B]) =
join (q & (p \oplus g:fun [pair [T1, T2], U]), f \circ g) ! [A, B]
..
Attempting to prove conjecture SJ10.1:
iterate(p, f):fun[bag[U], bag[V]] ! (join(q, g) ! [A, B])
= join(q & (p:pred[U] \oplus g), f \circ g) ! [A, B]
The formulas cannot be ordered using the current ordering.
Suspending proof of conjecture SJ10.1
LP0.1.1488: resume by induction on A:bag[T1]
Creating subgoals for proof by structural induction on `A:bag[T1]'
Basis subgoal:
Subgoal 1: iterate(p, f):fun[bag[U], bag[V]] ! (join(q, g) ! [{}, B])
= join(q & (p:pred[U] \oplus g), f \circ g) ! [{}, B]
Induction constant: Ac
Induction hypothesis:
SJ10InductHyp.1:
iterate(p, f):fun[bag[U], bag[V]] ! (join(q, g) ! [Ac, B])
= join(q & (p:pred[U] \oplus g), f \circ g) ! [Ac, B]
Induction subgoal:
Subgoal 2: iterate(p, f):fun[bag[U], bag[V]]
! (join(q, g) ! [insert(t1, Ac), B])
= join(q & (p:pred[U] \oplus g), f \circ g)
! [insert(t1, 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 SJ10InductHyp.1 to the system.
Level 2 subgoal 2 (induction step) for proof by induction on A
[] Proved by normalization.
Conjecture SJ10.1
[] Proved by structural induction on `A:bag[T1]'.
The formulas cannot be ordered using the current ordering.
LP0.1.1489: qed
All conjectures have been proved.
LP0.1.1490:
LP0.1.1491: quit
End of input from file `/pro/oodb/specs/KOLA98/SIGMOD98_Scripts.lp'.
End of input from file `command line arguments'.