LP (the Larch Prover), Release 3.1b (98/06/09) logging to `/users/myoeli/AY_DIR/LPGUIDE/nmutex.lplog' on 12 November 2000 23:03:53. LP1.5: set script nmutex Input is being recorded now in `/users/myoeli/AY_DIR/LPGUIDE/nmutex.lpscr'. LP1.6: clear LP1.7: set trace 1 The trace-level is now 1. LP1.8: set page-mode on Page-mode is now `on'. LP1.9: LP1.10: % Axioms for the natural numbers under addition LP1.11: LP1.12: set name nat The name-prefix is now `nat'. LP1.13: declare sort Nat LP1.14: declare variables i, j: Nat LP1.15: declare operators 0 : -> Nat s : Nat -> Nat .. LP1.16: assert s(i) = s(j) <=> i = j; 0 ~= s(i) .. Added 2 facts named nat.1, nat.2 to the system. The system now contains 2 rewrite rules. The rewriting system is guaranteed to terminate. LP1.17: LP1.18: LP1.19: % Axioms for trees LP1.20: LP1.21: set name tree The name-prefix is now `tree'. LP1.22: declare sort Node LP1.23: declare variables x, y, z: Node LP1.24: declare operators root : -> Node L : Node -> Node R : Node -> Node level : Node -> Nat .. LP1.25: LP1.26: assert sort Node generated by root, L, R; level(root) = 0; level(L(x)) = s(level(x)); level(R(x)) = s(level(x)) .. Added 4 facts named tree.1, ..., tree.4 to the system. The system now contains 5 rewrite rules. The rewriting system is guaranteed to terminate. LP1.27: LP1.28: LP1.29: % Axioms for arbiter LP1.30: LP1.31: set name invariant The name-prefix is now `invariant'. LP1.32: declare operators gr, req : Node -> Bool LP1.33: assert ~(gr(L(x)) /\ gr(R(x))); (gr(L(x)) \/ gr(R(x))) => (gr(x)/\req(x)) .. Added 2 facts named invariant.1, invariant.2 to the system. The system now contains 7 rewrite rules. The rewriting system is guaranteed to terminate. LP1.34: LP1.35: set name nmutex The name-prefix is now `nmutex'. LP1.36: set proof-method normalization The proof-methods are now `normalization'. LP1.37: prove level(y) = level(z) /\ gr(y) /\ gr(z) => y = z Attempting to prove conjecture nmutex.1: level(y) = level(z) /\ gr(y) /\ gr(z) => y = z Suspending proof of conjecture nmutex.1 LP1.38: resume by induction on y Creating subgoals for proof by structural induction on `y' Basis subgoal: Subgoal 1: level(root) = level(z) /\ gr(root) /\ gr(z) => root = z Induction constant: yc Induction hypothesis: nmutexInductHyp.1: level(yc) = level(z) /\ gr(yc) /\ gr(z) => yc = z Induction subgoals: Subgoal 2: level(L(yc)) = level(z) /\ gr(L(yc)) /\ gr(z) => L(yc) = z Subgoal 3: level(R(yc)) = level(z) /\ gr(R(yc)) /\ gr(z) => R(yc) = z Attempting to prove level 2 subgoal 1 (basis step) for proof by induction on y Suspending proof of level 2 subgoal 1 (basis step) for proof by induction on y LP1.39: resume by induction on z % To prove basis of induction on y Creating subgoals for proof by structural induction on `z' Basis subgoal: Subgoal 1: 0 = level(root) /\ gr(root) /\ gr(root) => root = root Induction constant: zc Induction hypothesis: nmutexInductHyp.1: 0 = level(zc) /\ gr(root) /\ gr(zc) => root = zc Induction subgoals: Subgoal 2: 0 = level(L(zc)) /\ gr(L(zc)) /\ gr(root) => root = L(zc) Subgoal 3: 0 = level(R(zc)) /\ gr(R(zc)) /\ gr(root) => root = R(zc) Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on z Level 3 subgoal 1 (basis step) for proof by induction on z [] Proved by normalization. Attempting to prove level 3 subgoal 2 (induction step) for proof by induction on z Added hypothesis nmutexInductHyp.1 to the system. Level 3 subgoal 2 (induction step) for proof by induction on z [] Proved by normalization. Attempting to prove level 3 subgoal 3 (induction step) for proof by induction on z Level 3 subgoal 3 (induction step) for proof by induction on z [] Proved by normalization. Level 2 subgoal 1 (basis step) for proof by induction on y [] Proved by structural induction on `z'. Attempting to prove level 2 subgoal 2 (induction step) for proof by induction on y Added hypothesis nmutexInductHyp.1 to the system. The system now contains 8 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 2 subgoal 2 (induction step) for proof by induction on y LP1.40: resume by induction on z % To prove first induction step of induction on y Creating subgoals for proof by structural induction on `z' Basis subgoal: Subgoal 1: s(level(yc)) = level(root) /\ gr(L(yc)) /\ gr(root) => L(yc) = root Induction constant: zc Induction hypothesis: nmutexInductHyp.2: s(level(yc)) = level(zc) /\ gr(L(yc)) /\ gr(zc) => L(yc) = zc Induction subgoals: Subgoal 2: s(level(yc)) = level(L(zc)) /\ gr(L(yc)) /\ gr(L(zc)) => L(yc) = L(zc) Subgoal 3: s(level(yc)) = level(R(zc)) /\ gr(L(yc)) /\ gr(R(zc)) => L(yc) = R(zc) Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on z Level 3 subgoal 1 (basis step) for proof by induction on z [] Proved by normalization. Attempting to prove level 3 subgoal 2 (induction step) for proof by induction on z Added hypothesis nmutexInductHyp.2 to the system. The system now contains 9 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 3 subgoal 2 (induction step) for proof by induction on z LP1.41: resume by case yc = zc Creating subgoals for proof by cases Case hypotheses: nmutexCaseHyp.1.1: yc = zc nmutexCaseHyp.1.2: ~(yc = zc) Same subgoal for all cases: level(yc) = level(zc) /\ gr(L(yc)) /\ gr(L(zc)) => L(yc) = L(zc) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis nmutexCaseHyp.1.1 to the system. Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis nmutexCaseHyp.1.2 to the system. The system now contains 10 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 4 subgoal for case 2 (out of 2) LP1.42: resume by => Creating subgoals for proof of => Hypothesis: nmutexImpliesHyp.1: level(yc) = level(zc) /\ gr(L(yc)) /\ gr(L(zc)) Subgoal: L(yc) = L(zc) Attempting to prove level 5 subgoal for proof of => Added hypothesis nmutexImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula nmutexImpliesHyp.1 to yield the following formulas, which imply nmutexImpliesHyp.1. nmutexImpliesHyp.1.1: level(yc) = level(zc) nmutexImpliesHyp.1.2: gr(L(yc)) nmutexImpliesHyp.1.3: gr(L(zc)) The system now contains 13 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 5 subgoal for proof of => LP1.43: critical-pairs *Hyp with * The following equations are critical pairs between rewrite rules nmutexCaseHyp.1.2 and nmutexInductHyp.1. nmutex.2: ~(gr(yc) /\ gr(zc)) The system now contains 1 formula and 13 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.2 and invariant.1. nmutex.3: ~gr(R(yc)) The system now contains 1 formula and 14 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.2 and invariant.2. nmutex.4: gr(yc) /\ req(yc) nmutex.5: gr(L(L(yc))) \/ gr(R(L(yc))) => req(L(yc)) The system now contains 2 formulas and 15 rewrite rules. The rewriting system is guaranteed to terminate. Deduction rule lp_and_is_true has been applied to formula nmutex.4 to yield the following formulas, which imply nmutex.4. nmutex.4.1: gr(yc) nmutex.4.2: req(yc) Deleted formula nmutexInductHyp.2, which reduced to `true'. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.3 and invariant.1. nmutex.6: ~gr(R(zc)) The system now contains 1 formula and 17 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.3 and invariant.2. nmutex.7: false nmutex.8: gr(L(L(zc))) \/ gr(R(L(zc))) => req(L(zc)) The system now contains 2 formulas and 18 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Formula nmutex.7, false, is inconsistent. Level 5 subgoal for proof of =>: L(yc) = L(zc) [] Proved by inconsistent hypothesis. Level 4 subgoal for case 2 (out of 2): level(yc) = level(zc) /\ gr(L(yc)) /\ gr(L(zc)) => L(yc) = L(zc) [] Proved =>. Level 3 subgoal 2 (induction step) for proof by induction on z: s(level(yc)) = level(L(zc)) /\ gr(L(yc)) /\ gr(L(zc)) => L(yc) = L(zc) [] Proved by cases yc = zc. Attempting to prove level 3 subgoal 3 (induction step) for proof by induction on z: s(level(yc)) = level(R(zc)) /\ gr(L(yc)) /\ gr(R(zc)) => L(yc) = R(zc) The system now contains 9 rewrite rules. The rewriting system is guaranteed to terminate. LP1.44: resume by case yc = zc Creating subgoals for proof by cases Case hypotheses: nmutexCaseHyp.1.1: yc = zc nmutexCaseHyp.1.2: ~(yc = zc) Same subgoal for all cases: level(yc) = level(zc) /\ gr(L(yc)) /\ gr(R(zc)) => L(yc) = R(zc) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis nmutexCaseHyp.1.1 to the system. Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis nmutexCaseHyp.1.2 to the system. The system now contains 10 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 4 subgoal for case 2 (out of 2) LP1.45: resume by => Creating subgoals for proof of => Hypothesis: nmutexImpliesHyp.1: level(yc) = level(zc) /\ gr(L(yc)) /\ gr(R(zc)) Subgoal: L(yc) = R(zc) Attempting to prove level 5 subgoal for proof of => Added hypothesis nmutexImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula nmutexImpliesHyp.1 to yield the following formulas, which imply nmutexImpliesHyp.1. nmutexImpliesHyp.1.1: level(yc) = level(zc) nmutexImpliesHyp.1.2: gr(L(yc)) nmutexImpliesHyp.1.3: gr(R(zc)) The system now contains 13 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 5 subgoal for proof of => LP1.46: critical-pairs *Hyp with * The following equations are critical pairs between rewrite rules nmutexCaseHyp.1.2 and nmutexInductHyp.1. nmutex.2: ~(gr(yc) /\ gr(zc)) The system now contains 1 formula and 13 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.2 and invariant.1. nmutex.3: ~gr(R(yc)) The system now contains 1 formula and 14 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.2 and invariant.2. nmutex.4: gr(yc) /\ req(yc) nmutex.5: gr(L(L(yc))) \/ gr(R(L(yc))) => req(L(yc)) The system now contains 2 formulas and 15 rewrite rules. The rewriting system is guaranteed to terminate. Deduction rule lp_and_is_true has been applied to formula nmutex.4 to yield the following formulas, which imply nmutex.4. nmutex.4.1: gr(yc) nmutex.4.2: req(yc) Deleted formula nmutexInductHyp.2, which reduced to `true'. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.3 and invariant.1. nmutex.6: ~gr(L(zc)) The system now contains 1 formula and 17 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.3 and invariant.2. nmutex.7: false nmutex.8: gr(L(R(zc))) \/ gr(R(R(zc))) => req(R(zc)) The system now contains 2 formulas and 18 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Formula nmutex.7, false, is inconsistent. Level 5 subgoal for proof of =>: L(yc) = R(zc) [] Proved by inconsistent hypothesis. Level 4 subgoal for case 2 (out of 2): level(yc) = level(zc) /\ gr(L(yc)) /\ gr(R(zc)) => L(yc) = R(zc) [] Proved =>. Level 3 subgoal 3 (induction step) for proof by induction on z: s(level(yc)) = level(R(zc)) /\ gr(L(yc)) /\ gr(R(zc)) => L(yc) = R(zc) [] Proved by cases yc = zc. Level 2 subgoal 2 (induction step) for proof by induction on y: level(L(yc)) = level(z) /\ gr(L(yc)) /\ gr(z) => L(yc) = z [] Proved by structural induction on `z'. Attempting to prove level 2 subgoal 3 (induction step) for proof by induction on y: level(R(yc)) = level(z) /\ gr(R(yc)) /\ gr(z) => R(yc) = z The system now contains 8 rewrite rules. The rewriting system is guaranteed to terminate. LP1.47: resume by induction on z % To prove second induction step of induction on y Creating subgoals for proof by structural induction on `z' Basis subgoal: Subgoal 1: s(level(yc)) = level(root) /\ gr(R(yc)) /\ gr(root) => R(yc) = root Induction constant: zc Induction hypothesis: nmutexInductHyp.2: s(level(yc)) = level(zc) /\ gr(R(yc)) /\ gr(zc) => R(yc) = zc Induction subgoals: Subgoal 2: s(level(yc)) = level(L(zc)) /\ gr(L(zc)) /\ gr(R(yc)) => R(yc) = L(zc) Subgoal 3: s(level(yc)) = level(R(zc)) /\ gr(R(yc)) /\ gr(R(zc)) => R(yc) = R(zc) Attempting to prove level 3 subgoal 1 (basis step) for proof by induction on z Level 3 subgoal 1 (basis step) for proof by induction on z [] Proved by normalization. Attempting to prove level 3 subgoal 2 (induction step) for proof by induction on z Added hypothesis nmutexInductHyp.2 to the system. The system now contains 9 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 3 subgoal 2 (induction step) for proof by induction on z LP1.48: resume by case yc = zc Creating subgoals for proof by cases Case hypotheses: nmutexCaseHyp.1.1: yc = zc nmutexCaseHyp.1.2: ~(yc = zc) Same subgoal for all cases: level(yc) = level(zc) /\ gr(L(zc)) /\ gr(R(yc)) => R(yc) = L(zc) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis nmutexCaseHyp.1.1 to the system. Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis nmutexCaseHyp.1.2 to the system. The system now contains 10 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 4 subgoal for case 2 (out of 2) LP1.49: resume by => Creating subgoals for proof of => Hypothesis: nmutexImpliesHyp.1: level(yc) = level(zc) /\ gr(L(zc)) /\ gr(R(yc)) Subgoal: R(yc) = L(zc) Attempting to prove level 5 subgoal for proof of => Added hypothesis nmutexImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula nmutexImpliesHyp.1 to yield the following formulas, which imply nmutexImpliesHyp.1. nmutexImpliesHyp.1.1: level(yc) = level(zc) nmutexImpliesHyp.1.2: gr(L(zc)) nmutexImpliesHyp.1.3: gr(R(yc)) The system now contains 13 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 5 subgoal for proof of => LP1.50: critical-pairs *Hyp with * The following equations are critical pairs between rewrite rules nmutexCaseHyp.1.2 and nmutexInductHyp.1. nmutex.2: ~(gr(yc) /\ gr(zc)) The system now contains 1 formula and 13 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.2 and invariant.1. nmutex.3: ~gr(R(zc)) The system now contains 1 formula and 14 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.2 and invariant.2. nmutex.4: gr(zc) /\ req(zc) nmutex.5: gr(L(L(zc))) \/ gr(R(L(zc))) => req(L(zc)) The system now contains 2 formulas and 15 rewrite rules. The rewriting system is guaranteed to terminate. Deduction rule lp_and_is_true has been applied to formula nmutex.4 to yield the following formulas, which imply nmutex.4. nmutex.4.1: gr(zc) nmutex.4.2: req(zc) Deleted formula nmutexInductHyp.1, which reduced to `true'. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.3 and invariant.1. nmutex.6: ~gr(L(yc)) The system now contains 1 formula and 17 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.3 and invariant.2. nmutex.7: false nmutex.8: gr(L(R(yc))) \/ gr(R(R(yc))) => req(R(yc)) The system now contains 2 formulas and 18 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Formula nmutex.7, false, is inconsistent. Level 5 subgoal for proof of =>: R(yc) = L(zc) [] Proved by inconsistent hypothesis. Level 4 subgoal for case 2 (out of 2): level(yc) = level(zc) /\ gr(L(zc)) /\ gr(R(yc)) => R(yc) = L(zc) [] Proved =>. Level 3 subgoal 2 (induction step) for proof by induction on z: s(level(yc)) = level(L(zc)) /\ gr(L(zc)) /\ gr(R(yc)) => R(yc) = L(zc) [] Proved by cases yc = zc. Attempting to prove level 3 subgoal 3 (induction step) for proof by induction on z: s(level(yc)) = level(R(zc)) /\ gr(R(yc)) /\ gr(R(zc)) => R(yc) = R(zc) The system now contains 9 rewrite rules. The rewriting system is guaranteed to terminate. LP1.51: resume by case yc = zc Creating subgoals for proof by cases Case hypotheses: nmutexCaseHyp.1.1: yc = zc nmutexCaseHyp.1.2: ~(yc = zc) Same subgoal for all cases: level(yc) = level(zc) /\ gr(R(yc)) /\ gr(R(zc)) => R(yc) = R(zc) Attempting to prove level 4 subgoal for case 1 (out of 2) Added hypothesis nmutexCaseHyp.1.1 to the system. Level 4 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 4 subgoal for case 2 (out of 2) Added hypothesis nmutexCaseHyp.1.2 to the system. The system now contains 10 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 4 subgoal for case 2 (out of 2) LP1.52: resume by => Creating subgoals for proof of => Hypothesis: nmutexImpliesHyp.1: level(yc) = level(zc) /\ gr(R(yc)) /\ gr(R(zc)) Subgoal: R(yc) = R(zc) Attempting to prove level 5 subgoal for proof of => Added hypothesis nmutexImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula nmutexImpliesHyp.1 to yield the following formulas, which imply nmutexImpliesHyp.1. nmutexImpliesHyp.1.1: level(yc) = level(zc) nmutexImpliesHyp.1.2: gr(R(yc)) nmutexImpliesHyp.1.3: gr(R(zc)) The system now contains 13 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 5 subgoal for proof of => LP1.53: critical-pairs *Hyp with * The following equations are critical pairs between rewrite rules nmutexCaseHyp.1.2 and nmutexInductHyp.1. nmutex.2: ~(gr(yc) /\ gr(zc)) The system now contains 1 formula and 13 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.2 and invariant.1. nmutex.3: ~gr(L(yc)) The system now contains 1 formula and 14 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.2 and invariant.2. nmutex.4: gr(yc) /\ req(yc) nmutex.5: gr(L(R(yc))) \/ gr(R(R(yc))) => req(R(yc)) The system now contains 2 formulas and 15 rewrite rules. The rewriting system is guaranteed to terminate. Deduction rule lp_and_is_true has been applied to formula nmutex.4 to yield the following formulas, which imply nmutex.4. nmutex.4.1: gr(yc) nmutex.4.2: req(yc) Deleted formula nmutexInductHyp.2, which reduced to `true'. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.3 and invariant.1. nmutex.6: ~gr(L(zc)) The system now contains 1 formula and 17 rewrite rules. The rewriting system is guaranteed to terminate. The following equations are critical pairs between rewrite rules nmutexImpliesHyp.1.3 and invariant.2. nmutex.7: false nmutex.8: gr(L(R(zc))) \/ gr(R(R(zc))) => req(R(zc)) The system now contains 2 formulas and 18 rewrite rules. The rewriting system is guaranteed to terminate. Critical pair computation abandoned because a theorem has been proved. Formula nmutex.7, false, is inconsistent. Level 5 subgoal for proof of =>: R(yc) = R(zc) [] Proved by inconsistent hypothesis. Level 4 subgoal for case 2 (out of 2): level(yc) = level(zc) /\ gr(R(yc)) /\ gr(R(zc)) => R(yc) = R(zc) [] Proved =>. Level 3 subgoal 3 (induction step) for proof by induction on z: s(level(yc)) = level(R(zc)) /\ gr(R(yc)) /\ gr(R(zc)) => R(yc) = R(zc) [] Proved by cases yc = zc. Level 2 subgoal 3 (induction step) for proof by induction on y: level(R(yc)) = level(z) /\ gr(R(yc)) /\ gr(z) => R(yc) = z [] Proved by structural induction on `z'. Conjecture nmutex.1: level(y) = level(z) /\ gr(y) /\ gr(z) => y = z [] Proved by structural induction on `y'. The system now contains 8 rewrite rules. The rewriting system is guaranteed to terminate. LP1.54: qed All conjectures have been proved. LP1.55: statistics Statistics as of 12 November 2000 23:07:35. Recent Success Failure Total ------ Count Time Count Time Time Ordering 78 0.05 25 0.01 0.06 Rewriting 242 0.09 3136 0.61 0.70 Deductions 20 0.05 78 0.00 0.05 Unification 48 0.03 152 0.03 0.06 Prover 1.02 GC's 2 Total time 2.01 Heap size = 157,652 words Free space = 5,722,432 words End of input from file `/users/myoeli/AY_DIR/LPGUIDE/nmutex.lp'. LP2: q