Welcome to Abella 2.0.5-dev.
Abella < Specification "processes_terms".
Reading specification "processes_terms".


Abella < Define trans : pt -> (pt -> pt) -> prop by
nabla x, trans x (out x);
trans (app U V) (a\nu (b\nu (x\par (P b) (par (out2 b x a) (in x Q))))) := trans U P /\ trans V Q;
trans (abs U) (a\in2 a P) := nabla x, trans (U x) (P x);
trans (subex U V) (a\nu (x\par (P x a) (in x Q))) := (nabla y, trans (U y) (P y)) /\ trans V Q.


Abella < Theorem trans_fonc :
forall U P Q, trans U P -> trans U Q -> P = Q.



============================
forall U P Q, trans U P -> trans U Q -> P = Q

trans_fonc < induction on 1.


IH : forall U P Q, trans U P * -> trans U Q -> P = Q
============================
forall U P Q, trans U P @ -> trans U Q -> P = Q

trans_fonc < intros.


Variables: U P Q
IH : forall U P Q, trans U P * -> trans U Q -> P = Q
H1 : trans U P @
H2 : trans U Q
============================
P = Q

trans_fonc < case H1.

Subgoal 1:

Variables: Q
IH : forall U P Q, trans U P * -> trans U Q -> P = Q
H2 : trans n1 (Q n1)
============================
out n1 = Q n1

Subgoal 2 is:
a\nu (b\nu (x\par (P1 b) (par (out2 b x a) (in x Q1)))) = Q

Subgoal 3 is:
a\in2 a P1 = Q

Subgoal 4 is:
a\nu (x\par (P1 x a) (in x Q1)) = Q

trans_fonc < case H2.

Subgoal 1:

IH : forall U P Q, trans U P * -> trans U Q -> P = Q
============================
out n1 = out n1

Subgoal 2 is:
a\nu (b\nu (x\par (P1 b) (par (out2 b x a) (in x Q1)))) = Q

Subgoal 3 is:
a\in2 a P1 = Q

Subgoal 4 is:
a\nu (x\par (P1 x a) (in x Q1)) = Q

trans_fonc < search.

Subgoal 2:

Variables: Q Q1 P1 V U1
IH : forall U P Q, trans U P * -> trans U Q -> P = Q
H2 : trans (app U1 V) Q
H3 : trans U1 P1 *
H4 : trans V Q1 *
============================
a\nu (b\nu (x\par (P1 b) (par (out2 b x a) (in x Q1)))) = Q

Subgoal 3 is:
a\in2 a P1 = Q

Subgoal 4 is:
a\nu (x\par (P1 x a) (in x Q1)) = Q

trans_fonc < case H2.

Subgoal 2:

Variables: Q1 P1 V U1 Q2 P2
IH : forall U P Q, trans U P * -> trans U Q -> P = Q
H3 : trans U1 P1 *
H4 : trans V Q1 *
H5 : trans U1 P2
H6 : trans V Q2
============================
a\nu (b\nu (x\par (P1 b) (par (out2 b x a) (in x Q1)))) =
a\nu (b\nu (x\par (P2 b) (par (out2 b x a) (in x Q2))))

Subgoal 3 is:
a\in2 a P1 = Q

Subgoal 4 is:
a\nu (x\par (P1 x a) (in x Q1)) = Q

trans_fonc < apply IH to H3 H5.

Subgoal 2:

Variables: Q1 V U1 Q2 P2
IH : forall U P Q, trans U P * -> trans U Q -> P = Q
H3 : trans U1 P2 *
H4 : trans V Q1 *
H5 : trans U1 P2
H6 : trans V Q2
============================
a\nu (b\nu (x\par (P2 b) (par (out2 b x a) (in x Q1)))) =
a\nu (b\nu (x\par (P2 b) (par (out2 b x a) (in x Q2))))

Subgoal 3 is:
a\in2 a P1 = Q

