finite-pic.thm [Abella trace]

%% Simulation and bisimulation for the pi-calculus %% %% Given that the meta-logic of Abella is intuitionistic, the %% specification of bisimulation here corresponds to open bisimulation. %% %% Here we prove here that simulation is preorder and bisimulation is an %% equivalence relation.

Specification "finite-pic".

% Simulation defined

CoDefine sim : proc -> proc -> prop by sim P Q := (forall A P1, {one P A P1} -> exists Q1, {one Q A Q1} /\ sim P1 Q1) /\ (forall X M, {oneb P (dn X) M} -> exists N, {oneb Q (dn X) N} /\ forall W, sim (M W) (N W)) /\ (forall X M, {oneb P (up X) M} -> exists N, {oneb Q (up X) N} /\ nabla w, sim (M w) (N w)).

% Simulation is a preorder

Theorem sim_refl : forall P, sim P P.

coinduction.

intros.

unfold.

intros.

apply CH with P = P1.

search.

intros.

exists M.

split.

search.

intros.

apply CH with P = M W.

search.

intros.

exists M.

split.

search.

intros.

apply CH with P = M n1.

search.

Theorem sim_trans : forall P Q R, sim P Q -> sim Q R -> sim P R.

coinduction.

intros.

case H1.

case H2.

unfold.

intros.

apply H3 to H9.

apply H6 to H10.

apply CH to H11 H13.

search.

intros.

apply H4 to H9.

apply H7 to H10.

exists N1.

split.

search.

intros.

apply H11 with W = W.

apply H13 with W = W.

apply CH to H14 H15.

search.

intros.

apply H5 to H9.

apply H8 to H10.

apply CH to H11 H13.

search.

% Bisimulation defined

CoDefine bisim : proc -> proc -> prop by bisim P Q := (forall A P1, {one P A P1} -> exists Q1, {one Q A Q1} /\ bisim P1 Q1) /\ (forall X M, {oneb P (dn X) M} -> exists N, {oneb Q (dn X) N} /\ forall W, bisim (M W) (N W)) /\ (forall X M, {oneb P (up X) M} -> exists N, {oneb Q (up X) N} /\ nabla w, bisim (M w) (N w)) /\ (forall A Q1, {one Q A Q1} -> exists P1, {one P A P1} /\ bisim Q1 P1) /\ (forall X N, {oneb Q (dn X) N} -> exists M, {oneb P (dn X) M} /\ forall W, bisim (N W) (M W)) /\ (forall X N, {oneb Q (up X) N} -> exists M, {oneb P (up X) M} /\ nabla w, bisim (N w) (M w)).

% Bisimulation is an equivalence

Theorem bisim_refl : forall P, bisim P P.

coinduction.

intros.

unfold.

intros.

apply CH with P = P1.

search.

intros.

exists M.

split.

search.

intros.

apply CH with P = M W.

search.

intros.

exists M.

split.

search.

intros.

apply CH with P = M n1.

search.

intros.

apply CH with P = Q1.

search.

intros.

exists N.

split.

search.

intros.

apply CH with P = N W.

search.

intros.

exists N.

split.

search.

intros.

apply CH with P = N n1.

search.

Theorem bisim_sym : forall P Q, bisim P Q -> bisim Q P.

intros.

case H1.

unfold.

intros.

apply H5 to H8.

search.

intros.

apply H6 to H8.

search.

intros.

apply H7 to H8.

search.

intros.

apply H2 to H8.

search.

intros.

apply H3 to H8.

search.

intros.

apply H4 to H8.

search.

Theorem bisim_trans : forall P Q R, bisim P Q -> bisim Q R -> bisim P R.

coinduction.

intros.

case H1.

case H2.

unfold.

intros.

apply H3 to H15.

apply H9 to H16.

apply CH to H17 H19.

search.

intros.

apply H4 to H15.

apply H10 to H16.

exists N1.

split.

search.

intros.

apply H17 with W = W.

apply H19 with W = W.

apply CH to H20 H21.

search.

intros.

apply H5 to H15.

apply H11 to H16.

apply CH to H17 H19.

search.

intros.

apply H12 to H15.

apply H6 to H16.

apply CH to H17 H19.

search.

intros.

apply H13 to H15.

apply H7 to H16.

exists M1.

split.

search.

intros.

apply H17 with W = W.

apply H19 with W = W.

apply CH to H20 H21.

search.

intros.

apply H14 to H15.

apply H8 to H16.

apply CH to H17 H19.

search.

forall P, sim P P

sim_refl < coinduction.

CH: forall P, sim P P +

forall P, sim P P #

CH: forall P, sim P P +

forall P, sim P P #

sim_refl < intros.

Variables: P

CH: forall P, sim P P +

sim P P #

Variables: P

CH: forall P, sim P P +

sim P P #

sim_refl < unfold.

Subgoal 1

Variables: P

CH: forall P, sim P P +

forall A P1, {one P A P1} -> (exists Q1, {one P A Q1} /\ sim P1 Q1 +)

(+ 2 more subgoals)

Subgoal 1

Variables: P

CH: forall P, sim P P +

forall A P1, {one P A P1} -> (exists Q1, {one P A Q1} /\ sim P1 Q1 +)

(+ 2 more subgoals)

sim_refl < intros.

Subgoal 1

Variables: P A P1

CH: forall P, sim P P +

H1: {one P A P1}

exists Q1, {one P A Q1} /\ sim P1 Q1 +

