Verbose proof for Lemma1.

Lemma1:

{1} ∀ s : s = result(Cross bridge(M), result(Cross bridge(C), s_{0})) ⊃ location(M, s) = Rb ∧ location(C, s) = Rb

For the top quantifier in 1, we introduce Skolem constants: (S ),

Lemma1:

{1} S = result(Cross bridge(M), result(Cross bridge(C), s_{0})) ⊃ location(M, S) = Rb ∧ location(C, S) = Rb

Applying disjunctive simplification to flatten sequent,

Lemma1:

{-1} S = result(Cross bridge(M), result(Cross bridge(C), s_{0})) ; {1} location(M, S) = Rb ∧ location(C, S) = Rb

Replacing using formula -1,

Lemma1:

{-1} S = result(Cross bridge(M), result(Cross bridge(C), s_{0})) ; {1} location(M, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb∧ location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Deleting some formulas,

Lemma1:

{1} location(M, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb∧ location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Applying Axiom1 where

Lemma1:

{-1} (∀ (s, p) : location(p, result(Cross bridge(p), s)) = opposite(location(p, s))) ; {1} location(M, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb∧ location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Applying propositional simplification, we get 2 subgoals:

Lemma1.1:

{-1} (∀ (s, p) : location(p, result(Cross bridge(p), s)) = opposite(location(p, s))) ; {1} location(M, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Instantiating quantified variables,

Lemma1.1:

{-1} location(M, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = opposite(location(M, result(Cross bridge(C), s_{0}))) ; [1] location(M, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Expanding the definition of opposite ,

Lemma1.1:

{-1} location(M, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = (if location(M, result(Cross bridge(C), s_{0})) = Lb then Rb else Lb endif) ; [1] location(M, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Replacing using formula -1,

Lemma1.1:

{-1} location(M, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = (if location(M, result(Cross bridge(C), s_{0})) = Lb then Rb else Lb endif) ; {1} (if location(M, result(Cross bridge(C), s_{0})) = Lb then Rb else Lb endif) = Rb

Deleting some formulas,

Lemma1.1:

{1} (if location(M, result(Cross bridge(C), s_{0})) = Lb then Rb else Lb endif) = Rb

Rewriting using Axiom2 ,

we get 2 subgoals:

Lemma1.1.1:

{1} (if location(M, s_{0}) = Lb then Rb else Lb endif) = Rb

Applying Axiom3 where

Lemma1.1.1:

{-1} location(M, s_{0}) = Lb ∧ location(C, s_{0}) = Lb ; [1] (if location(M, s_{0}) = Lb then Rb else Lb endif) = Rb

Applying disjunctive simplification to flatten sequent,

Lemma1.1.1:

{-1} location(M, s_{0}) = Lb
{-2} location(C, s_{0}) = Lb
[1] (if location(M, s_{0}) = Lb then Rb else Lb endif) = Rb

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), s_{0})) = Lb then Rb

else Lb

endif) = Rb

Applying DAA where t1 gets C , t2 gets M ,

Lemma1.1.2:

{-1} C ≠ M ⊃ Cross bridge(C) ≠ Cross bridge(M)
[1] Cross bridge(C) ≠ Cross bridge(M)

[2] (if location(M, result(Cross bridge(C), s_{0})) = Lb then Rb

else Lb

endif) = Rb

Splitting conjunctions,

we get 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), s_{0})) = 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), s_{0})) = Lb then Rb

else Lb

endif) = Rb

Applying DNA1 where

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), s_{0})) = Lb then Rb

else Lb

endif) = Rb

which is trivially true. This completes the proof of Lemma1.1.2.2.

Lemma1.2:

{-1} (∀ (s, p) : location(p, result(Cross bridge(p), s)) = opposite(location(p, s))) ; {1} location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Instantiating quantified variables,

Lemma1.2:

{-1} location(C, result(Cross bridge(C), s_{0})) = opposite(location(C, s_{0})) ; [1] location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Expanding the definition of opposite ,

Lemma1.2:

{-1} location(C, result(Cross bridge(C), s_{0})) = (if location(C, s_{0}) = Lb then Rb else Lb endif) ; [1] location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Applying Axiom3 where

Lemma1.2:

{-1} location(M, s_{0}) = Lb ∧ location(C, s_{0}) = Lb

{-2} location(C, result(Cross bridge(C), s_{0})) =

(if location(C, s_{0}) = Lb then Rb else Lb endif)

[1] location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Applying disjunctive simplification to flatten sequent,

Lemma1.2:

{-1} location(M, s_{0}) = Lb
{-2} location(C, s_{0}) = Lb

{-3} location(C, result(Cross bridge(C), s_{0})) =

(if location(C, s_{0}) = Lb then Rb else Lb endif)

[1] location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Simplifying, rewriting, and recording with decision procedures,

Lemma1.2:

{-1} location(M, s_{0}) = Lb
{-2} location(C, s_{0}) = Lb
{-3} location(C, result(Cross bridge(C), s_{0})) = Rb
[1] location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Applying Axiom2 where s gets result(Cross bridge(C), s_{0}) , a gets Cross bridge(M) , p gets C ,

Lemma1.2:

{-1} Cross bridge(M) ≠ Cross bridge(C) ⊃ location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = location(C, result(Cross bridge(C), s_{0}))

{-2} location(M, s_{0}) = Lb
{-3} location(C, s_{0}) = Lb
{-4} location(C, result(Cross bridge(C), s_{0})) = Rb
[1] location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Deleting some formulas,

Lemma1.2:

{-1} Cross bridge(M) ≠ Cross bridge(C) ⊃ location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = location(C, result(Cross bridge(C), s_{0}))

{-2} location(C, result(Cross bridge(C), s_{0})) = Rb
[1] location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Splitting conjunctions, we get 2 subgoals:

Lemma1.2.1:

{-1} location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) =

location(C, result(Cross bridge(C), s_{0}))

{-2} location(C, result(Cross bridge(C), s_{0})) = Rb
[1] location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Replacing using formula -2,

Lemma1.2.1:

{-1} location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb
[-2] location(C, result(Cross bridge(C), s_{0})) = Rb
[1] location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

which is trivially true. This completes the proof of Lemma1.2.1.

Lemma1.2.2:

{-1} location(C, result(Cross bridge(C), s_{0})) = Rb
{1} Cross bridge(M) ≠ Cross bridge(C)
[2] location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Applying DAA where t1 gets M , t2 gets C ,

Lemma1.2.2:

{-1} M ≠ C ⊃ Cross bridge(M) ≠ Cross bridge(C)
[-2] location(C, result(Cross bridge(C), s_{0})) = Rb
[1] Cross bridge(M) ≠ Cross bridge(C)
[2] location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Splitting conjunctions, we get 2 subgoals:

Lemma1.2.2.1:

{-1} Cross bridge(M) ≠ Cross bridge(C)
[-2] location(C, result(Cross bridge(C), s_{0})) = Rb
[1] Cross bridge(M) ≠ Cross bridge(C)
[2] location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = 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), s_{0})) = Rb
{1} M ≠ C
[2] Cross bridge(M) ≠ Cross bridge(C)
[3] location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Applying DNA1 where

Lemma1.2.2.2:

{-1} C ≠ M
[-2] location(C, result(Cross bridge(C), s_{0})) = Rb
[1] M ≠ C
[2] Cross bridge(M) ≠ Cross bridge(C)
[3] location(C, result(Cross bridge(M), result(Cross bridge(C), s_{0}))) = Rb

Simplifying, rewriting, and recording with decision procedures, This completes the proof of Lemma1.2.2.2. Q.E.D.