Lemma1 : |------- {1} FORALL s: s = result(Cross_bridge(M), result(Cross_bridge(C), s0)) IMPLIES location(M, s) = Rb AND location(C, s) = Rb Rule? (SKOLEM 1 ("S")) For the top quantifier in 1, we introduce Skolem constants: (S), this simplifies to: Lemma1 : |------- {1} S = result(Cross_bridge(M), result(Cross_bridge(C), s0)) IMPLIES location(M, S) = Rb AND location(C, S) = Rb Rule? (FLATTEN 1) Applying disjunctive simplification to flatten sequent, this simplifies to: Lemma1 : {-1} S = result(Cross_bridge(M), result(Cross_bridge(C), s0)) |------- {1} location(M, S) = Rb AND location(C, S) = Rb Rule? (replace -1 (1)) Replacing using formula -1, this simplifies to: Lemma1 : [-1] S = result(Cross_bridge(M), result(Cross_bridge(C), s0)) |------- {1} location(M, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb AND location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (delete -1) Deleting some formulas, this simplifies to: Lemma1 : |------- [1] location(M, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb AND location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (LEMMA "Axiom1") Applying Axiom1 where this simplifies to: Lemma1 : {-1} (FORALL (s, p): location(p, result(Cross_bridge(p), s)) = opposite(location(p, s))) |------- [1] location(M, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb AND location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (prop) Applying propositional simplification, this yields 2 subgoals: Lemma1.1 : [-1] (FORALL (s, p): location(p, result(Cross_bridge(p), s)) = opposite(location(p, s))) |------- {1} location(M, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (QUANT?) Instantiating quantified variables, this simplifies to: Lemma1.1 : {-1} location(M, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = opposite(location(M, result(Cross_bridge(C), s0))) |------- [1] location(M, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (EXPAND "opposite") Expanding the definition of opposite, this simplifies to: Lemma1.1 : {-1} location(M, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = (IF location(M, result(Cross_bridge(C), s0)) = Lb THEN Rb ELSE Lb ENDIF) |------- [1] location(M, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (REPLACE -1 (1)) Replacing using formula -1, this simplifies to: Lemma1.1 : [-1] location(M, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = (IF location(M, result(Cross_bridge(C), s0)) = Lb THEN Rb ELSE Lb ENDIF) |------- {1} (IF location(M, result(Cross_bridge(C), s0)) = Lb THEN Rb ELSE Lb ENDIF) = Rb Rule? (REWRITE "Axiom2") Found matching substitution: s gets s0, a gets Cross_bridge(C), p gets M, Rewriting using Axiom2, this yields 2 subgoals: Lemma1.1.1 : {-1} location(M, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = (IF location(M, s0) = Lb THEN Rb ELSE Lb ENDIF) |------- {1} (IF location(M, s0) = Lb THEN Rb ELSE Lb ENDIF) = Rb Rule? (undo) This will undo the proof to: Lemma1.1 : [-1] location(M, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = (IF location(M, result(Cross_bridge(C), s0)) = Lb THEN Rb ELSE Lb ENDIF) |------- {1} (IF location(M, result(Cross_bridge(C), s0)) = Lb THEN Rb ELSE Lb ENDIF) = Rb Sure?(Y or N): y Lemma1.1 : [-1] location(M, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = (IF location(M, result(Cross_bridge(C), s0)) = Lb THEN Rb ELSE Lb ENDIF) |------- {1} (IF location(M, result(Cross_bridge(C), s0)) = Lb THEN Rb ELSE Lb ENDIF) = Rb Rule? (delete -1) Deleting some formulas, this simplifies to: Lemma1.1 : |------- [1] (IF location(M, result(Cross_bridge(C), s0)) = Lb THEN Rb ELSE Lb ENDIF) = Rb Rule? (REWRITE "Axiom2") Found matching substitution: s gets s0, a gets Cross_bridge(C), p gets M, Rewriting using Axiom2, this yields 2 subgoals: Lemma1.1.1 : |------- {1} (IF location(M, s0) = Lb THEN Rb ELSE Lb ENDIF) = Rb Rule? (LEMMA "Axiom3") Applying Axiom3 where this simplifies to: Lemma1.1.1 : {-1} location(M, s0) = Lb AND location(C, s0) = Lb |------- [1] (IF location(M, s0) = Lb THEN Rb ELSE Lb ENDIF) = Rb Rule? (flatten) Applying disjunctive simplification to flatten sequent, this simplifies to: Lemma1.1.1 : {-1} location(M, s0) = Lb {-2} location(C, s0) = Lb |------- [1] (IF location(M, s0) = Lb THEN Rb ELSE Lb ENDIF) = Rb Rule? (assert) Simplifying, rewriting, and recording with decision procedures, This completes the proof of Lemma1.1.1. Lemma1.1.2 : |------- {1} Cross_bridge(C) /= Cross_bridge(M) [2] (IF location(M, result(Cross_bridge(C), s0)) = Lb THEN Rb ELSE Lb ENDIF) = Rb Rule? (LEMMA "DAA" ("t1" "C" "t2" "M")) Applying DAA where t1 gets C, t2 gets M, this simplifies to: Lemma1.1.2 : {-1} C /= M IMPLIES Cross_bridge(C) /= Cross_bridge(M) |------- [1] Cross_bridge(C) /= Cross_bridge(M) [2] (IF location(M, result(Cross_bridge(C), s0)) = Lb THEN Rb ELSE Lb ENDIF) = Rb Rule? (split) Splitting conjunctions, this yields 2 subgoals: Lemma1.1.2.1 : {-1} Cross_bridge(C) /= Cross_bridge(M) |------- [1] Cross_bridge(C) /= Cross_bridge(M) [2] (IF location(M, result(Cross_bridge(C), s0)) = Lb THEN Rb ELSE Lb ENDIF) = Rb which is trivially true. This completes the proof of Lemma1.1.2.1. Lemma1.1.2.2 : |------- {1} C /= M [2] Cross_bridge(C) /= Cross_bridge(M) [3] (IF location(M, result(Cross_bridge(C), s0)) = Lb THEN Rb ELSE Lb ENDIF) = Rb Rule? (lemma "DNA1") Applying DNA1 where this simplifies to: Lemma1.1.2.2 : {-1} C /= M |------- [1] C /= M [2] Cross_bridge(C) /= Cross_bridge(M) [3] (IF location(M, result(Cross_bridge(C), s0)) = Lb THEN Rb ELSE Lb ENDIF) = Rb which is trivially true. This completes the proof of Lemma1.1.2.2. This completes the proof of Lemma1.1.2. This completes the proof of Lemma1.1. Lemma1.2 : [-1] (FORALL (s, p): location(p, result(Cross_bridge(p), s)) = opposite(location(p, s))) |------- {1} location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (QUANT?) Instantiating quantified variables, this simplifies to: Lemma1.2 : {-1} location(C, result(Cross_bridge(C), s0)) = opposite(location(C, s0)) |------- [1] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (EXPAND "opposite") Expanding the definition of opposite, this simplifies to: Lemma1.2 : {-1} location(C, result(Cross_bridge(C), s0)) = (IF location(C, s0) = Lb THEN Rb ELSE Lb ENDIF) |------- [1] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (REWRITE "Axiom3") No matching instance for Axiom3 found. No change on: (REWRITE "Axiom3") Lemma1.2 : {-1} location(C, result(Cross_bridge(C), s0)) = (IF location(C, s0) = Lb THEN Rb ELSE Lb ENDIF) |------- [1] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (undo) This will undo the proof to: Lemma1.2 : {-1} location(C, result(Cross_bridge(C), s0)) = opposite(location(C, s0)) |------- [1] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Sure?(Y or N): n Lemma1.2 : {-1} location(C, result(Cross_bridge(C), s0)) = (IF location(C, s0) = Lb THEN Rb ELSE Lb ENDIF) |------- [1] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (LEMMA "Axiom3") Applying Axiom3 where this simplifies to: Lemma1.2 : {-1} location(M, s0) = Lb AND location(C, s0) = Lb [-2] location(C, result(Cross_bridge(C), s0)) = (IF location(C, s0) = Lb THEN Rb ELSE Lb ENDIF) |------- [1] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (flatten) Applying disjunctive simplification to flatten sequent, this simplifies to: Lemma1.2 : {-1} location(M, s0) = Lb {-2} location(C, s0) = Lb [-3] location(C, result(Cross_bridge(C), s0)) = (IF location(C, s0) = Lb THEN Rb ELSE Lb ENDIF) |------- [1] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (assert) Simplifying, rewriting, and recording with decision procedures, this simplifies to: Lemma1.2 : [-1] location(M, s0) = Lb [-2] location(C, s0) = Lb {-3} location(C, result(Cross_bridge(C), s0)) = Rb |------- [1] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (LEMMA "Axiom2" ("s" "result(Cross_bridge(C), s0)" "a" "Cross_bridge(M)" "p" "C")) Applying Axiom2 where s gets result(Cross_bridge(C), s0), a gets Cross_bridge(M), p gets C, this simplifies to: Lemma1.2 : {-1} Cross_bridge(M) /= Cross_bridge(C) IMPLIES location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = location(C, result(Cross_bridge(C), s0)) [-2] location(M, s0) = Lb [-3] location(C, s0) = Lb [-4] location(C, result(Cross_bridge(C), s0)) = Rb |------- [1] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (delete -2 -3) Deleting some formulas, this simplifies to: Lemma1.2 : [-1] Cross_bridge(M) /= Cross_bridge(C) IMPLIES location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = location(C, result(Cross_bridge(C), s0)) [-2] location(C, result(Cross_bridge(C), s0)) = Rb |------- [1] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (split) Splitting conjunctions, this yields 2 subgoals: Lemma1.2.1 : {-1} location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = location(C, result(Cross_bridge(C), s0)) [-2] location(C, result(Cross_bridge(C), s0)) = Rb |------- [1] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (replace -2 (-1)) Replacing using formula -2, this simplifies to: Lemma1.2.1 : {-1} location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb [-2] location(C, result(Cross_bridge(C), s0)) = Rb |------- [1] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb which is trivially true. This completes the proof of Lemma1.2.1. Lemma1.2.2 : [-1] location(C, result(Cross_bridge(C), s0)) = Rb |------- {1} Cross_bridge(M) /= Cross_bridge(C) [2] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (LEMMA "DAA" ("t1" "M" "t2" "C")) Applying DAA where t1 gets M, t2 gets C, this simplifies to: Lemma1.2.2 : {-1} M /= C IMPLIES Cross_bridge(M) /= Cross_bridge(C) [-2] location(C, result(Cross_bridge(C), s0)) = Rb |------- [1] Cross_bridge(M) /= Cross_bridge(C) [2] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (split) Splitting conjunctions, this yields 2 subgoals: Lemma1.2.2.1 : {-1} Cross_bridge(M) /= Cross_bridge(C) [-2] location(C, result(Cross_bridge(C), s0)) = Rb |------- [1] Cross_bridge(M) /= Cross_bridge(C) [2] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb which is trivially true. This completes the proof of Lemma1.2.2.1. Lemma1.2.2.2 : [-1] location(C, result(Cross_bridge(C), s0)) = Rb |------- {1} M /= C [2] Cross_bridge(M) /= Cross_bridge(C) [3] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (LEMMA "DNA1") Applying DNA1 where this simplifies to: Lemma1.2.2.2 : {-1} C /= M [-2] location(C, result(Cross_bridge(C), s0)) = Rb |------- [1] M /= C [2] Cross_bridge(M) /= Cross_bridge(C) [3] location(C, result(Cross_bridge(M), result(Cross_bridge(C), s0))) = Rb Rule? (assert) Simplifying, rewriting, and recording with decision procedures, This completes the proof of Lemma1.2.2.2. This completes the proof of Lemma1.2.2. This completes the proof of Lemma1.2. Q.E.D. Run time = 8.58 secs. Real time = 590.11 secs. Wrote proof file /u8/eyal/ongo/cs323/pvs/mcp1.prf NIL