(+ 2 more subgoals)

Subgoal 1

Variables: P A P1

CH: forall P, sim P P +

H1: {one P A P1}

exists Q1, {one P A Q1} /\ sim P1 Q1 +

(+ 2 more subgoals)

sim_refl < apply CH with P = P1.

Subgoal 1

Variables: P A P1

CH: forall P, sim P P +

H1: {one P A P1}

H2: sim P1 P1 +

exists Q1, {one P A Q1} /\ sim P1 Q1 +

(+ 2 more subgoals)

Subgoal 1

Variables: P A P1

CH: forall P, sim P P +

H1: {one P A P1}

H2: sim P1 P1 +

exists Q1, {one P A Q1} /\ sim P1 Q1 +

(+ 2 more subgoals)

sim_refl < search.

Subgoal 2

Variables: P

CH: forall P, sim P P +

forall X M, {oneb P (dn X) M} -> (exists N, {oneb P (dn X) N} /\ (forall W, sim (M W) (N W) +))

(+ 1 more subgoal)

Subgoal 2

Variables: P

CH: forall P, sim P P +

forall X M, {oneb P (dn X) M} -> (exists N, {oneb P (dn X) N} /\ (forall W, sim (M W) (N W) +))

(+ 1 more subgoal)

sim_refl < intros.

Subgoal 2

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (dn X) M}

exists N, {oneb P (dn X) N} /\ (forall W, sim (M W) (N W) +)

(+ 1 more subgoal)

Subgoal 2

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (dn X) M}

exists N, {oneb P (dn X) N} /\ (forall W, sim (M W) (N W) +)

(+ 1 more subgoal)

sim_refl < exists M.

Subgoal 2

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (dn X) M}

{oneb P (dn X) M} /\ (forall W, sim (M W) (M W) +)

(+ 1 more subgoal)

Subgoal 2

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (dn X) M}

{oneb P (dn X) M} /\ (forall W, sim (M W) (M W) +)

(+ 1 more subgoal)

sim_refl < split.

Subgoal 2.1

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (dn X) M}

{oneb P (dn X) M}

(+ 2 more subgoals)

Subgoal 2.1

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (dn X) M}

{oneb P (dn X) M}

(+ 2 more subgoals)

sim_refl < search.

Subgoal 2.2

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (dn X) M}

forall W, sim (M W) (M W) +

(+ 1 more subgoal)

Subgoal 2.2

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (dn X) M}

forall W, sim (M W) (M W) +

(+ 1 more subgoal)

sim_refl < intros.

Subgoal 2.2

Variables: P X M W

CH: forall P, sim P P +

H1: {oneb P (dn X) M}

sim (M W) (M W) +

(+ 1 more subgoal)

Subgoal 2.2

Variables: P X M W

CH: forall P, sim P P +

H1: {oneb P (dn X) M}

sim (M W) (M W) +

(+ 1 more subgoal)

sim_refl < apply CH with P = M W.

Subgoal 2.2

Variables: P X M W

CH: forall P, sim P P +

H1: {oneb P (dn X) M}

H2: sim (M W) (M W) +

sim (M W) (M W) +

(+ 1 more subgoal)

Subgoal 2.2

Variables: P X M W

CH: forall P, sim P P +

H1: {oneb P (dn X) M}

H2: sim (M W) (M W) +

sim (M W) (M W) +

(+ 1 more subgoal)

sim_refl < search.

Subgoal 3

Variables: P

CH: forall P, sim P P +

forall X M, {oneb P (up X) M} -> (exists N, {oneb P (up X) N} /\ (nabla w, sim (M w) (N w) +))

Subgoal 3

Variables: P

CH: forall P, sim P P +

forall X M, {oneb P (up X) M} -> (exists N, {oneb P (up X) N} /\ (nabla w, sim (M w) (N w) +))

sim_refl < intros.

Subgoal 3

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (up X) M}

exists N, {oneb P (up X) N} /\ (nabla w, sim (M w) (N w) +)

Subgoal 3

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (up X) M}

exists N, {oneb P (up X) N} /\ (nabla w, sim (M w) (N w) +)

sim_refl < exists M.

Subgoal 3

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (up X) M}

{oneb P (up X) M} /\ (nabla w, sim (M w) (M w) +)

Subgoal 3

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (up X) M}

{oneb P (up X) M} /\ (nabla w, sim (M w) (M w) +)

sim_refl < split.

Subgoal 3.1

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (up X) M}

{oneb P (up X) M}

(+ 1 more subgoal)

Subgoal 3.1

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (up X) M}

{oneb P (up X) M}

(+ 1 more subgoal)

sim_refl < search.

Subgoal 3.2

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (up X) M}

nabla w, sim (M w) (M w) +

Subgoal 3.2

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (up X) M}

nabla w, sim (M w) (M w) +

sim_refl < intros.

Subgoal 3.2

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (up X) M}

sim (M n1) (M n1) +

Subgoal 3.2

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (up X) M}

sim (M n1) (M n1) +

sim_refl < apply CH with P = M n1.

Subgoal 3.2

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (up X) M}

H2: sim (M n1) (M n1) +

sim (M n1) (M n1) +

Subgoal 3.2

Variables: P X M

CH: forall P, sim P P +

H1: {oneb P (up X) M}

H2: sim (M n1) (M n1) +

sim (M n1) (M n1) +

sim_refl < search.

Proof completed

forall P Q R, sim P Q -> sim Q R -> sim P R