Subgoal 4 is:
a\nu (x\par (P1 x a) (in x Q1)) = Q

trans_fonc < apply IH to H4 H6.

Subgoal 2:

Variables: V U1 Q2 P2
IH : forall U P Q, trans U P * -> trans U Q -> P = Q
H3 : trans U1 P2 *
H4 : trans V Q2 *
H5 : trans U1 P2
H6 : trans V Q2
============================
a\nu (b\nu (x\par (P2 b) (par (out2 b x a) (in x Q2)))) =
a\nu (b\nu (x\par (P2 b) (par (out2 b x a) (in x Q2))))

Subgoal 3 is:
a\in2 a P1 = Q

Subgoal 4 is:
a\nu (x\par (P1 x a) (in x Q1)) = Q

trans_fonc < search.

Subgoal 3:

Variables: Q P1 U1
IH : forall U P Q, trans U P * -> trans U Q -> P = Q
H2 : trans (abs U1) Q
H3 : trans (U1 n1) (P1 n1) *
============================
a\in2 a P1 = Q

Subgoal 4 is:
a\nu (x\par (P1 x a) (in x Q1)) = Q

trans_fonc < case H2.

Subgoal 3:

Variables: P1 U1 P2
IH : forall U P Q, trans U P * -> trans U Q -> P = Q
H3 : trans (U1 n1) (P1 n1) *
H4 : trans (U1 n1) (P2 n1)
============================
a\in2 a P1 = a\in2 a P2

Subgoal 4 is:
a\nu (x\par (P1 x a) (in x Q1)) = Q

trans_fonc < apply IH to H3 H4.

Subgoal 3:

Variables: U1 P2
IH : forall U P Q, trans U P * -> trans U Q -> P = Q
H3 : trans (U1 n1) (P2 n1) *
H4 : trans (U1 n1) (P2 n1)
============================
a\in2 a (z1\P2 z1) = a\in2 a P2

Subgoal 4 is:
a\nu (x\par (P1 x a) (in x Q1)) = Q

trans_fonc < search.

Subgoal 4:

Variables: Q Q1 P1 V U1
IH : forall U P Q, trans U P * -> trans U Q -> P = Q
H2 : trans (subex U1 V) Q
H3 : trans (U1 n1) (P1 n1) *
H4 : trans V Q1 *
============================
a\nu (x\par (P1 x a) (in x Q1)) = Q

trans_fonc < case H2.

Subgoal 4:

Variables: Q1 P1 V U1 Q2 P2
IH : forall U P Q, trans U P * -> trans U Q -> P = Q
H3 : trans (U1 n1) (P1 n1) *
H4 : trans V Q1 *
H5 : trans (U1 n1) (P2 n1)
H6 : trans V Q2
============================
a\nu (x\par (P1 x a) (in x Q1)) = a\nu (x\par (P2 x a) (in x Q2))

trans_fonc < apply IH to H3 H5.

Subgoal 4:

Variables: Q1 V U1 Q2 P2
IH : forall U P Q, trans U P * -> trans U Q -> P = Q
H3 : trans (U1 n1) (P2 n1) *
H4 : trans V Q1 *
H5 : trans (U1 n1) (P2 n1)
H6 : trans V Q2
============================
a\nu (x\par (P2 x a) (in x Q1)) = a\nu (x\par (P2 x a) (in x Q2))

trans_fonc < apply IH to H4 H6.

Subgoal 4:

Variables: V U1 Q2 P2
IH : forall U P Q, trans U P * -> trans U Q -> P = Q
H3 : trans (U1 n1) (P2 n1) *
H4 : trans V Q2 *
H5 : trans (U1 n1) (P2 n1)
H6 : trans V Q2
============================
a\nu (x\par (P2 x a) (in x Q2)) = a\nu (x\par (P2 x a) (in x Q2))

trans_fonc < search.
Proof completed.

Abella <