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 <