sim_trans < coinduction.

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 #

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.

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 #

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 < case H1.

Variables: P Q R

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H2: sim Q R

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

sim P R #

Variables: P Q R

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H2: sim Q R

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

sim P R #

sim_trans < case H2.

Variables: P Q R

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

sim P R #

Variables: P Q R

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

sim P R #

sim_trans < unfold.

Subgoal 1

Variables: P Q R

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

forall A P1, {one P A P1} -> (exists Q1, {one R A Q1} /\ sim P1 Q1 +)

(+ 2 more subgoals)

Subgoal 1

Variables: P Q R

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

forall A P1, {one P A P1} -> (exists Q1, {one R A Q1} /\ sim P1 Q1 +)

(+ 2 more subgoals)

sim_trans < intros.

Subgoal 1

Variables: P Q R A P1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {one P A P1}

exists Q1, {one R A Q1} /\ sim P1 Q1 +

(+ 2 more subgoals)

Subgoal 1

Variables: P Q R A P1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {one P A P1}

exists Q1, {one R A Q1} /\ sim P1 Q1 +

(+ 2 more subgoals)

sim_trans < apply H3 to H9.

Subgoal 1

Variables: P Q R A P1 Q2

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {one P A P1}

H10: {one Q A Q2}

H11: sim P1 Q2

exists Q1, {one R A Q1} /\ sim P1 Q1 +

(+ 2 more subgoals)

Subgoal 1

Variables: P Q R A P1 Q2

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {one P A P1}

H10: {one Q A Q2}

H11: sim P1 Q2

exists Q1, {one R A Q1} /\ sim P1 Q1 +

(+ 2 more subgoals)

sim_trans < apply H6 to H10.

Subgoal 1

Variables: P Q R A P1 Q2 Q1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {one P A P1}

H10: {one Q A Q2}

H11: sim P1 Q2

H12: {one R A Q1}

H13: sim Q2 Q1

exists Q1, {one R A Q1} /\ sim P1 Q1 +

(+ 2 more subgoals)

Subgoal 1

Variables: P Q R A P1 Q2 Q1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {one P A P1}

H10: {one Q A Q2}

H11: sim P1 Q2

H12: {one R A Q1}

H13: sim Q2 Q1

exists Q1, {one R A Q1} /\ sim P1 Q1 +

(+ 2 more subgoals)

sim_trans < apply CH to H11 H13.

Subgoal 1

Variables: P Q R A P1 Q2 Q1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {one P A P1}

H10: {one Q A Q2}

H11: sim P1 Q2

H12: {one R A Q1}

H13: sim Q2 Q1

H14: sim P1 Q1 +

exists Q1, {one R A Q1} /\ sim P1 Q1 +

(+ 2 more subgoals)

Subgoal 1

Variables: P Q R A P1 Q2 Q1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {one P A P1}

H10: {one Q A Q2}

H11: sim P1 Q2

H12: {one R A Q1}

H13: sim Q2 Q1

H14: sim P1 Q1 +

exists Q1, {one R A Q1} /\ sim P1 Q1 +

(+ 2 more subgoals)

sim_trans < search.

Subgoal 2

Variables: P Q R

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

forall X M, {oneb P (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W) +))

(+ 1 more subgoal)

Subgoal 2

Variables: P Q R

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

forall X M, {oneb P (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W) +))

(+ 1 more subgoal)

sim_trans < intros.

Subgoal 2

Variables: P Q R X M

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W) +)

(+ 1 more subgoal)

Subgoal 2

Variables: P Q R X M

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W) +)

(+ 1 more subgoal)

sim_trans < apply H4 to H9.

Subgoal 2

Variables: P Q R X M N

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W) +)

(+ 1 more subgoal)

Subgoal 2

Variables: P Q R X M N

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W) +)

(+ 1 more subgoal)

sim_trans < apply H7 to H10.

Subgoal 2

Variables: P Q R X M N N1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W) +)

(+ 1 more subgoal)

Subgoal 2

Variables: P Q R X M N N1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W) +)

(+ 1 more subgoal)

sim_trans < exists N1.

Subgoal 2

Variables: P Q R X M N N1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

{oneb R (dn X) N1} /\ (forall W, sim (M W) (N1 W) +)

(+ 1 more subgoal)

Subgoal 2

Variables: P Q R X M N N1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

{oneb R (dn X) N1} /\ (forall W, sim (M W) (N1 W) +)

(+ 1 more subgoal)

sim_trans < split.

Subgoal 2.1

Variables: P Q R X M N N1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

{oneb R (dn X) N1}

(+ 2 more subgoals)

Subgoal 2.1

Variables: P Q R X M N N1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

{oneb R (dn X) N1}

(+ 2 more subgoals)

sim_trans < search.

Subgoal 2.2

Variables: P Q R X M N N1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

forall W, sim (M W) (N1 W) +

(+ 1 more subgoal)

Subgoal 2.2

Variables: P Q R X M N N1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

forall W, sim (M W) (N1 W) +

(+ 1 more subgoal)

sim_trans < intros.

Subgoal 2.2

Variables: P Q R X M N N1 W

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

sim (M W) (N1 W) +

(+ 1 more subgoal)

Subgoal 2.2

Variables: P Q R X M N N1 W

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

sim (M W) (N1 W) +

(+ 1 more subgoal)

sim_trans < apply H11 with W = W.

Subgoal 2.2

Variables: P Q R X M N N1 W

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

H14: sim (M W) (N W)

