Welcome to Abella 1.1.3-dev2
Reading clauses from ccs.mod
Abella < Theorem mu_id_step_absurd :
forall A Q, {step (mu (x1\x1)) A Q} -> false.
1 subgoal(s).
============================
forall A Q, {step (mu (x1\x1)) A Q} -> false
mu_id_step_absurd < induction on 1.
1 subgoal(s).
IH : forall A Q, {step (mu (x1\x1)) A Q}* -> false
============================
forall A Q, {step (mu (x1\x1)) A Q}@ -> false
mu_id_step_absurd < intros.
1 subgoal(s).
Variables: A, Q
IH : forall A Q, {step (mu (x1\x1)) A Q}* -> false
H1 : {step (mu (x1\x1)) A Q}@
============================
false
mu_id_step_absurd < case H1.
1 subgoal(s).
Variables: A, Q
IH : forall A Q, {step (mu (x1\x1)) A Q}* -> false
H2 : {step (mu (x1\x1)) A Q}*
============================
false
mu_id_step_absurd < apply IH to H2.
Proof completed.
Abella < CoDefine sim P Q := forall A P1, {step P A P1} -> (exists Q1, {step Q A Q1} /\ sim P1 Q1).
Abella < Theorem sim_mu_par_ext :
forall P Q Q1, {step Q a (par Q Q1)} -> sim (mu (x1\out a x1)) Q.
1 subgoal(s).
============================
forall P Q Q1, {step Q a (par Q Q1)} -> sim (mu (x1\out a x1)) Q
sim_mu_par_ext < coinduction.
1 subgoal(s).
CH : forall P Q Q1, {step Q a (par Q Q1)} -> sim (mu (x1\out a x1)) Q +
============================
forall P Q Q1, {step Q a (par Q Q1)} -> sim (mu (x1\out a x1)) Q @
sim_mu_par_ext < intros.
1 subgoal(s).
Variables: P, Q, Q1
CH : forall P Q Q1, {step Q a (par Q Q1)} -> sim (mu (x1\out a x1)) Q +
H1 : {step Q a (par Q Q1)}
============================
sim (mu (x1\out a x1)) Q @
sim_mu_par_ext < unfold.
1 subgoal(s).
Variables: P, Q, Q1
CH : forall P Q Q1, {step Q a (par Q Q1)} -> sim (mu (x1\out a x1)) Q +
H1 : {step Q a (par Q Q1)}
============================
forall A P1, {step (mu (x1\out a x1)) A P1} -> (exists Q1,
{step Q A Q1} /\ sim P1 Q1 +)
sim_mu_par_ext < intros.
1 subgoal(s).
Variables: P, Q, Q1, A, P1
CH : forall P Q Q1, {step Q a (par Q Q1)} -> sim (mu (x1\out a x1)) Q +
H1 : {step Q a (par Q Q1)}
H2 : {step (mu (x1\out a x1)) A P1}
============================
exists Q1, {step Q A Q1} /\ sim P1 Q1 +
sim_mu_par_ext < case H2.
1 subgoal(s).
Variables: P, Q, Q1, A, P1
CH : forall P Q Q1, {step Q a (par Q Q1)} -> sim (mu (x1\out a x1)) Q +
H1 : {step Q a (par Q Q1)}
H3 : {step (out a (mu (x1\out a x1))) A P1}
============================
exists Q1, {step Q A Q1} /\ sim P1 Q1 +
sim_mu_par_ext < case H3.
1 subgoal(s).
Variables: P, Q, Q1, A, P1
CH : forall P Q Q1, {step Q a (par Q Q1)} -> sim (mu (x1\out a x1)) Q +
H1 : {step Q a (par Q Q1)}
============================
exists Q1, {step Q a Q1} /\ sim (mu (x1\out a x1)) Q1 +
sim_mu_par_ext < assert {step (par Q Q1) a (par (par Q Q1) Q1)}.
1 subgoal(s).
Variables: P, Q, Q1, A, P1
CH : forall P Q Q1, {step Q a (par Q Q1)} -> sim (mu (x1\out a x1)) Q +
H1 : {step Q a (par Q Q1)}
H4 : {step (par Q Q1) a (par (par Q Q1) Q1)}
============================
exists Q1, {step Q a Q1} /\ sim (mu (x1\out a x1)) Q1 +
sim_mu_par_ext < apply CH to H4.
1 subgoal(s).
Variables: P, Q, Q1, A, P1
CH : forall P Q Q1, {step Q a (par Q Q1)} -> sim (mu (x1\out a x1)) Q +
H1 : {step Q a (par Q Q1)}
H4 : {step (par Q Q1) a (par (par Q Q1) Q1)}
H5 : sim (mu (x1\out a x1)) (par Q Q1) +
============================
exists Q1, {step Q a Q1} /\ sim (mu (x1\out a x1)) Q1 +
sim_mu_par_ext < search.
Proof completed.
Abella < Theorem sim_mu_par :
sim (mu (x1\out a x1)) (mu (x1\par (out a x1) (out a x1))).
1 subgoal(s).
============================
sim (mu (x1\out a x1)) (mu (x1\par (out a x1) (out a x1)))
sim_mu_par < apply sim_mu_par_ext to _ with Q = mu (x1\par (out a x1) (out a x1)).
1 subgoal(s).
H1 : sim (mu (x1\out a x1)) (mu (x1\par (out a x1) (out a x1)))
============================
sim (mu (x1\out a x1)) (mu (x1\par (out a x1) (out a x1)))
sim_mu_par < search.
Proof completed.
Abella < Theorem sim_refl :
forall P, sim P P.
1 subgoal(s).
============================
forall P, sim P P
sim_refl < coinduction.
1 subgoal(s).
CH : forall P, sim P P +
============================
forall P, sim P P @
sim_refl < intros.
1 subgoal(s).
Variables: P
CH : forall P, sim P P +
============================
sim P P @
sim_refl < unfold.
1 subgoal(s).
Variables: P
CH : forall P, sim P P +
============================
forall A P1, {step P A P1} -> (exists Q1, {step P A Q1} /\ sim P1 Q1 +)
sim_refl < intros.
1 subgoal(s).
Variables: P, A, P1
CH : forall P, sim P P +
H1 : {step P A P1}
============================
exists Q1, {step P A Q1} /\ sim P1 Q1 +
sim_refl < apply CH with P = P1.
1 subgoal(s).
Variables: P, A, P1
CH : forall P, sim P P +
H1 : {step P A P1}
H2 : sim P1 P1 +
============================
exists Q1, {step P A Q1} /\ sim P1 Q1 +
sim_refl < search.
Proof completed.
Abella < Theorem sim_trans :
forall P Q R, sim P Q -> sim Q R -> sim P R.
1 subgoal(s).
============================
forall P Q R, sim P Q -> sim Q R -> sim P R
sim_trans < coinduction.
1 subgoal(s).
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
============================
forall P Q R, sim P Q -> sim Q R -> sim P R @
sim_trans < intros.
1 subgoal(s).
Variables: P, Q, R
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H1 : sim P Q
H2 : sim Q R
============================
sim P R @
sim_trans < unfold.
1 subgoal(s).
Variables: P, Q, R
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H1 : sim P Q
H2 : sim Q R
============================
forall A P1, {step P A P1} -> (exists Q1, {step R A Q1} /\ sim P1 Q1 +)
sim_trans < intros.
1 subgoal(s).
Variables: P, Q, R, A, P1
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H1 : sim P Q
H2 : sim Q R
H3 : {step P A P1}
============================
exists Q1, {step R A Q1} /\ sim P1 Q1 +
sim_trans < case H1.
1 subgoal(s).
Variables: P, Q, R, A, P1
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H2 : sim Q R
H3 : {step P A P1}
H4 : forall A P1, {step P A P1} -> (exists Q2, {step Q A Q2} /\ sim P1 Q2)
============================
exists Q1, {step R A Q1} /\ sim P1 Q1 +
sim_trans < apply H4 to H3.
1 subgoal(s).
Variables: P, Q, R, A, P1, Q2
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H2 : sim Q R
H3 : {step P A P1}
H4 : forall A P1, {step P A P1} -> (exists Q2, {step Q A Q2} /\ sim P1 Q2)
H5 : {step Q A Q2}
H6 : sim P1 Q2
============================
exists Q1, {step R A Q1} /\ sim P1 Q1 +
sim_trans < case H2.
1 subgoal(s).
Variables: P, Q, R, A, P1, Q2
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H3 : {step P A P1}
H4 : forall A P1, {step P A P1} -> (exists Q2, {step Q A Q2} /\ sim P1 Q2)
H5 : {step Q A Q2}
H6 : sim P1 Q2
H7 : forall A P1, {step Q A P1} -> (exists Q2, {step R A Q2} /\ sim P1 Q2)
============================
exists Q1, {step R A Q1} /\ sim P1 Q1 +
sim_trans < apply H7 to H5.
1 subgoal(s).
Variables: P, Q, R, A, P1, Q2, Q1
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H3 : {step P A P1}
H4 : forall A P1, {step P A P1} -> (exists Q2, {step Q A Q2} /\ sim P1 Q2)
H5 : {step Q A Q2}
H6 : sim P1 Q2
H7 : forall A P1, {step Q A P1} -> (exists Q2, {step R A Q2} /\ sim P1 Q2)
H8 : {step R A Q1}
H9 : sim Q2 Q1
============================
exists Q1, {step R A Q1} /\ sim P1 Q1 +
sim_trans < apply CH to H6 H9.
1 subgoal(s).
Variables: P, Q, R, A, P1, Q2, Q1
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H3 : {step P A P1}
H4 : forall A P1, {step P A P1} -> (exists Q2, {step Q A Q2} /\ sim P1 Q2)
H5 : {step Q A Q2}
H6 : sim P1 Q2
H7 : forall A P1, {step Q A P1} -> (exists Q2, {step R A Q2} /\ sim P1 Q2)
H8 : {step R A Q1}
H9 : sim Q2 Q1
H10 : sim P1 Q1 +
============================
exists Q1, {step R A Q1} /\ sim P1 Q1 +
sim_trans < search.
Proof completed.
Abella < CoDefine bisim P Q := (forall A P1, {step P A P1} -> (exists Q1, {step Q A Q1} /\ bisim P1 Q1)) /\
(forall A Q1, {step Q A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1)).
Abella < Theorem bisim_refl :
forall P, bisim P P.
1 subgoal(s).
============================
forall P, bisim P P
bisim_refl < coinduction.
1 subgoal(s).
CH : forall P, bisim P P +
============================
forall P, bisim P P @
bisim_refl < intros.
1 subgoal(s).
Variables: P
CH : forall P, bisim P P +
============================
bisim P P @
bisim_refl < unfold.
2 subgoal(s).
Variables: P
CH : forall P, bisim P P +
============================
forall A P1, {step P A P1} -> (exists Q1, {step P A Q1} /\ bisim P1 Q1 +)
subgoal 2 is:
forall A Q1, {step P A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)
bisim_refl < intros.
2 subgoal(s).
Variables: P, A, P1
CH : forall P, bisim P P +
H1 : {step P A P1}
============================
exists Q1, {step P A Q1} /\ bisim P1 Q1 +
subgoal 2 is:
forall A Q1, {step P A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)
bisim_refl < apply CH with P = P1.
2 subgoal(s).
Variables: P, A, P1
CH : forall P, bisim P P +
H1 : {step P A P1}
H2 : bisim P1 P1 +
============================
exists Q1, {step P A Q1} /\ bisim P1 Q1 +
subgoal 2 is:
forall A Q1, {step P A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)
bisim_refl < search.
1 subgoal(s).
Variables: P
CH : forall P, bisim P P +
============================
forall A Q1, {step P A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)
bisim_refl < intros.
1 subgoal(s).
Variables: P, A, Q1
CH : forall P, bisim P P +
H1 : {step P A Q1}
============================
exists P1, {step P A P1} /\ bisim P1 Q1 +
bisim_refl < apply CH with P = Q1.
1 subgoal(s).
Variables: P, A, Q1
CH : forall P, bisim P P +
H1 : {step P A Q1}
H2 : bisim Q1 Q1 +
============================
exists P1, {step P A P1} /\ bisim P1 Q1 +
bisim_refl < search.
Proof completed.
Abella < Theorem bisim_sym :
forall P Q, bisim P Q -> bisim Q P.
1 subgoal(s).
============================
forall P Q, bisim P Q -> bisim Q P
bisim_sym < coinduction.
1 subgoal(s).
CH : forall P Q, bisim P Q -> bisim Q P +
============================
forall P Q, bisim P Q -> bisim Q P @
bisim_sym < intros.
1 subgoal(s).
Variables: P, Q
CH : forall P Q, bisim P Q -> bisim Q P +
H1 : bisim P Q
============================
bisim Q P @
bisim_sym < case H1.
1 subgoal(s).
Variables: P, Q
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
============================
bisim Q P @
bisim_sym < unfold.
2 subgoal(s).
Variables: P, Q
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
============================
forall A P1, {step Q A P1} -> (exists Q1, {step P A Q1} /\ bisim P1 Q1 +)
subgoal 2 is:
forall A Q1, {step P A Q1} -> (exists P1, {step Q A P1} /\ bisim P1 Q1 +)
bisim_sym < intros.
2 subgoal(s).
Variables: P, Q, A, P1
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H4 : {step Q A P1}
============================
exists Q1, {step P A Q1} /\ bisim P1 Q1 +
subgoal 2 is:
forall A Q1, {step P A Q1} -> (exists P1, {step Q A P1} /\ bisim P1 Q1 +)
bisim_sym < apply H3 to H4.
2 subgoal(s).
Variables: P, Q, A, P1, P2
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H4 : {step Q A P1}
H5 : {step P A P2}
H6 : bisim P2 P1
============================
exists Q1, {step P A Q1} /\ bisim P1 Q1 +
subgoal 2 is:
forall A Q1, {step P A Q1} -> (exists P1, {step Q A P1} /\ bisim P1 Q1 +)
bisim_sym < apply CH to H6.
2 subgoal(s).
Variables: P, Q, A, P1, P2
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H4 : {step Q A P1}
H5 : {step P A P2}
H6 : bisim P2 P1
H7 : bisim P1 P2 +
============================
exists Q1, {step P A Q1} /\ bisim P1 Q1 +
subgoal 2 is:
forall A Q1, {step P A Q1} -> (exists P1, {step Q A P1} /\ bisim P1 Q1 +)
bisim_sym < search.
1 subgoal(s).
Variables: P, Q
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
============================
forall A Q1, {step P A Q1} -> (exists P1, {step Q A P1} /\ bisim P1 Q1 +)
bisim_sym < intros.
1 subgoal(s).
Variables: P, Q, A, Q1
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H4 : {step P A Q1}
============================
exists P1, {step Q A P1} /\ bisim P1 Q1 +
bisim_sym < apply H2 to H4.
1 subgoal(s).
Variables: P, Q, A, Q1, Q2
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H4 : {step P A Q1}
H5 : {step Q A Q2}
H6 : bisim Q1 Q2
============================
exists P1, {step Q A P1} /\ bisim P1 Q1 +
bisim_sym < apply CH to H6.
1 subgoal(s).
Variables: P, Q, A, Q1, Q2
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H4 : {step P A Q1}
H5 : {step Q A Q2}
H6 : bisim Q1 Q2
H7 : bisim Q2 Q1 +
============================
exists P1, {step Q A P1} /\ bisim P1 Q1 +
bisim_sym < search.
Proof completed.
Abella < Theorem bisim_trans :
forall P Q R, bisim P Q -> bisim Q R -> bisim P R.
1 subgoal(s).
============================
forall P Q R, bisim P Q -> bisim Q R -> bisim P R
bisim_trans < coinduction.
1 subgoal(s).
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
============================
forall P Q R, bisim P Q -> bisim Q R -> bisim P R @
bisim_trans < intros.
1 subgoal(s).
Variables: P, Q, R
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H1 : bisim P Q
H2 : bisim Q R
============================
bisim P R @
bisim_trans < case H1.
1 subgoal(s).
Variables: P, Q, R
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H2 : bisim Q R
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
============================
bisim P R @
bisim_trans < case H2.
1 subgoal(s).
Variables: P, Q, R
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\
bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\
bisim P2 Q2)
============================
bisim P R @
bisim_trans < unfold.
2 subgoal(s).
Variables: P, Q, R
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\
bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\
bisim P2 Q2)
============================
forall A P1, {step P A P1} -> (exists Q1, {step R A Q1} /\ bisim P1 Q1 +)
subgoal 2 is:
forall A Q1, {step R A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)
bisim_trans < intros.
2 subgoal(s).
Variables: P, Q, R, A, P1
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\
bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\
bisim P2 Q2)
H7 : {step P A P1}
============================
exists Q1, {step R A Q1} /\ bisim P1 Q1 +
subgoal 2 is:
forall A Q1, {step R A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)
bisim_trans < apply H3 to H7.
2 subgoal(s).
Variables: P, Q, R, A, P1, Q2
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\
bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\
bisim P2 Q2)
H7 : {step P A P1}
H8 : {step Q A Q2}
H9 : bisim P1 Q2
============================
exists Q1, {step R A Q1} /\ bisim P1 Q1 +
subgoal 2 is:
forall A Q1, {step R A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)
bisim_trans < apply H5 to H8.
2 subgoal(s).
Variables: P, Q, R, A, P1, Q2, Q1
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\
bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\
bisim P2 Q2)
H7 : {step P A P1}
H8 : {step Q A Q2}
H9 : bisim P1 Q2
H10 : {step R A Q1}
H11 : bisim Q2 Q1
============================
exists Q1, {step R A Q1} /\ bisim P1 Q1 +
subgoal 2 is:
forall A Q1, {step R A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)
bisim_trans < apply CH to H9 H11.
2 subgoal(s).
Variables: P, Q, R, A, P1, Q2, Q1
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\
bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\
bisim P2 Q2)
H7 : {step P A P1}
H8 : {step Q A Q2}
H9 : bisim P1 Q2
H10 : {step R A Q1}
H11 : bisim Q2 Q1
H12 : bisim P1 Q1 +
============================
exists Q1, {step R A Q1} /\ bisim P1 Q1 +
subgoal 2 is:
forall A Q1, {step R A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)
bisim_trans < search.
1 subgoal(s).
Variables: P, Q, R
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\
bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\
bisim P2 Q2)
============================
forall A Q1, {step R A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)
bisim_trans < intros.
1 subgoal(s).
Variables: P, Q, R, A, Q1
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\
bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\
bisim P2 Q2)
H7 : {step R A Q1}
============================
exists P1, {step P A P1} /\ bisim P1 Q1 +
bisim_trans < apply H6 to H7.
1 subgoal(s).
Variables: P, Q, R, A, Q1, P2
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\
bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\
bisim P2 Q2)
H7 : {step R A Q1}
H8 : {step Q A P2}
H9 : bisim P2 Q1
============================
exists P1, {step P A P1} /\ bisim P1 Q1 +
bisim_trans < apply H4 to H8.
1 subgoal(s).
Variables: P, Q, R, A, Q1, P2, P1
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\
bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\
bisim P2 Q2)
H7 : {step R A Q1}
H8 : {step Q A P2}
H9 : bisim P2 Q1
H10 : {step P A P1}
H11 : bisim P1 P2
============================
exists P1, {step P A P1} /\ bisim P1 Q1 +
bisim_trans < apply CH to H11 H9.
1 subgoal(s).
Variables: P, Q, R, A, Q1, P2, P1
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\
bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\
bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\
bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\
bisim P2 Q2)
H7 : {step R A Q1}
H8 : {step Q A P2}
H9 : bisim P2 Q1
H10 : {step P A P1}
H11 : bisim P1 P2
H12 : bisim P1 Q1 +
============================
exists P1, {step P A P1} /\ bisim P1 Q1 +
bisim_trans < search.
Proof completed.
Abella < Goodbye.