sim (M W) (N1 W) +

(+ 1 more subgoal)

Subgoal 2.2

Variables: P Q R X M N N1 W

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

H14: sim (M W) (N W)

sim (M W) (N1 W) +

(+ 1 more subgoal)

sim_trans < apply H13 with W = W.

Subgoal 2.2

Variables: P Q R X M N N1 W

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

H14: sim (M W) (N W)

H15: sim (N W) (N1 W)

sim (M W) (N1 W) +

(+ 1 more subgoal)

Subgoal 2.2

Variables: P Q R X M N N1 W

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

H14: sim (M W) (N W)

H15: sim (N W) (N1 W)

sim (M W) (N1 W) +

(+ 1 more subgoal)

sim_trans < apply CH to H14 H15.

Subgoal 2.2

Variables: P Q R X M N N1 W

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

H14: sim (M W) (N W)

H15: sim (N W) (N1 W)

H16: sim (M W) (N1 W) +

sim (M W) (N1 W) +

(+ 1 more subgoal)

Subgoal 2.2

Variables: P Q R X M N N1 W

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (dn X) M}

H10: {oneb Q (dn X) N}

H11: forall W, sim (M W) (N W)

H12: {oneb R (dn X) N1}

H13: forall W, sim (N W) (N1 W)

H14: sim (M W) (N W)

H15: sim (N W) (N1 W)

H16: sim (M W) (N1 W) +

sim (M W) (N1 W) +

(+ 1 more subgoal)

sim_trans < search.

Subgoal 3

Variables: P Q R

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

forall X M, {oneb P (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w) +))

Subgoal 3

Variables: P Q R

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

forall X M, {oneb P (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w) +))

sim_trans < intros.

Subgoal 3

Variables: P Q R X M

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (up X) M}

exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w) +)

Subgoal 3

Variables: P Q R X M

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (up X) M}

exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w) +)

sim_trans < apply H5 to H9.

Subgoal 3

Variables: P Q R X M N

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (up X) M}

H10: {oneb Q (up X) N}

H11: sim (M n1) (N n1)

exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w) +)

Subgoal 3

Variables: P Q R X M N

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (up X) M}

H10: {oneb Q (up X) N}

H11: sim (M n1) (N n1)

exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w) +)

sim_trans < apply H8 to H10.

Subgoal 3

Variables: P Q R X M N N1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (up X) M}

H10: {oneb Q (up X) N}

H11: sim (M n1) (N n1)

H12: {oneb R (up X) N1}

H13: sim (N n1) (N1 n1)

exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w) +)

Subgoal 3

Variables: P Q R X M N N1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (up X) M}

H10: {oneb Q (up X) N}

H11: sim (M n1) (N n1)

H12: {oneb R (up X) N1}

H13: sim (N n1) (N1 n1)

exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w) +)

sim_trans < apply CH to H11 H13.

Subgoal 3

Variables: P Q R X M N N1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (up X) M}

H10: {oneb Q (up X) N}

H11: sim (M n1) (N n1)

H12: {oneb R (up X) N1}

H13: sim (N n1) (N1 n1)

H14: sim (M n1) (N1 n1) +

exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w) +)

Subgoal 3

Variables: P Q R X M N N1

CH: forall P Q R, sim P Q -> sim Q R -> sim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ sim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, sim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, sim (M w) (N w)))

H6: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ sim P2 Q2)

H7: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, sim (M W) (N W)))

H8: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w)))

H9: {oneb P (up X) M}

H10: {oneb Q (up X) N}

H11: sim (M n1) (N n1)

H12: {oneb R (up X) N1}

H13: sim (N n1) (N1 n1)

H14: sim (M n1) (N1 n1) +

exists N, {oneb R (up X) N} /\ (nabla w, sim (M w) (N w) +)

sim_trans < search.

Proof completed

forall P, bisim P P

bisim_refl < coinduction.

CH: forall P, bisim P P +

forall P, bisim P P #

CH: forall P, bisim P P +

forall P, bisim P P #

bisim_refl < intros.

Variables: P

CH: forall P, bisim P P +

bisim P P #

Variables: P

CH: forall P, bisim P P +

bisim P P #

bisim_refl < unfold.

Subgoal 1

Variables: P

CH: forall P, bisim P P +

forall A P1, {one P A P1} -> (exists Q1, {one P A Q1} /\ bisim P1 Q1 +)

(+ 5 more subgoals)

Subgoal 1

Variables: P

CH: forall P, bisim P P +

forall A P1, {one P A P1} -> (exists Q1, {one P A Q1} /\ bisim P1 Q1 +)

(+ 5 more subgoals)

bisim_refl < intros.

Subgoal 1

Variables: P A P1

CH: forall P, bisim P P +

H1: {one P A P1}

exists Q1, {one P A Q1} /\ bisim P1 Q1 +

(+ 5 more subgoals)

Subgoal 1

Variables: P A P1

CH: forall P, bisim P P +

H1: {one P A P1}

exists Q1, {one P A Q1} /\ bisim P1 Q1 +

(+ 5 more subgoals)

bisim_refl < apply CH with P = P1.

Subgoal 1

Variables: P A P1

CH: forall P, bisim P P +

H1: {one P A P1}

H2: bisim P1 P1 +

exists Q1, {one P A Q1} /\ bisim P1 Q1 +

(+ 5 more subgoals)

Subgoal 1

Variables: P A P1

CH: forall P, bisim P P +

H1: {one P A P1}

H2: bisim P1 P1 +

exists Q1, {one P A Q1} /\ bisim P1 Q1 +

(+ 5 more subgoals)

bisim_refl < search.

Subgoal 2

Variables: P

CH: forall P, bisim P P +

forall X M, {oneb P (dn X) M} -> (exists N, {oneb P (dn X) N} /\ (forall W, bisim (M W) (N W) +))

(+ 4 more subgoals)

Subgoal 2

Variables: P

CH: forall P, bisim P P +

forall X M, {oneb P (dn X) M} -> (exists N, {oneb P (dn X) N} /\ (forall W, bisim (M W) (N W) +))

(+ 4 more subgoals)

bisim_refl < intros.

Subgoal 2

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (dn X) M}

exists N, {oneb P (dn X) N} /\ (forall W, bisim (M W) (N W) +)

(+ 4 more subgoals)

Subgoal 2

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (dn X) M}

exists N, {oneb P (dn X) N} /\ (forall W, bisim (M W) (N W) +)

(+ 4 more subgoals)

bisim_refl < exists M.

Subgoal 2

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (dn X) M}

{oneb P (dn X) M} /\ (forall W, bisim (M W) (M W) +)

(+ 4 more subgoals)

Subgoal 2

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (dn X) M}

{oneb P (dn X) M} /\ (forall W, bisim (M W) (M W) +)

(+ 4 more subgoals)

bisim_refl < split.

Subgoal 2.1

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (dn X) M}

{oneb P (dn X) M}

(+ 5 more subgoals)

Subgoal 2.1

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (dn X) M}

{oneb P (dn X) M}

(+ 5 more subgoals)

bisim_refl < search.

Subgoal 2.2

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (dn X) M}

forall W, bisim (M W) (M W) +

(+ 4 more subgoals)

Subgoal 2.2

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (dn X) M}

forall W, bisim (M W) (M W) +

(+ 4 more subgoals)

bisim_refl < intros.

Subgoal 2.2

Variables: P X M W

CH: forall P, bisim P P +

H1: {oneb P (dn X) M}

bisim (M W) (M W) +

(+ 4 more subgoals)

Subgoal 2.2

Variables: P X M W

CH: forall P, bisim P P +

H1: {oneb P (dn X) M}

bisim (M W) (M W) +

(+ 4 more subgoals)

bisim_refl < apply CH with P = M W.

Subgoal 2.2

Variables: P X M W

CH: forall P, bisim P P +

H1: {oneb P (dn X) M}

H2: bisim (M W) (M W) +

bisim (M W) (M W) +

(+ 4 more subgoals)

Subgoal 2.2

Variables: P X M W

CH: forall P, bisim P P +

H1: {oneb P (dn X) M}

H2: bisim (M W) (M W) +

bisim (M W) (M W) +

(+ 4 more subgoals)

bisim_refl < search.

Subgoal 3

Variables: P

CH: forall P, bisim P P +

forall X M, {oneb P (up X) M} -> (exists N, {oneb P (up X) N} /\ (nabla w, bisim (M w) (N w) +))

(+ 3 more subgoals)

Subgoal 3

Variables: P

CH: forall P, bisim P P +

forall X M, {oneb P (up X) M} -> (exists N, {oneb P (up X) N} /\ (nabla w, bisim (M w) (N w) +))

(+ 3 more subgoals)

bisim_refl < intros.

Subgoal 3

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (up X) M}

exists N, {oneb P (up X) N} /\ (nabla w, bisim (M w) (N w) +)

(+ 3 more subgoals)

Subgoal 3

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (up X) M}

exists N, {oneb P (up X) N} /\ (nabla w, bisim (M w) (N w) +)

(+ 3 more subgoals)

bisim_refl < exists M.

Subgoal 3

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (up X) M}

{oneb P (up X) M} /\ (nabla w, bisim (M w) (M w) +)

(+ 3 more subgoals)

Subgoal 3

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (up X) M}

{oneb P (up X) M} /\ (nabla w, bisim (M w) (M w) +)

(+ 3 more subgoals)

bisim_refl < split.

Subgoal 3.1

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (up X) M}

{oneb P (up X) M}

(+ 4 more subgoals)

Subgoal 3.1

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (up X) M}

{oneb P (up X) M}

(+ 4 more subgoals)

bisim_refl < search.

Subgoal 3.2

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (up X) M}

nabla w, bisim (M w) (M w) +

(+ 3 more subgoals)

Subgoal 3.2

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (up X) M}

nabla w, bisim (M w) (M w) +

(+ 3 more subgoals)

bisim_refl < intros.

Subgoal 3.2

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (up X) M}

bisim (M n1) (M n1) +

(+ 3 more subgoals)

Subgoal 3.2

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (up X) M}

bisim (M n1) (M n1) +

(+ 3 more subgoals)

bisim_refl < apply CH with P = M n1.

Subgoal 3.2

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (up X) M}

H2: bisim (M n1) (M n1) +

bisim (M n1) (M n1) +

(+ 3 more subgoals)

Subgoal 3.2

Variables: P X M

CH: forall P, bisim P P +

H1: {oneb P (up X) M}

H2: bisim (M n1) (M n1) +

bisim (M n1) (M n1) +

(+ 3 more subgoals)

bisim_refl < search.

Subgoal 4

Variables: P

CH: forall P, bisim P P +

forall A Q1, {one P A Q1} -> (exists P1, {one P A P1} /\ bisim Q1 P1 +)

(+ 2 more subgoals)

Subgoal 4

Variables: P

CH: forall P, bisim P P +

forall A Q1, {one P A Q1} -> (exists P1, {one P A P1} /\ bisim Q1 P1 +)

(+ 2 more subgoals)

bisim_refl < intros.

Subgoal 4

Variables: P A Q1

CH: forall P, bisim P P +

H1: {one P A Q1}

exists P1, {one P A P1} /\ bisim Q1 P1 +

(+ 2 more subgoals)

Subgoal 4

Variables: P A Q1

CH: forall P, bisim P P +

H1: {one P A Q1}

exists P1, {one P A P1} /\ bisim Q1 P1 +

(+ 2 more subgoals)

bisim_refl < apply CH with P = Q1.

Subgoal 4

Variables: P A Q1

CH: forall P, bisim P P +

H1: {one P A Q1}

H2: bisim Q1 Q1 +

exists P1, {one P A P1} /\ bisim Q1 P1 +

(+ 2 more subgoals)

Subgoal 4

Variables: P A Q1

CH: forall P, bisim P P +

H1: {one P A Q1}

H2: bisim Q1 Q1 +

exists P1, {one P A P1} /\ bisim Q1 P1 +

(+ 2 more subgoals)

bisim_refl < search.

Subgoal 5

Variables: P

CH: forall P, bisim P P +

forall X N, {oneb P (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W) +))

(+ 1 more subgoal)

Subgoal 5

Variables: P

CH: forall P, bisim P P +

forall X N, {oneb P (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W) +))

(+ 1 more subgoal)

bisim_refl < intros.

Subgoal 5

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (dn X) N}

exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W) +)

(+ 1 more subgoal)

Subgoal 5

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (dn X) N}

exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W) +)

(+ 1 more subgoal)

bisim_refl < exists N.

Subgoal 5

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (dn X) N}

{oneb P (dn X) N} /\ (forall W, bisim (N W) (N W) +)

(+ 1 more subgoal)

Subgoal 5

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (dn X) N}

{oneb P (dn X) N} /\ (forall W, bisim (N W) (N W) +)

(+ 1 more subgoal)

bisim_refl < split.

Subgoal 5.1

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (dn X) N}

{oneb P (dn X) N}

(+ 2 more subgoals)

Subgoal 5.1

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (dn X) N}

{oneb P (dn X) N}

(+ 2 more subgoals)

bisim_refl < search.

Subgoal 5.2

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (dn X) N}

forall W, bisim (N W) (N W) +

(+ 1 more subgoal)

Subgoal 5.2

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (dn X) N}

forall W, bisim (N W) (N W) +

(+ 1 more subgoal)

bisim_refl < intros.

Subgoal 5.2

Variables: P X N W

CH: forall P, bisim P P +

H1: {oneb P (dn X) N}

bisim (N W) (N W) +

(+ 1 more subgoal)

Subgoal 5.2

Variables: P X N W

CH: forall P, bisim P P +

H1: {oneb P (dn X) N}

bisim (N W) (N W) +

(+ 1 more subgoal)

bisim_refl < apply CH with P = N W.

Subgoal 5.2

Variables: P X N W

CH: forall P, bisim P P +

H1: {oneb P (dn X) N}

H2: bisim (N W) (N W) +

bisim (N W) (N W) +

(+ 1 more subgoal)

Subgoal 5.2

Variables: P X N W

CH: forall P, bisim P P +

H1: {oneb P (dn X) N}

H2: bisim (N W) (N W) +

bisim (N W) (N W) +

(+ 1 more subgoal)

bisim_refl < search.

Subgoal 6

Variables: P

CH: forall P, bisim P P +

forall X N, {oneb P (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w) +))

Subgoal 6

Variables: P

CH: forall P, bisim P P +

forall X N, {oneb P (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w) +))

bisim_refl < intros.

Subgoal 6

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (up X) N}

exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w) +)

Subgoal 6

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (up X) N}

exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w) +)

bisim_refl < exists N.

Subgoal 6

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (up X) N}

{oneb P (up X) N} /\ (nabla w, bisim (N w) (N w) +)

Subgoal 6

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (up X) N}

{oneb P (up X) N} /\ (nabla w, bisim (N w) (N w) +)

bisim_refl < split.

Subgoal 6.1

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (up X) N}

{oneb P (up X) N}

(+ 1 more subgoal)

Subgoal 6.1

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (up X) N}

{oneb P (up X) N}

(+ 1 more subgoal)

bisim_refl < search.

Subgoal 6.2

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (up X) N}

nabla w, bisim (N w) (N w) +

Subgoal 6.2

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (up X) N}

nabla w, bisim (N w) (N w) +

bisim_refl < intros.

Subgoal 6.2

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (up X) N}

bisim (N n1) (N n1) +

Subgoal 6.2

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (up X) N}

bisim (N n1) (N n1) +

bisim_refl < apply CH with P = N n1.

Subgoal 6.2

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (up X) N}

H2: bisim (N n1) (N n1) +

bisim (N n1) (N n1) +

Subgoal 6.2

Variables: P X N

CH: forall P, bisim P P +

H1: {oneb P (up X) N}

H2: bisim (N n1) (N n1) +

bisim (N n1) (N n1) +

bisim_refl < search.

Proof completed

forall P Q, bisim P Q -> bisim Q P

bisim_sym < intros.

Variables: P Q

H1: bisim P Q

bisim Q P

Variables: P Q

H1: bisim P Q

bisim Q P

bisim_sym < case H1.

Variables: P Q

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

bisim Q P

Variables: P Q

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

bisim Q P

bisim_sym < unfold.

Subgoal 1

Variables: P Q

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

forall A P1, {one Q A P1} -> (exists Q1, {one P A Q1} /\ bisim P1 Q1)

(+ 5 more subgoals)

Subgoal 1

Variables: P Q

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

forall A P1, {one Q A P1} -> (exists Q1, {one P A Q1} /\ bisim P1 Q1)

(+ 5 more subgoals)

bisim_sym < intros.

Subgoal 1

Variables: P Q A P1

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {one Q A P1}

exists Q1, {one P A Q1} /\ bisim P1 Q1

(+ 5 more subgoals)

Subgoal 1

Variables: P Q A P1

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {one Q A P1}

exists Q1, {one P A Q1} /\ bisim P1 Q1

(+ 5 more subgoals)

bisim_sym < apply H5 to H8.

Subgoal 1

Variables: P Q A P1 P2

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {one Q A P1}

H9: {one P A P2}

H10: bisim P1 P2

exists Q1, {one P A Q1} /\ bisim P1 Q1

(+ 5 more subgoals)

Subgoal 1

Variables: P Q A P1 P2

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {one Q A P1}

H9: {one P A P2}

H10: bisim P1 P2

exists Q1, {one P A Q1} /\ bisim P1 Q1

(+ 5 more subgoals)

bisim_sym < search.

Subgoal 2

Variables: P Q

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

forall X M, {oneb Q (dn X) M} -> (exists N, {oneb P (dn X) N} /\ (forall W, bisim (M W) (N W)))

(+ 4 more subgoals)

Subgoal 2

Variables: P Q

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

forall X M, {oneb Q (dn X) M} -> (exists N, {oneb P (dn X) N} /\ (forall W, bisim (M W) (N W)))

(+ 4 more subgoals)

bisim_sym < intros.

Subgoal 2

Variables: P Q X M

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb Q (dn X) M}

exists N, {oneb P (dn X) N} /\ (forall W, bisim (M W) (N W))

(+ 4 more subgoals)

Subgoal 2

Variables: P Q X M

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb Q (dn X) M}

exists N, {oneb P (dn X) N} /\ (forall W, bisim (M W) (N W))

(+ 4 more subgoals)

bisim_sym < apply H6 to H8.

Subgoal 2

Variables: P Q X M M1

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb Q (dn X) M}

H9: {oneb P (dn X) M1}

H10: forall W, bisim (M W) (M1 W)

exists N, {oneb P (dn X) N} /\ (forall W, bisim (M W) (N W))

(+ 4 more subgoals)

Subgoal 2

Variables: P Q X M M1

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb Q (dn X) M}

H9: {oneb P (dn X) M1}

H10: forall W, bisim (M W) (M1 W)

exists N, {oneb P (dn X) N} /\ (forall W, bisim (M W) (N W))

(+ 4 more subgoals)

bisim_sym < search.

Subgoal 3

Variables: P Q

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

forall X M, {oneb Q (up X) M} -> (exists N, {oneb P (up X) N} /\ (nabla w, bisim (M w) (N w)))

(+ 3 more subgoals)

Subgoal 3

Variables: P Q

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

forall X M, {oneb Q (up X) M} -> (exists N, {oneb P (up X) N} /\ (nabla w, bisim (M w) (N w)))

(+ 3 more subgoals)

bisim_sym < intros.

Subgoal 3

Variables: P Q X M

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb Q (up X) M}

exists N, {oneb P (up X) N} /\ (nabla w, bisim (M w) (N w))

(+ 3 more subgoals)

Subgoal 3

Variables: P Q X M

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb Q (up X) M}

exists N, {oneb P (up X) N} /\ (nabla w, bisim (M w) (N w))

(+ 3 more subgoals)

bisim_sym < apply H7 to H8.

Subgoal 3

Variables: P Q X M M1

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb Q (up X) M}

H9: {oneb P (up X) M1}

H10: bisim (M n1) (M1 n1)

exists N, {oneb P (up X) N} /\ (nabla w, bisim (M w) (N w))

(+ 3 more subgoals)

Subgoal 3

Variables: P Q X M M1

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb Q (up X) M}

H9: {oneb P (up X) M1}

H10: bisim (M n1) (M1 n1)

exists N, {oneb P (up X) N} /\ (nabla w, bisim (M w) (N w))

(+ 3 more subgoals)

bisim_sym < search.

Subgoal 4

Variables: P Q

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

forall A Q1, {one P A Q1} -> (exists P1, {one Q A P1} /\ bisim Q1 P1)

(+ 2 more subgoals)

Subgoal 4

Variables: P Q

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

forall A Q1, {one P A Q1} -> (exists P1, {one Q A P1} /\ bisim Q1 P1)

(+ 2 more subgoals)

bisim_sym < intros.

Subgoal 4

Variables: P Q A Q1

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {one P A Q1}

exists P1, {one Q A P1} /\ bisim Q1 P1

(+ 2 more subgoals)

Subgoal 4

Variables: P Q A Q1

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {one P A Q1}

exists P1, {one Q A P1} /\ bisim Q1 P1

(+ 2 more subgoals)

bisim_sym < apply H2 to H8.

Subgoal 4

Variables: P Q A Q1 Q2

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {one P A Q1}

H9: {one Q A Q2}

H10: bisim Q1 Q2

exists P1, {one Q A P1} /\ bisim Q1 P1

(+ 2 more subgoals)

Subgoal 4

Variables: P Q A Q1 Q2

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {one P A Q1}

H9: {one Q A Q2}

H10: bisim Q1 Q2

exists P1, {one Q A P1} /\ bisim Q1 P1

(+ 2 more subgoals)

bisim_sym < search.

Subgoal 5

Variables: P Q

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

forall X N, {oneb P (dn X) N} -> (exists M, {oneb Q (dn X) M} /\ (forall W, bisim (N W) (M W)))

(+ 1 more subgoal)

Subgoal 5

Variables: P Q

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

forall X N, {oneb P (dn X) N} -> (exists M, {oneb Q (dn X) M} /\ (forall W, bisim (N W) (M W)))

(+ 1 more subgoal)

bisim_sym < intros.

Subgoal 5

Variables: P Q X N

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb P (dn X) N}

exists M, {oneb Q (dn X) M} /\ (forall W, bisim (N W) (M W))

(+ 1 more subgoal)

Subgoal 5

Variables: P Q X N

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb P (dn X) N}

exists M, {oneb Q (dn X) M} /\ (forall W, bisim (N W) (M W))

(+ 1 more subgoal)

bisim_sym < apply H3 to H8.

Subgoal 5

Variables: P Q X N N1

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb P (dn X) N}

H9: {oneb Q (dn X) N1}

H10: forall W, bisim (N W) (N1 W)

exists M, {oneb Q (dn X) M} /\ (forall W, bisim (N W) (M W))

(+ 1 more subgoal)

Subgoal 5

Variables: P Q X N N1

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb P (dn X) N}

H9: {oneb Q (dn X) N1}

H10: forall W, bisim (N W) (N1 W)

exists M, {oneb Q (dn X) M} /\ (forall W, bisim (N W) (M W))

(+ 1 more subgoal)

bisim_sym < search.

Subgoal 6

Variables: P Q

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

forall X N, {oneb P (up X) N} -> (exists M, {oneb Q (up X) M} /\ (nabla w, bisim (N w) (M w)))

Subgoal 6

Variables: P Q

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

forall X N, {oneb P (up X) N} -> (exists M, {oneb Q (up X) M} /\ (nabla w, bisim (N w) (M w)))

bisim_sym < intros.

Subgoal 6

Variables: P Q X N

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb P (up X) N}

exists M, {oneb Q (up X) M} /\ (nabla w, bisim (N w) (M w))

Subgoal 6

Variables: P Q X N

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb P (up X) N}

exists M, {oneb Q (up X) M} /\ (nabla w, bisim (N w) (M w))

bisim_sym < apply H4 to H8.

Subgoal 6

Variables: P Q X N N1

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb P (up X) N}

H9: {oneb Q (up X) N1}

H10: bisim (N n1) (N1 n1)

exists M, {oneb Q (up X) M} /\ (nabla w, bisim (N w) (M w))

Subgoal 6

Variables: P Q X N N1

H2: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H3: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H4: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H5: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H6: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H7: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H8: {oneb P (up X) N}

H9: {oneb Q (up X) N1}

H10: bisim (N n1) (N1 n1)

exists M, {oneb Q (up X) M} /\ (nabla w, bisim (N w) (M w))

bisim_sym < search.

Proof completed

forall P Q R, bisim P Q -> bisim Q R -> bisim P R

bisim_trans < coinduction.

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 #

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.

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 #

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.

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, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H6: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H7: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H8: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

bisim P R #

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, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H6: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H7: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H8: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

bisim P R #

bisim_trans < case H2.

Variables: P Q R

CH: forall P Q R, bisim P Q -> bisim Q R -> bisim P R +

H3: forall A P2, {one P A P2} -> (exists Q2, {one Q A Q2} /\ bisim P2 Q2)

H4: forall X M, {oneb P (dn X) M} -> (exists N, {oneb Q (dn X) N} /\ (forall W, bisim (M W) (N W)))

H5: forall X M, {oneb P (up X) M} -> (exists N, {oneb Q (up X) N} /\ (nabla w, bisim (M w) (N w)))

H6: forall A Q2, {one Q A Q2} -> (exists P2, {one P A P2} /\ bisim Q2 P2)

H7: forall X N, {oneb Q (dn X) N} -> (exists M, {oneb P (dn X) M} /\ (forall W, bisim (N W) (M W)))

H8: forall X N, {oneb Q (up X) N} -> (exists M, {oneb P (up X) M} /\ (nabla w, bisim (N w) (M w)))

H9: forall A P2, {one Q A P2} -> (exists Q2, {one R A Q2} /\ bisim P2 Q2)

H10: forall X M, {oneb Q (dn X) M} -> (exists N, {oneb R (dn X) N} /\ (forall W, bisim (M W) (N W)))

H11: forall X M, {oneb Q (up X) M} -> (exists N, {oneb R (up X) N} /\ (nabla w, bisim (M w) (N w)))

H12: forall A Q2, {one R A Q2} -> (exists P2, {one Q A P2} /\ bisim Q2 P2)

H13: forall X N, {oneb R (dn X) N} -> (exists M, {oneb Q (dn X) M} /\ (forall W, bisim (N W) (M W)))

H14: forall X N, {oneb R (up X) N} -> (exists M, {oneb Q (up X) M} /\ (nabla w, bisim (N w) (M w)))