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


Abella < Define str_ker : pt -> pt -> prop,
str_eq : pt -> pt -> prop by
str_ker (par P null) P;
str_ker (par null P) P;
str_ker P (par P null);
str_ker P (par null P);
str_ker (nu x\null) null;
str_ker null (nu x\null);
str_ker (par P Q) (par Q P);
str_ker (par (par P Q) R) (par P (par Q R));
str_ker (par P (par Q R)) (par (par P Q) R);
str_ker (nu (x\par P (Q x))) (par P (nu Q));
str_ker (nu (x\par (P x) Q)) (par (nu P) Q);
str_ker (par P (nu Q)) (nu (x\par P (Q x)));
str_ker (par (nu P) Q) (nu (x\par (P x) Q));
str_ker (nu (x\nu (P x))) (nu (y\nu (x\P x y)));
str_eq P P;
str_eq P Q := str_ker P Q;
str_eq (nu P) (nu Q) := nabla x, str_eq (P x) (Q x);
str_eq (par P R) (par Q R) := str_eq P Q;
str_eq (par P Q) (par P R) := str_eq Q R;
str_eq P R := exists Q, str_eq P Q /\ str_eq Q R.


Abella < Theorem str_ker_sym :
forall P Q, str_ker P Q -> str_ker Q P.



============================
forall P Q, str_ker P Q -> str_ker Q P

str_ker_sym < intros.


Variables: P Q
H1 : str_ker P Q
============================
str_ker Q P

str_ker_sym < case H1.

Subgoal 1:

Variables: Q
============================
str_ker Q (par Q null)

Subgoal 2 is:
str_ker Q (par null Q)

Subgoal 3 is:
str_ker (par P null) P

Subgoal 4 is:
str_ker (par null P) P

Subgoal 5 is:
str_ker null (nu x\null)

Subgoal 6 is:
str_ker (nu x\null) null

Subgoal 7 is:
str_ker (par Q1 P1) (par P1 Q1)

Subgoal 8 is:
str_ker (par P1 (par Q1 R)) (par (par P1 Q1) R)

Subgoal 9 is:
str_ker (par (par P1 Q1) R) (par P1 (par Q1 R))

Subgoal 10 is:
str_ker (par P1 (nu Q1)) (nu (x\par P1 (Q1 x)))

Subgoal 11 is:
str_ker (par (nu P1) Q1) (nu (x\par (P1 x) Q1))

Subgoal 12 is:
str_ker (nu (x\par P1 (Q1 x))) (par P1 (nu Q1))

Subgoal 13 is:
str_ker (nu (x\par (P1 x) Q1)) (par (nu P1) Q1)

Subgoal 14 is:
str_ker (nu (y\nu (x\P1 x y))) (nu (x\nu (P1 x)))

str_ker_sym < search.

Subgoal 2:

Variables: Q
============================
str_ker Q (par null Q)

Subgoal 3 is:
str_ker (par P null) P

Subgoal 4 is:
str_ker (par null P) P

Subgoal 5 is:
str_ker null (nu x\null)

Subgoal 6 is:
str_ker (nu x\null) null

Subgoal 7 is:
str_ker (par Q1 P1) (par P1 Q1)

Subgoal 8 is:
str_ker (par P1 (par Q1 R)) (par (par P1 Q1) R)

Subgoal 9 is:
str_ker (par (par P1 Q1) R) (par P1 (par Q1 R))

Subgoal 10 is:
str_ker (par P1 (nu Q1)) (nu (x\par P1 (Q1 x)))

Subgoal 11 is:
str_ker (par (nu P1) Q1) (nu (x\par (P1 x) Q1))

Subgoal 12 is:
str_ker (nu (x\par P1 (Q1 x))) (par P1 (nu Q1))

Subgoal 13 is:
str_ker (nu (x\par (P1 x) Q1)) (par (nu P1) Q1)

Subgoal 14 is:
str_ker (nu (y\nu (x\P1 x y))) (nu (x\nu (P1 x)))

str_ker_sym < search.

Subgoal 3:

Variables: P
============================
str_ker (par P null) P

Subgoal 4 is:
str_ker (par null P) P

Subgoal 5 is:
str_ker null (nu x\null)

Subgoal 6 is:
str_ker (nu x\null) null

Subgoal 7 is:
str_ker (par Q1 P1) (par P1 Q1)

Subgoal 8 is:
str_ker (par P1 (par Q1 R)) (par (par P1 Q1) R)

Subgoal 9 is:
str_ker (par (par P1 Q1) R) (par P1 (par Q1 R))

Subgoal 10 is:
str_ker (par P1 (nu Q1)) (nu (x\par P1 (Q1 x)))

Subgoal 11 is:
str_ker (par (nu P1) Q1) (nu (x\par (P1 x) Q1))

Subgoal 12 is:
str_ker (nu (x\par P1 (Q1 x))) (par P1 (nu Q1))

Subgoal 13 is:
str_ker (nu (x\par (P1 x) Q1)) (par (nu P1) Q1)

Subgoal 14 is:
str_ker (nu (y\nu (x\P1 x y))) (nu (x\nu (P1 x)))

str_ker_sym < search.

Subgoal 4:

Variables: P
============================
str_ker (par null P) P

Subgoal 5 is:
str_ker null (nu x\null)

Subgoal 6 is:
str_ker (nu x\null) null

Subgoal 7 is:
str_ker (par Q1 P1) (par P1 Q1)

Subgoal 8 is:
str_ker (par P1 (par Q1 R)) (par (par P1 Q1) R)

Subgoal 9 is:
str_ker (par (par P1 Q1) R) (par P1 (par Q1 R))

Subgoal 10 is:
str_ker (par P1 (nu Q1)) (nu (x\par P1 (Q1 x)))

Subgoal 11 is:
str_ker (par (nu P1) Q1) (nu (x\par (P1 x) Q1))

Subgoal 12 is:
str_ker (nu (x\par P1 (Q1 x))) (par P1 (nu Q1))

Subgoal 13 is:
str_ker (nu (x\par (P1 x) Q1)) (par (nu P1) Q1)

Subgoal 14 is:
str_ker (nu (y\nu (x\P1 x y))) (nu (x\nu (P1 x)))

str_ker_sym < search.

Subgoal 5:

============================
str_ker null (nu x\null)

Subgoal 6 is:
str_ker (nu x\null) null

Subgoal 7 is:
str_ker (par Q1 P1) (par P1 Q1)

Subgoal 8 is:
str_ker (par P1 (par Q1 R)) (par (par P1 Q1) R)

Subgoal 9 is:
str_ker (par (par P1 Q1) R) (par P1 (par Q1 R))

Subgoal 10 is:
str_ker (par P1 (nu Q1)) (nu (x\par P1 (Q1 x)))

Subgoal 11 is:
str_ker (par (nu P1) Q1) (nu (x\par (P1 x) Q1))

Subgoal 12 is:
str_ker (nu (x\par P1 (Q1 x))) (par P1 (nu Q1))

Subgoal 13 is:
str_ker (nu (x\par (P1 x) Q1)) (par (nu P1) Q1)

Subgoal 14 is:
str_ker (nu (y\nu (x\P1 x y))) (nu (x\nu (P1 x)))

str_ker_sym < search.

Subgoal 6:

============================
str_ker (nu x\null) null

Subgoal 7 is:
str_ker (par Q1 P1) (par P1 Q1)

Subgoal 8 is:
str_ker (par P1 (par Q1 R)) (par (par P1 Q1) R)

Subgoal 9 is:
str_ker (par (par P1 Q1) R) (par P1 (par Q1 R))

Subgoal 10 is:
str_ker (par P1 (nu Q1)) (nu (x\par P1 (Q1 x)))

Subgoal 11 is:
str_ker (par (nu P1) Q1) (nu (x\par (P1 x) Q1))

Subgoal 12 is:
str_ker (nu (x\par P1 (Q1 x))) (par P1 (nu Q1))

Subgoal 13 is:
str_ker (nu (x\par (P1 x) Q1)) (par (nu P1) Q1)

Subgoal 14 is:
str_ker (nu (y\nu (x\P1 x y))) (nu (x\nu (P1 x)))

str_ker_sym < search.

Subgoal 7:

Variables: P1 Q1
============================
str_ker (par Q1 P1) (par P1 Q1)

Subgoal 8 is:
str_ker (par P1 (par Q1 R)) (par (par P1 Q1) R)

Subgoal 9 is:
str_ker (par (par P1 Q1) R) (par P1 (par Q1 R))

Subgoal 10 is:
str_ker (par P1 (nu Q1)) (nu (x\par P1 (Q1 x)))

Subgoal 11 is:
str_ker (par (nu P1) Q1) (nu (x\par (P1 x) Q1))

Subgoal 12 is:
str_ker (nu (x\par P1 (Q1 x))) (par P1 (nu Q1))

Subgoal 13 is:
str_ker (nu (x\par (P1 x) Q1)) (par (nu P1) Q1)

Subgoal 14 is:
str_ker (nu (y\nu (x\P1 x y))) (nu (x\nu (P1 x)))

str_ker_sym < search.

Subgoal 8:

Variables: R Q1 P1
============================
str_ker (par P1 (par Q1 R)) (par (par P1 Q1) R)

Subgoal 9 is:
str_ker (par (par P1 Q1) R) (par P1 (par Q1 R))

Subgoal 10 is:
str_ker (par P1 (nu Q1)) (nu (x\par P1 (Q1 x)))

Subgoal 11 is:
str_ker (par (nu P1) Q1) (nu (x\par (P1 x) Q1))

Subgoal 12 is:
str_ker (nu (x\par P1 (Q1 x))) (par P1 (nu Q1))

Subgoal 13 is:
str_ker (nu (x\par (P1 x) Q1)) (par (nu P1) Q1)

Subgoal 14 is:
str_ker (nu (y\nu (x\P1 x y))) (nu (x\nu (P1 x)))

str_ker_sym < search.

Subgoal 9:

Variables: R Q1 P1
============================
str_ker (par (par P1 Q1) R) (par P1 (par Q1 R))

Subgoal 10 is:
str_ker (par P1 (nu Q1)) (nu (x\par P1 (Q1 x)))

Subgoal 11 is:
str_ker (par (nu P1) Q1) (nu (x\par (P1 x) Q1))

Subgoal 12 is:
str_ker (nu (x\par P1 (Q1 x))) (par P1 (nu Q1))

Subgoal 13 is:
str_ker (nu (x\par (P1 x) Q1)) (par (nu P1) Q1)

Subgoal 14 is:
str_ker (nu (y\nu (x\P1 x y))) (nu (x\nu (P1 x)))

str_ker_sym < search.

Subgoal 10:

Variables: Q1 P1
============================
str_ker (par P1 (nu Q1)) (nu (x\par P1 (Q1 x)))

Subgoal 11 is:
str_ker (par (nu P1) Q1) (nu (x\par (P1 x) Q1))

Subgoal 12 is:
str_ker (nu (x\par P1 (Q1 x))) (par P1 (nu Q1))

Subgoal 13 is:
str_ker (nu (x\par (P1 x) Q1)) (par (nu P1) Q1)

Subgoal 14 is:
str_ker (nu (y\nu (x\P1 x y))) (nu (x\nu (P1 x)))

str_ker_sym < search.

Subgoal 11:

Variables: Q1 P1
============================
str_ker (par (nu P1) Q1) (nu (x\par (P1 x) Q1))

Subgoal 12 is:
str_ker (nu (x\par P1 (Q1 x))) (par P1 (nu Q1))

Subgoal 13 is:
str_ker (nu (x\par (P1 x) Q1)) (par (nu P1) Q1)

Subgoal 14 is:
str_ker (nu (y\nu (x\P1 x y))) (nu (x\nu (P1 x)))

str_ker_sym < search.

Subgoal 12:

Variables: Q1 P1
============================
str_ker (nu (x\par P1 (Q1 x))) (par P1 (nu Q1))

Subgoal 13 is:
str_ker (nu (x\par (P1 x) Q1)) (par (nu P1) Q1)

Subgoal 14 is:
str_ker (nu (y\nu (x\P1 x y))) (nu (x\nu (P1 x)))

str_ker_sym < search.

Subgoal 13:

Variables: Q1 P1
============================
str_ker (nu (x\par (P1 x) Q1)) (par (nu P1) Q1)

Subgoal 14 is:
str_ker (nu (y\nu (x\P1 x y))) (nu (x\nu (P1 x)))

str_ker_sym < search.

Subgoal 14:

Variables: P1
============================
str_ker (nu (y\nu (x\P1 x y))) (nu (x\nu (P1 x)))

str_ker_sym < search.
Proof completed.

Abella < Theorem str_eq_sym :
forall P Q, str_eq P Q -> str_eq Q P.



============================
forall P Q, str_eq P Q -> str_eq Q P

str_eq_sym < induction on 1.


IH : forall P Q, str_eq P Q * -> str_eq Q P
============================
forall P Q, str_eq P Q @ -> str_eq Q P

str_eq_sym < intros.


Variables: P Q
IH : forall P Q, str_eq P Q * -> str_eq Q P
H1 : str_eq P Q @
============================
str_eq Q P

str_eq_sym < case H1.

Subgoal 1:

Variables: Q
IH : forall P Q, str_eq P Q * -> str_eq Q P
============================
str_eq Q Q

Subgoal 2 is:
str_eq Q P

Subgoal 3 is:
str_eq (nu Q1) (nu P1)

Subgoal 4 is:
str_eq (par Q1 R) (par P1 R)

Subgoal 5 is:
str_eq (par P1 R) (par P1 Q1)

Subgoal 6 is:
str_eq Q P

str_eq_sym < search.

Subgoal 2:

Variables: P Q
IH : forall P Q, str_eq P Q * -> str_eq Q P
H2 : str_ker P Q *
============================
str_eq Q P

Subgoal 3 is:
str_eq (nu Q1) (nu P1)

Subgoal 4 is:
str_eq (par Q1 R) (par P1 R)

Subgoal 5 is:
str_eq (par P1 R) (par P1 Q1)

Subgoal 6 is:
str_eq Q P

str_eq_sym < apply str_ker_sym to H2.

Subgoal 2:

Variables: P Q
IH : forall P Q, str_eq P Q * -> str_eq Q P
H2 : str_ker P Q *
H3 : str_ker Q P
============================
str_eq Q P

Subgoal 3 is:
str_eq (nu Q1) (nu P1)

Subgoal 4 is:
str_eq (par Q1 R) (par P1 R)

Subgoal 5 is:
str_eq (par P1 R) (par P1 Q1)

Subgoal 6 is:
str_eq Q P

str_eq_sym < search.

Subgoal 3:

Variables: Q1 P1
IH : forall P Q, str_eq P Q * -> str_eq Q P
H2 : str_eq (P1 n1) (Q1 n1) *
============================
str_eq (nu Q1) (nu P1)

Subgoal 4 is:
str_eq (par Q1 R) (par P1 R)

Subgoal 5 is:
str_eq (par P1 R) (par P1 Q1)

Subgoal 6 is:
str_eq Q P

str_eq_sym < apply IH to H2.

Subgoal 3:

Variables: Q1 P1
IH : forall P Q, str_eq P Q * -> str_eq Q P
H2 : str_eq (P1 n1) (Q1 n1) *
H3 : str_eq (Q1 n1) (P1 n1)
============================
str_eq (nu Q1) (nu P1)

Subgoal 4 is:
str_eq (par Q1 R) (par P1 R)

Subgoal 5 is:
str_eq (par P1 R) (par P1 Q1)

Subgoal 6 is:
str_eq Q P

str_eq_sym < search.

Subgoal 4:

Variables: R Q1 P1
IH : forall P Q, str_eq P Q * -> str_eq Q P
H2 : str_eq P1 Q1 *
============================
str_eq (par Q1 R) (par P1 R)

Subgoal 5 is:
str_eq (par P1 R) (par P1 Q1)

Subgoal 6 is:
str_eq Q P

str_eq_sym < apply IH to H2.

Subgoal 4:

Variables: R Q1 P1
IH : forall P Q, str_eq P Q * -> str_eq Q P
H2 : str_eq P1 Q1 *
H3 : str_eq Q1 P1
============================
str_eq (par Q1 R) (par P1 R)

Subgoal 5 is:
str_eq (par P1 R) (par P1 Q1)

Subgoal 6 is:
str_eq Q P

str_eq_sym < search.

Subgoal 5:

Variables: R P1 Q1
IH : forall P Q, str_eq P Q * -> str_eq Q P
H2 : str_eq Q1 R *
============================
str_eq (par P1 R) (par P1 Q1)

Subgoal 6 is:
str_eq Q P

str_eq_sym < apply IH to H2.

Subgoal 5:

Variables: R P1 Q1
IH : forall P Q, str_eq P Q * -> str_eq Q P
H2 : str_eq Q1 R *
H3 : str_eq R Q1
============================
str_eq (par P1 R) (par P1 Q1)

Subgoal 6 is:
str_eq Q P

str_eq_sym < search.

Subgoal 6:

Variables: P Q Q1
IH : forall P Q, str_eq P Q * -> str_eq Q P
H2 : str_eq P Q1 *
H3 : str_eq Q1 Q *
============================
str_eq Q P

str_eq_sym < apply IH to H3.

Subgoal 6:

Variables: P Q Q1
IH : forall P Q, str_eq P Q * -> str_eq Q P
H2 : str_eq P Q1 *
H3 : str_eq Q1 Q *
H4 : str_eq Q Q1
============================
str_eq Q P

str_eq_sym < apply IH to H2.

Subgoal 6:

Variables: P Q Q1
IH : forall P Q, str_eq P Q * -> str_eq Q P
H2 : str_eq P Q1 *
H3 : str_eq Q1 Q *
H4 : str_eq Q Q1
H5 : str_eq Q1 P
============================
str_eq Q P

str_eq_sym < search.
Proof completed.

Abella < Theorem nu_gen :
forall P, str_eq P (nu x\P).



============================
forall P, str_eq P (nu x\P)

nu_gen < intros.


Variables: P
============================
str_eq P (nu x\P)

nu_gen < unfold 20.


Variables: P
============================
exists Q, str_eq P Q /\ str_eq Q (nu x\P)

nu_gen < exists nu (x\par P null).


Variables: P
============================
str_eq P (nu (x\par P null)) /\ str_eq (nu (x\par P null)) (nu x\P)

nu_gen < search.
Proof completed.

Abella < Define red_ker_tensor : pt -> pt -> pt -> prop,
red_tensor : pt -> pt -> prop,
red_ker_exp : pt -> pt -> pt -> prop,
red_exp : pt -> pt -> prop,
red : pt -> pt -> prop by
nabla x y z, red_ker_tensor (out2 x y z) (in2 x (P x y z)) (P x y z y z);
nabla x y z, red_ker_tensor (in2 x (P x y z)) (out2 x y z) (P x y z y z);
red_ker_tensor (par P Q) R (par S Q) := red_ker_tensor P R S;
red_ker_tensor (par P Q) R (par P S) := red_ker_tensor Q R S;
red_ker_tensor (nu P) Q (nu R) := nabla x, red_ker_tensor (P x) Q (R x);
red_ker_tensor P (par Q R) (par S R) := red_ker_tensor P Q S;
red_ker_tensor P (par Q R) (par Q S) := red_ker_tensor P R S;
red_ker_tensor P (nu Q) (nu R) := nabla x, red_ker_tensor P (Q x) (R x);
red_tensor (par P Q) R := red_ker_tensor P Q R;
red_tensor (par P1 Q) (par P2 Q) := red_tensor P1 P2;
red_tensor (par P Q1) (par P Q2) := red_tensor Q1 Q2;
red_tensor (nu P1) (nu P2) := nabla x, red_tensor (P1 x) (P2 x);
nabla x y, red_ker_exp (out x y) (in x (P x y)) (par (P x y y) (in x (P x y)));
nabla x y, red_ker_exp (in x (P x y)) (out x y) (par (P x y y) (in x (P x y)));
red_ker_exp (par P Q) R (par S Q) := red_ker_exp P R S;
red_ker_exp (par P Q) R (par P S) := red_ker_exp Q R S;
red_ker_exp (nu P) Q (nu R) := nabla x, red_ker_exp (P x) Q (R x);
red_ker_exp P (par Q R) (par S R) := red_ker_exp P Q S;
red_ker_exp P (par Q R) (par Q S) := red_ker_exp P R S;
red_ker_exp P (nu Q) (nu R) := nabla x, red_ker_exp P (Q x) (R x);
red_exp (par P Q) R := red_ker_exp P Q R;
red_exp (par P1 Q) (par P2 Q) := red_exp P1 P2;
red_exp (par P Q1) (par P Q2) := red_exp Q1 Q2;
red_exp (nu P1) (nu P2) := nabla x, red_exp (P1 x) (P2 x);
red P Q := red_tensor P Q;
red P Q := red_exp P Q.


Abella < Theorem red_ker_tensor_null_cases :
forall P Q, red_ker_tensor null P Q -> false.



============================
forall P Q, red_ker_tensor null P Q -> false

red_ker_tensor_null_cases < induction on 1.


IH : forall P Q, red_ker_tensor null P Q * -> false
============================
forall P Q, red_ker_tensor null P Q @ -> false

red_ker_tensor_null_cases < intros.


Variables: P Q
IH : forall P Q, red_ker_tensor null P Q * -> false
H1 : red_ker_tensor null P Q @
============================
false

red_ker_tensor_null_cases < case H1.

Subgoal 1:

Variables: R S Q1
IH : forall P Q, red_ker_tensor null P Q * -> false
H2 : red_ker_tensor null Q1 S *
============================
false

Subgoal 2 is:
false

Subgoal 3 is:
false

red_ker_tensor_null_cases < apply IH to H2.

Subgoal 2:

Variables: S Q1 R
IH : forall P Q, red_ker_tensor null P Q * -> false
H2 : red_ker_tensor null R S *
============================
false

Subgoal 3 is:
false

red_ker_tensor_null_cases < apply IH to H2.

Subgoal 3:

Variables: R Q1
IH : forall P Q, red_ker_tensor null P Q * -> false
H2 : red_ker_tensor null (Q1 n1) (R n1) *
============================
false

red_ker_tensor_null_cases < apply IH to H2.
Proof completed.

Abella < Theorem red_ker_exp_null_cases :
forall P Q, red_ker_exp null P Q -> false.



============================
forall P Q, red_ker_exp null P Q -> false

red_ker_exp_null_cases < induction on 1.


IH : forall P Q, red_ker_exp null P Q * -> false
============================
forall P Q, red_ker_exp null P Q @ -> false

red_ker_exp_null_cases < intros.


Variables: P Q
IH : forall P Q, red_ker_exp null P Q * -> false
H1 : red_ker_exp null P Q @
============================
false

red_ker_exp_null_cases < case H1.

Subgoal 1:

Variables: R S Q1
IH : forall P Q, red_ker_exp null P Q * -> false
H2 : red_ker_exp null Q1 S *
============================
false

Subgoal 2 is:
false

Subgoal 3 is:
false

red_ker_exp_null_cases < apply IH to H2.

Subgoal 2:

Variables: S Q1 R
IH : forall P Q, red_ker_exp null P Q * -> false
H2 : red_ker_exp null R S *
============================
false

Subgoal 3 is:
false

red_ker_exp_null_cases < apply IH to H2.

Subgoal 3:

Variables: R Q1
IH : forall P Q, red_ker_exp null P Q * -> false
H2 : red_ker_exp null (Q1 n1) (R n1) *
============================
false

red_ker_exp_null_cases < apply IH to H2.
Proof completed.

Abella < Theorem red_ker_tensor_no_new_names :
forall P Q R, nabla x, red_ker_tensor P Q (R x) ->
(exists S, nabla x, S = R x).



============================
forall P Q R, nabla x, red_ker_tensor P Q (R x) ->
(exists S, nabla x, S = R x)

red_ker_tensor_no_new_names < induction on 1.


IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x, S = R x)
============================
forall P Q R, nabla x, red_ker_tensor P Q (R x) @ ->
(exists S, nabla x, S = R x)

red_ker_tensor_no_new_names < intros.


Variables: P Q R
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x, S = R x)
H1 : red_ker_tensor P Q (R n1) @
============================
exists S, nabla x, S = R x

red_ker_tensor_no_new_names < case H1.

Subgoal 1:

Variables: Q1
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x1, S = R x1)
============================
exists S, nabla x, S = Q1 n2 n3 n4 n3 n4

Subgoal 2 is:
exists S, nabla x, S = P2 n2 n3 n4 n3 n4

Subgoal 3 is:
exists S1, nabla x, S1 = par (S x) P3

Subgoal 4 is:
exists S1, nabla x, S1 = par P2 (S x)

Subgoal 5 is:
exists S, nabla x, S = nu (R1 x)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_tensor_no_new_names < search.

Subgoal 2:

Variables: P2
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x1, S = R x1)
============================
exists S, nabla x, S = P2 n2 n3 n4 n3 n4

Subgoal 3 is:
exists S1, nabla x, S1 = par (S x) P3

Subgoal 4 is:
exists S1, nabla x, S1 = par P2 (S x)

Subgoal 5 is:
exists S, nabla x, S = nu (R1 x)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_tensor_no_new_names < search.

Subgoal 3:

Variables: Q P3 S P2
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_tensor P2 Q (S n1) *
============================
exists S1, nabla x, S1 = par (S x) P3

Subgoal 4 is:
exists S1, nabla x, S1 = par P2 (S x)

Subgoal 5 is:
exists S, nabla x, S = nu (R1 x)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_tensor_no_new_names < apply IH to H2.

Subgoal 3:

Variables: Q P3 P2 S1
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_tensor P2 Q S1 *
============================
exists S2, nabla x, S2 = par S1 P3

Subgoal 4 is:
exists S1, nabla x, S1 = par P2 (S x)

Subgoal 5 is:
exists S, nabla x, S = nu (R1 x)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_tensor_no_new_names < search.

Subgoal 4:

Variables: Q S P2 P3
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_tensor P3 Q (S n1) *
============================
exists S1, nabla x, S1 = par P2 (S x)

Subgoal 5 is:
exists S, nabla x, S = nu (R1 x)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_tensor_no_new_names < apply IH to H2.

Subgoal 4:

Variables: Q P2 P3 S1
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_tensor P3 Q S1 *
============================
exists S2, nabla x, S2 = par P2 S1

Subgoal 5 is:
exists S, nabla x, S = nu (R1 x)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_tensor_no_new_names < search.

Subgoal 5:

Variables: Q R1 P2
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_tensor (P2 n2) Q (R1 n1 n2) *
============================
exists S, nabla x, S = nu (R1 x)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_tensor_no_new_names < apply IH to H2.

Subgoal 5:

Variables: Q P2 S1
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_tensor (P2 n2) Q (S1 n2) *
============================
exists S, nabla x, S = nu (z2\S1 z2)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_tensor_no_new_names < search.

Subgoal 6:

Variables: P Q3 S Q2
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_tensor P Q2 (S n1) *
============================
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_tensor_no_new_names < apply IH to H2.

Subgoal 6:

Variables: P Q3 Q2 S1
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_tensor P Q2 S1 *
============================
exists S2, nabla x, S2 = par S1 Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_tensor_no_new_names < search.

Subgoal 7:

Variables: P S Q2 Q3
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_tensor P Q3 (S n1) *
============================
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_tensor_no_new_names < apply IH to H2.

Subgoal 7:

Variables: P Q2 Q3 S1
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_tensor P Q3 S1 *
============================
exists S2, nabla x, S2 = par Q2 S1

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_tensor_no_new_names < search.

Subgoal 8:

Variables: P R1 Q2
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_tensor P (Q2 n2) (R1 n1 n2) *
============================
exists S, nabla x, S = nu (R1 x)

red_ker_tensor_no_new_names < apply IH to H2.

Subgoal 8:

Variables: P Q2 S1
IH : forall P Q R, nabla x, red_ker_tensor P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_tensor P (Q2 n2) (S1 n2) *
============================
exists S, nabla x, S = nu (z2\S1 z2)

red_ker_tensor_no_new_names < search.
Proof completed.

Abella < Theorem red_tensor_no_new_names :
forall P Q, nabla x, red_tensor P (Q x) -> (exists R, nabla y, R = Q y).



============================
forall P Q, nabla x, red_tensor P (Q x) -> (exists R, nabla y, R = Q y)

red_tensor_no_new_names < induction on 1.


IH : forall P Q, nabla x, red_tensor P (Q x) * ->
(exists R, nabla y, R = Q y)
============================
forall P Q, nabla x, red_tensor P (Q x) @ -> (exists R, nabla y, R = Q y)

red_tensor_no_new_names < intros.


Variables: P Q
IH : forall P Q, nabla x, red_tensor P (Q x) * ->
(exists R, nabla y, R = Q y)
H1 : red_tensor P (Q n1) @
============================
exists R, nabla y, R = Q y

red_tensor_no_new_names < case H1.

Subgoal 1:

Variables: Q P3 P2
IH : forall P Q, nabla x, red_tensor P (Q x) * ->
(exists R, nabla y, R = Q y)
H2 : red_ker_tensor P2 P3 (Q n1) *
============================
exists R, nabla y, R = Q y

Subgoal 2 is:
exists R, nabla y, R = par (P2 y) P4

Subgoal 3 is:
exists R, nabla y, R = par P2 (Q2 y)

Subgoal 4 is:
exists R, nabla y, R = nu (P2 y)

red_tensor_no_new_names < backchain red_ker_tensor_no_new_names with x = n1.

Subgoal 2:

Variables: P4 P2 P3
IH : forall P Q, nabla x, red_tensor P (Q x) * ->
(exists R, nabla y, R = Q y)
H2 : red_tensor P3 (P2 n1) *
============================
exists R, nabla y, R = par (P2 y) P4

Subgoal 3 is:
exists R, nabla y, R = par P2 (Q2 y)

Subgoal 4 is:
exists R, nabla y, R = nu (P2 y)

red_tensor_no_new_names < apply IH to H2 with x = n1.

Subgoal 2:

Variables: P4 P3 R
IH : forall P Q, nabla x, red_tensor P (Q x) * ->
(exists R, nabla y, R = Q y)
H2 : red_tensor P3 R *
============================
exists R1, nabla y, R1 = par R P4

Subgoal 3 is:
exists R, nabla y, R = par P2 (Q2 y)

Subgoal 4 is:
exists R, nabla y, R = nu (P2 y)

red_tensor_no_new_names < search.

Subgoal 3:

Variables: Q2 P2 P3
IH : forall P Q, nabla x, red_tensor P (Q x) * ->
(exists R, nabla y, R = Q y)
H2 : red_tensor P3 (Q2 n1) *
============================
exists R, nabla y, R = par P2 (Q2 y)

Subgoal 4 is:
exists R, nabla y, R = nu (P2 y)

red_tensor_no_new_names < apply IH to H2 with x = n1.

Subgoal 3:

Variables: P2 P3 R
IH : forall P Q, nabla x, red_tensor P (Q x) * ->
(exists R, nabla y, R = Q y)
H2 : red_tensor P3 R *
============================
exists R1, nabla y, R1 = par P2 R

Subgoal 4 is:
exists R, nabla y, R = nu (P2 y)

red_tensor_no_new_names < search.

Subgoal 4:

Variables: P2 P3
IH : forall P Q, nabla x, red_tensor P (Q x) * ->
(exists R, nabla y, R = Q y)
H2 : red_tensor (P3 n2) (P2 n1 n2) *
============================
exists R, nabla y, R = nu (P2 y)

red_tensor_no_new_names < apply IH to H2 with x = n1.

Subgoal 4:

Variables: P3 R1
IH : forall P Q, nabla x, red_tensor P (Q x) * ->
(exists R, nabla y, R = Q y)
H2 : red_tensor (P3 n2) (R1 n2) *
============================
exists R, nabla y, R = nu (z2\R1 z2)

red_tensor_no_new_names < search.
Proof completed.

Abella < Theorem red_ker_exp_no_new_names :
forall P Q R, nabla x, red_ker_exp P Q (R x) -> (exists S, nabla x, S = R x).



============================
forall P Q R, nabla x, red_ker_exp P Q (R x) -> (exists S, nabla x, S = R x)

red_ker_exp_no_new_names < induction on 1.


IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x, S = R x)
============================
forall P Q R, nabla x, red_ker_exp P Q (R x) @ ->
(exists S, nabla x, S = R x)

red_ker_exp_no_new_names < intros.


Variables: P Q R
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x, S = R x)
H1 : red_ker_exp P Q (R n1) @
============================
exists S, nabla x, S = R x

red_ker_exp_no_new_names < case H1.

Subgoal 1:

Variables: Q1
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x1, S = R x1)
============================
exists S, nabla x, S = par (Q1 n2 n3 n3) (in n2 (Q1 n2 n3))

Subgoal 2 is:
exists S, nabla x, S = par (P2 n2 n3 n3) (in n2 (P2 n2 n3))

Subgoal 3 is:
exists S1, nabla x, S1 = par (S x) P3

Subgoal 4 is:
exists S1, nabla x, S1 = par P2 (S x)

Subgoal 5 is:
exists S, nabla x, S = nu (R1 x)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_exp_no_new_names < search.

Subgoal 2:

Variables: P2
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x1, S = R x1)
============================
exists S, nabla x, S = par (P2 n2 n3 n3) (in n2 (P2 n2 n3))

Subgoal 3 is:
exists S1, nabla x, S1 = par (S x) P3

Subgoal 4 is:
exists S1, nabla x, S1 = par P2 (S x)

Subgoal 5 is:
exists S, nabla x, S = nu (R1 x)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_exp_no_new_names < search.

Subgoal 3:

Variables: Q P3 S P2
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_exp P2 Q (S n1) *
============================
exists S1, nabla x, S1 = par (S x) P3

Subgoal 4 is:
exists S1, nabla x, S1 = par P2 (S x)

Subgoal 5 is:
exists S, nabla x, S = nu (R1 x)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_exp_no_new_names < apply IH to H2.

Subgoal 3:

Variables: Q P3 P2 S1
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_exp P2 Q S1 *
============================
exists S2, nabla x, S2 = par S1 P3

Subgoal 4 is:
exists S1, nabla x, S1 = par P2 (S x)

Subgoal 5 is:
exists S, nabla x, S = nu (R1 x)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_exp_no_new_names < search.

Subgoal 4:

Variables: Q S P2 P3
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_exp P3 Q (S n1) *
============================
exists S1, nabla x, S1 = par P2 (S x)

Subgoal 5 is:
exists S, nabla x, S = nu (R1 x)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_exp_no_new_names < apply IH to H2.

Subgoal 4:

Variables: Q P2 P3 S1
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_exp P3 Q S1 *
============================
exists S2, nabla x, S2 = par P2 S1

Subgoal 5 is:
exists S, nabla x, S = nu (R1 x)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_exp_no_new_names < search.

Subgoal 5:

Variables: Q R1 P2
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_exp (P2 n2) Q (R1 n1 n2) *
============================
exists S, nabla x, S = nu (R1 x)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_exp_no_new_names < apply IH to H2.

Subgoal 5:

Variables: Q P2 S1
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_exp (P2 n2) Q (S1 n2) *
============================
exists S, nabla x, S = nu (z2\S1 z2)

Subgoal 6 is:
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_exp_no_new_names < search.

Subgoal 6:

Variables: P Q3 S Q2
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_exp P Q2 (S n1) *
============================
exists S1, nabla x, S1 = par (S x) Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_exp_no_new_names < apply IH to H2.

Subgoal 6:

Variables: P Q3 Q2 S1
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_exp P Q2 S1 *
============================
exists S2, nabla x, S2 = par S1 Q3

Subgoal 7 is:
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_exp_no_new_names < search.

Subgoal 7:

Variables: P S Q2 Q3
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_exp P Q3 (S n1) *
============================
exists S1, nabla x, S1 = par Q2 (S x)

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_exp_no_new_names < apply IH to H2.

Subgoal 7:

Variables: P Q2 Q3 S1
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_exp P Q3 S1 *
============================
exists S2, nabla x, S2 = par Q2 S1

Subgoal 8 is:
exists S, nabla x, S = nu (R1 x)

red_ker_exp_no_new_names < search.

Subgoal 8:

Variables: P R1 Q2
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_exp P (Q2 n2) (R1 n1 n2) *
============================
exists S, nabla x, S = nu (R1 x)

red_ker_exp_no_new_names < apply IH to H2.

Subgoal 8:

Variables: P Q2 S1
IH : forall P Q R, nabla x, red_ker_exp P Q (R x) * ->
(exists S, nabla x1, S = R x1)
H2 : red_ker_exp P (Q2 n2) (S1 n2) *
============================
exists S, nabla x, S = nu (z2\S1 z2)

red_ker_exp_no_new_names < search.
Proof completed.

Abella < Theorem red_exp_no_new_names :
forall P Q, nabla x, red_exp P (Q x) -> (exists R, nabla y, R = Q y).



============================
forall P Q, nabla x, red_exp P (Q x) -> (exists R, nabla y, R = Q y)

red_exp_no_new_names < induction on 1.


IH : forall P Q, nabla x, red_exp P (Q x) * -> (exists R, nabla y, R = Q y)
============================
forall P Q, nabla x, red_exp P (Q x) @ -> (exists R, nabla y, R = Q y)

red_exp_no_new_names < intros.


Variables: P Q
IH : forall P Q, nabla x, red_exp P (Q x) * -> (exists R, nabla y, R = Q y)
H1 : red_exp P (Q n1) @
============================
exists R, nabla y, R = Q y

red_exp_no_new_names < case H1.

Subgoal 1:

Variables: Q P3 P2
IH : forall P Q, nabla x, red_exp P (Q x) * -> (exists R, nabla y, R = Q y)
H2 : red_ker_exp P2 P3 (Q n1) *
============================
exists R, nabla y, R = Q y

Subgoal 2 is:
exists R, nabla y, R = par (P2 y) P4

Subgoal 3 is:
exists R, nabla y, R = par P2 (Q2 y)

Subgoal 4 is:
exists R, nabla y, R = nu (P2 y)

red_exp_no_new_names < backchain red_ker_exp_no_new_names with x = n1.

Subgoal 2:

Variables: P4 P2 P3
IH : forall P Q, nabla x, red_exp P (Q x) * -> (exists R, nabla y, R = Q y)
H2 : red_exp P3 (P2 n1) *
============================
exists R, nabla y, R = par (P2 y) P4

Subgoal 3 is:
exists R, nabla y, R = par P2 (Q2 y)

Subgoal 4 is:
exists R, nabla y, R = nu (P2 y)

red_exp_no_new_names < apply IH to H2 with x = n1.

Subgoal 2:

Variables: P4 P3 R
IH : forall P Q, nabla x, red_exp P (Q x) * -> (exists R, nabla y, R = Q y)
H2 : red_exp P3 R *
============================
exists R1, nabla y, R1 = par R P4

Subgoal 3 is:
exists R, nabla y, R = par P2 (Q2 y)

Subgoal 4 is:
exists R, nabla y, R = nu (P2 y)

red_exp_no_new_names < search.

Subgoal 3:

Variables: Q2 P2 P3
IH : forall P Q, nabla x, red_exp P (Q x) * -> (exists R, nabla y, R = Q y)
H2 : red_exp P3 (Q2 n1) *
============================
exists R, nabla y, R = par P2 (Q2 y)

Subgoal 4 is:
exists R, nabla y, R = nu (P2 y)

red_exp_no_new_names < apply IH to H2 with x = n1.

Subgoal 3:

Variables: P2 P3 R
IH : forall P Q, nabla x, red_exp P (Q x) * -> (exists R, nabla y, R = Q y)
H2 : red_exp P3 R *
============================
exists R1, nabla y, R1 = par P2 R

Subgoal 4 is:
exists R, nabla y, R = nu (P2 y)

red_exp_no_new_names < search.

Subgoal 4:

Variables: P2 P3
IH : forall P Q, nabla x, red_exp P (Q x) * -> (exists R, nabla y, R = Q y)
H2 : red_exp (P3 n2) (P2 n1 n2) *
============================
exists R, nabla y, R = nu (P2 y)

red_exp_no_new_names < apply IH to H2 with x = n1.

Subgoal 4:

Variables: P3 R1
IH : forall P Q, nabla x, red_exp P (Q x) * -> (exists R, nabla y, R = Q y)
H2 : red_exp (P3 n2) (R1 n2) *
============================
exists R, nabla y, R = nu (z2\R1 z2)

red_exp_no_new_names < search.
Proof completed.

Abella < Theorem red_ker_tensor_par_sym :
forall P Q R, red_ker_tensor P Q R -> red_ker_tensor Q P R.



============================
forall P Q R, red_ker_tensor P Q R -> red_ker_tensor Q P R

red_ker_tensor_par_sym < induction on 1.


IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
============================
forall P Q R, red_ker_tensor P Q R @ -> red_ker_tensor Q P R

red_ker_tensor_par_sym < intros.


Variables: P Q R
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
H1 : red_ker_tensor P Q R @
============================
red_ker_tensor Q P R

red_ker_tensor_par_sym < case H1.

Subgoal 1:

Variables: P1
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
============================
red_ker_tensor (in2 n1 (P1 n1 n2 n3)) (out2 n1 n2 n3) (P1 n1 n2 n3 n2 n3)

Subgoal 2 is:
red_ker_tensor (out2 n1 n2 n3) (in2 n1 (P1 n1 n2 n3)) (P1 n1 n2 n3 n2 n3)

Subgoal 3 is:
red_ker_tensor Q (par P1 Q1) (par S Q1)

Subgoal 4 is:
red_ker_tensor Q (par P1 Q1) (par P1 S)

Subgoal 5 is:
red_ker_tensor Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_tensor (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_tensor (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_tensor (nu Q1) P (nu R1)

red_ker_tensor_par_sym < search.

Subgoal 2:

Variables: P1
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
============================
red_ker_tensor (out2 n1 n2 n3) (in2 n1 (P1 n1 n2 n3)) (P1 n1 n2 n3 n2 n3)

Subgoal 3 is:
red_ker_tensor Q (par P1 Q1) (par S Q1)

Subgoal 4 is:
red_ker_tensor Q (par P1 Q1) (par P1 S)

Subgoal 5 is:
red_ker_tensor Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_tensor (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_tensor (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_tensor (nu Q1) P (nu R1)

red_ker_tensor_par_sym < search.

Subgoal 3:

Variables: Q Q1 S P1
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
H2 : red_ker_tensor P1 Q S *
============================
red_ker_tensor Q (par P1 Q1) (par S Q1)

Subgoal 4 is:
red_ker_tensor Q (par P1 Q1) (par P1 S)

Subgoal 5 is:
red_ker_tensor Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_tensor (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_tensor (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_tensor (nu Q1) P (nu R1)

red_ker_tensor_par_sym < apply IH to H2.

Subgoal 3:

Variables: Q Q1 S P1
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
H2 : red_ker_tensor P1 Q S *
H3 : red_ker_tensor Q P1 S
============================
red_ker_tensor Q (par P1 Q1) (par S Q1)

Subgoal 4 is:
red_ker_tensor Q (par P1 Q1) (par P1 S)

Subgoal 5 is:
red_ker_tensor Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_tensor (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_tensor (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_tensor (nu Q1) P (nu R1)

red_ker_tensor_par_sym < search.

Subgoal 4:

Variables: Q S P1 Q1
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
H2 : red_ker_tensor Q1 Q S *
============================
red_ker_tensor Q (par P1 Q1) (par P1 S)

Subgoal 5 is:
red_ker_tensor Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_tensor (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_tensor (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_tensor (nu Q1) P (nu R1)

red_ker_tensor_par_sym < apply IH to H2.

Subgoal 4:

Variables: Q S P1 Q1
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
H2 : red_ker_tensor Q1 Q S *
H3 : red_ker_tensor Q Q1 S
============================
red_ker_tensor Q (par P1 Q1) (par P1 S)

Subgoal 5 is:
red_ker_tensor Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_tensor (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_tensor (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_tensor (nu Q1) P (nu R1)

red_ker_tensor_par_sym < search.

Subgoal 5:

Variables: Q R1 P1
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
H2 : red_ker_tensor (P1 n1) Q (R1 n1) *
============================
red_ker_tensor Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_tensor (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_tensor (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_tensor (nu Q1) P (nu R1)

red_ker_tensor_par_sym < apply IH to H2.

Subgoal 5:

Variables: Q R1 P1
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
H2 : red_ker_tensor (P1 n1) Q (R1 n1) *
H3 : red_ker_tensor Q (P1 n1) (R1 n1)
============================
red_ker_tensor Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_tensor (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_tensor (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_tensor (nu Q1) P (nu R1)

red_ker_tensor_par_sym < search.

Subgoal 6:

Variables: P R1 S Q1
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
H2 : red_ker_tensor P Q1 S *
============================
red_ker_tensor (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_tensor (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_tensor (nu Q1) P (nu R1)

red_ker_tensor_par_sym < apply IH to H2.

Subgoal 6:

Variables: P R1 S Q1
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
H2 : red_ker_tensor P Q1 S *
H3 : red_ker_tensor Q1 P S
============================
red_ker_tensor (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_tensor (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_tensor (nu Q1) P (nu R1)

red_ker_tensor_par_sym < search.

Subgoal 7:

Variables: P S Q1 R1
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
H2 : red_ker_tensor P R1 S *
============================
red_ker_tensor (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_tensor (nu Q1) P (nu R1)

red_ker_tensor_par_sym < apply IH to H2.

Subgoal 7:

Variables: P S Q1 R1
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
H2 : red_ker_tensor P R1 S *
H3 : red_ker_tensor R1 P S
============================
red_ker_tensor (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_tensor (nu Q1) P (nu R1)

red_ker_tensor_par_sym < search.

Subgoal 8:

Variables: P R1 Q1
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
H2 : red_ker_tensor P (Q1 n1) (R1 n1) *
============================
red_ker_tensor (nu Q1) P (nu R1)

red_ker_tensor_par_sym < apply IH to H2.

Subgoal 8:

Variables: P R1 Q1
IH : forall P Q R, red_ker_tensor P Q R * -> red_ker_tensor Q P R
H2 : red_ker_tensor P (Q1 n1) (R1 n1) *
H3 : red_ker_tensor (Q1 n1) P (R1 n1)
============================
red_ker_tensor (nu Q1) P (nu R1)

red_ker_tensor_par_sym < search.
Proof completed.

Abella < Theorem red_ker_exp_par_sym :
forall P Q R, red_ker_exp P Q R -> red_ker_exp Q P R.



============================
forall P Q R, red_ker_exp P Q R -> red_ker_exp Q P R

red_ker_exp_par_sym < induction on 1.


IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
============================
forall P Q R, red_ker_exp P Q R @ -> red_ker_exp Q P R

red_ker_exp_par_sym < intros.


Variables: P Q R
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
H1 : red_ker_exp P Q R @
============================
red_ker_exp Q P R

red_ker_exp_par_sym < case H1.

Subgoal 1:

Variables: P1
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
============================
red_ker_exp (in n1 (P1 n1 n2)) (out n1 n2)
(par (P1 n1 n2 n2) (in n1 (P1 n1 n2)))

Subgoal 2 is:
red_ker_exp (out n1 n2) (in n1 (P1 n1 n2))
(par (P1 n1 n2 n2) (in n1 (P1 n1 n2)))

Subgoal 3 is:
red_ker_exp Q (par P1 Q1) (par S Q1)

Subgoal 4 is:
red_ker_exp Q (par P1 Q1) (par P1 S)

Subgoal 5 is:
red_ker_exp Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_exp (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_exp (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_exp (nu Q1) P (nu R1)

red_ker_exp_par_sym < search.

Subgoal 2:

Variables: P1
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
============================
red_ker_exp (out n1 n2) (in n1 (P1 n1 n2))
(par (P1 n1 n2 n2) (in n1 (P1 n1 n2)))

Subgoal 3 is:
red_ker_exp Q (par P1 Q1) (par S Q1)

Subgoal 4 is:
red_ker_exp Q (par P1 Q1) (par P1 S)

Subgoal 5 is:
red_ker_exp Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_exp (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_exp (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_exp (nu Q1) P (nu R1)

red_ker_exp_par_sym < search.

Subgoal 3:

Variables: Q Q1 S P1
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
H2 : red_ker_exp P1 Q S *
============================
red_ker_exp Q (par P1 Q1) (par S Q1)

Subgoal 4 is:
red_ker_exp Q (par P1 Q1) (par P1 S)

Subgoal 5 is:
red_ker_exp Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_exp (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_exp (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_exp (nu Q1) P (nu R1)

red_ker_exp_par_sym < apply IH to H2.

Subgoal 3:

Variables: Q Q1 S P1
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
H2 : red_ker_exp P1 Q S *
H3 : red_ker_exp Q P1 S
============================
red_ker_exp Q (par P1 Q1) (par S Q1)

Subgoal 4 is:
red_ker_exp Q (par P1 Q1) (par P1 S)

Subgoal 5 is:
red_ker_exp Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_exp (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_exp (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_exp (nu Q1) P (nu R1)

red_ker_exp_par_sym < search.

Subgoal 4:

Variables: Q S P1 Q1
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
H2 : red_ker_exp Q1 Q S *
============================
red_ker_exp Q (par P1 Q1) (par P1 S)

Subgoal 5 is:
red_ker_exp Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_exp (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_exp (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_exp (nu Q1) P (nu R1)

red_ker_exp_par_sym < apply IH to H2.

Subgoal 4:

Variables: Q S P1 Q1
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
H2 : red_ker_exp Q1 Q S *
H3 : red_ker_exp Q Q1 S
============================
red_ker_exp Q (par P1 Q1) (par P1 S)

Subgoal 5 is:
red_ker_exp Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_exp (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_exp (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_exp (nu Q1) P (nu R1)

red_ker_exp_par_sym < search.

Subgoal 5:

Variables: Q R1 P1
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
H2 : red_ker_exp (P1 n1) Q (R1 n1) *
============================
red_ker_exp Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_exp (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_exp (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_exp (nu Q1) P (nu R1)

red_ker_exp_par_sym < apply IH to H2.

Subgoal 5:

Variables: Q R1 P1
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
H2 : red_ker_exp (P1 n1) Q (R1 n1) *
H3 : red_ker_exp Q (P1 n1) (R1 n1)
============================
red_ker_exp Q (nu P1) (nu R1)

Subgoal 6 is:
red_ker_exp (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_exp (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_exp (nu Q1) P (nu R1)

red_ker_exp_par_sym < search.

Subgoal 6:

Variables: P R1 S Q1
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
H2 : red_ker_exp P Q1 S *
============================
red_ker_exp (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_exp (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_exp (nu Q1) P (nu R1)

red_ker_exp_par_sym < apply IH to H2.

Subgoal 6:

Variables: P R1 S Q1
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
H2 : red_ker_exp P Q1 S *
H3 : red_ker_exp Q1 P S
============================
red_ker_exp (par Q1 R1) P (par S R1)

Subgoal 7 is:
red_ker_exp (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_exp (nu Q1) P (nu R1)

red_ker_exp_par_sym < search.

Subgoal 7:

Variables: P S Q1 R1
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
H2 : red_ker_exp P R1 S *
============================
red_ker_exp (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_exp (nu Q1) P (nu R1)

red_ker_exp_par_sym < apply IH to H2.

Subgoal 7:

Variables: P S Q1 R1
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
H2 : red_ker_exp P R1 S *
H3 : red_ker_exp R1 P S
============================
red_ker_exp (par Q1 R1) P (par Q1 S)

Subgoal 8 is:
red_ker_exp (nu Q1) P (nu R1)

red_ker_exp_par_sym < search.

Subgoal 8:

Variables: P R1 Q1
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
H2 : red_ker_exp P (Q1 n1) (R1 n1) *
============================
red_ker_exp (nu Q1) P (nu R1)

red_ker_exp_par_sym < apply IH to H2.

Subgoal 8:

Variables: P R1 Q1
IH : forall P Q R, red_ker_exp P Q R * -> red_ker_exp Q P R
H2 : red_ker_exp P (Q1 n1) (R1 n1) *
H3 : red_ker_exp (Q1 n1) P (R1 n1)
============================
red_ker_exp (nu Q1) P (nu R1)

red_ker_exp_par_sym < search.
Proof completed.

Abella < Theorem red_ker_tensor_par_cases :
forall P Q R S, red_ker_tensor (par P Q) R S ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T)).



============================
forall P Q R S, red_ker_tensor (par P Q) R S ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))

red_ker_tensor_par_cases < induction on 1.


IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
============================
forall P Q R S, red_ker_tensor (par P Q) R S @ ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))

red_ker_tensor_par_cases < intros.


Variables: P Q R S
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H1 : red_ker_tensor (par P Q) R S @
============================
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))

red_ker_tensor_par_cases < case H1.

Subgoal 1:

Variables: P Q R S1
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor P R S1 *
============================
(exists T, red_ker_tensor P R T /\ str_eq (par S1 Q) (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq (par S1 Q) (par P T))

Subgoal 2 is:
(exists T, red_ker_tensor P R T /\ str_eq (par P S1) (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq (par P S1) (par P T))

Subgoal 3 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < search.

Subgoal 2:

Variables: P Q R S1
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor Q R S1 *
============================
(exists T, red_ker_tensor P R T /\ str_eq (par P S1) (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq (par P S1) (par P T))

Subgoal 3 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < search.

Subgoal 3:

Variables: P Q R1 S1 Q1
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
============================
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < apply IH to H2.

Subgoal 3:

Variables: P Q R1 S1 Q1
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H3 : (exists T, red_ker_tensor P Q1 T /\ str_eq S1 (par T Q)) \/
(exists T, red_ker_tensor Q Q1 T /\ str_eq S1 (par P T))
============================
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < case H3.

Subgoal 3.1:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor P Q1 T
H5 : str_eq S1 (par T Q)
============================
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 3.2 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < left.

Subgoal 3.1:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor P Q1 T
H5 : str_eq S1 (par T Q)
============================
exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)

Subgoal 3.2 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < exists par T R1.

Subgoal 3.1:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor P Q1 T
H5 : str_eq S1 (par T Q)
============================
red_ker_tensor P (par Q1 R1) (par T R1) /\
str_eq (par S1 R1) (par (par T R1) Q)

Subgoal 3.2 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < split.

Subgoal 3.1.1:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor P Q1 T
H5 : str_eq S1 (par T Q)
============================
red_ker_tensor P (par Q1 R1) (par T R1)

Subgoal 3.1.2 is:
str_eq (par S1 R1) (par (par T R1) Q)

Subgoal 3.2 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < search.

Subgoal 3.1.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor P Q1 T
H5 : str_eq S1 (par T Q)
============================
str_eq (par S1 R1) (par (par T R1) Q)

Subgoal 3.2 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < unfold 20.

Subgoal 3.1.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor P Q1 T
H5 : str_eq S1 (par T Q)
============================
exists Q1, str_eq (par S1 R1) Q1 /\ str_eq Q1 (par (par T R1) Q)

Subgoal 3.2 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < exists par (par R1 T) Q.

Subgoal 3.1.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor P Q1 T
H5 : str_eq S1 (par T Q)
============================
str_eq (par S1 R1) (par (par R1 T) Q) /\
str_eq (par (par R1 T) Q) (par (par T R1) Q)

Subgoal 3.2 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < search.

Subgoal 3.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor Q Q1 T
H5 : str_eq S1 (par P T)
============================
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < right.

Subgoal 3.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor Q Q1 T
H5 : str_eq S1 (par P T)
============================
exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T)

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < exists par T R1.

Subgoal 3.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor Q Q1 T
H5 : str_eq S1 (par P T)
============================
red_ker_tensor Q (par Q1 R1) (par T R1) /\
str_eq (par S1 R1) (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < split.

Subgoal 3.2.1:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor Q Q1 T
H5 : str_eq S1 (par P T)
============================
red_ker_tensor Q (par Q1 R1) (par T R1)

Subgoal 3.2.2 is:
str_eq (par S1 R1) (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < search.

Subgoal 3.2.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor Q Q1 T
H5 : str_eq S1 (par P T)
============================
str_eq (par S1 R1) (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < unfold 20.

Subgoal 3.2.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor Q Q1 T
H5 : str_eq S1 (par P T)
============================
exists Q, str_eq (par S1 R1) Q /\ str_eq Q (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < exists par (par T R1) P.

Subgoal 3.2.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor Q Q1 T
H5 : str_eq S1 (par P T)
============================
str_eq (par S1 R1) (par (par T R1) P) /\
str_eq (par (par T R1) P) (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < split.

Subgoal 3.2.2.1:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor Q Q1 T
H5 : str_eq S1 (par P T)
============================
str_eq (par S1 R1) (par (par T R1) P)

Subgoal 3.2.2.2 is:
str_eq (par (par T R1) P) (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < search.

Subgoal 3.2.2.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor Q Q1 T
H5 : str_eq S1 (par P T)
============================
str_eq (par (par T R1) P) (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < unfold 20.

Subgoal 3.2.2.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor Q Q1 T
H5 : str_eq S1 (par P T)
============================
exists Q, str_eq (par (par T R1) P) Q /\ str_eq Q (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < exists par (par P T) R1.

Subgoal 3.2.2.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) Q1 S1 *
H4 : red_ker_tensor Q Q1 T
H5 : str_eq S1 (par P T)
============================
str_eq (par (par T R1) P) (par (par P T) R1) /\
str_eq (par (par P T) R1) (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < search.

Subgoal 4:

Variables: P Q S1 Q1 R1
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) R1 S1 *
============================
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < apply IH to H2.

Subgoal 4:

Variables: P Q S1 Q1 R1
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) R1 S1 *
H3 : (exists T, red_ker_tensor P R1 T /\ str_eq S1 (par T Q)) \/
(exists T, red_ker_tensor Q R1 T /\ str_eq S1 (par P T))
============================
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < case H3.

Subgoal 4.1:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) R1 S1 *
H4 : red_ker_tensor P R1 T
H5 : str_eq S1 (par T Q)
============================
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 4.2 is:
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < search.

Subgoal 4.2:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) R1 S1 *
H4 : red_ker_tensor Q R1 T
H5 : str_eq S1 (par P T)
============================
(exists T, red_ker_tensor P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < right.

Subgoal 4.2:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) R1 S1 *
H4 : red_ker_tensor Q R1 T
H5 : str_eq S1 (par P T)
============================
exists T, red_ker_tensor Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T)

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < exists par Q1 T.

Subgoal 4.2:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) R1 S1 *
H4 : red_ker_tensor Q R1 T
H5 : str_eq S1 (par P T)
============================
red_ker_tensor Q (par Q1 R1) (par Q1 T) /\
str_eq (par Q1 S1) (par P (par Q1 T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < split.

Subgoal 4.2.1:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) R1 S1 *
H4 : red_ker_tensor Q R1 T
H5 : str_eq S1 (par P T)
============================
red_ker_tensor Q (par Q1 R1) (par Q1 T)

Subgoal 4.2.2 is:
str_eq (par Q1 S1) (par P (par Q1 T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < search.

Subgoal 4.2.2:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) R1 S1 *
H4 : red_ker_tensor Q R1 T
H5 : str_eq S1 (par P T)
============================
str_eq (par Q1 S1) (par P (par Q1 T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < unfold 20.

Subgoal 4.2.2:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) R1 S1 *
H4 : red_ker_tensor Q R1 T
H5 : str_eq S1 (par P T)
============================
exists Q, str_eq (par Q1 S1) Q /\ str_eq Q (par P (par Q1 T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < exists par Q1 (par P T).

Subgoal 4.2.2:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) R1 S1 *
H4 : red_ker_tensor Q R1 T
H5 : str_eq S1 (par P T)
============================
str_eq (par Q1 S1) (par Q1 (par P T)) /\
str_eq (par Q1 (par P T)) (par P (par Q1 T))

Subgoal 5 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < search.

Subgoal 5:

Variables: P Q R1 Q1
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) (Q1 n1) (R1 n1) *
============================
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < apply IH to H2.

Subgoal 5:

Variables: P Q R1 Q1
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) (Q1 n1) (R1 n1) *
H3 : (exists T, red_ker_tensor P (Q1 n1) T /\ str_eq (R1 n1) (par T Q)) \/
(exists T, red_ker_tensor Q (Q1 n1) T /\ str_eq (R1 n1) (par P T))
============================
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < case H3.

Subgoal 5.1:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_tensor P (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par (T n1) Q)
============================
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

Subgoal 5.2 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < left.

Subgoal 5.1:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_tensor P (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par (T n1) Q)
============================
exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)

Subgoal 5.2 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < exists nu T.

Subgoal 5.1:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_tensor P (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par (T n1) Q)
============================
red_ker_tensor P (nu Q1) (nu T) /\ str_eq (nu R1) (par (nu T) Q)

Subgoal 5.2 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < split.

Subgoal 5.1.1:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_tensor P (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par (T n1) Q)
============================
red_ker_tensor P (nu Q1) (nu T)

Subgoal 5.1.2 is:
str_eq (nu R1) (par (nu T) Q)

Subgoal 5.2 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < search.

Subgoal 5.1.2:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_tensor P (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par (T n1) Q)
============================
str_eq (nu R1) (par (nu T) Q)

Subgoal 5.2 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < unfold 20.

Subgoal 5.1.2:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_tensor P (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par (T n1) Q)
============================
exists Q1, str_eq (nu R1) Q1 /\ str_eq Q1 (par (nu T) Q)

Subgoal 5.2 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < exists nu (x\par (T x) Q).

Subgoal 5.1.2:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_tensor P (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par (T n1) Q)
============================
str_eq (nu R1) (nu (x\par (T x) Q)) /\
str_eq (nu (x\par (T x) Q)) (par (nu T) Q)

Subgoal 5.2 is:
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < search.

Subgoal 5.2:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_tensor (par P Q) R S * ->
(exists T, red_ker_tensor P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_tensor Q R T /\ str_eq S (par P T))
H2 : red_ker_tensor (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_tensor Q (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par P (T n1))
============================
(exists T, red_ker_tensor P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_tensor Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_tensor_par_cases < search.
Proof completed.

Abella < Theorem red_ker_exp_par_cases :
forall P Q R S, red_ker_exp (par P Q) R S ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T)).



============================
forall P Q R S, red_ker_exp (par P Q) R S ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))

red_ker_exp_par_cases < induction on 1.


IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
============================
forall P Q R S, red_ker_exp (par P Q) R S @ ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))

red_ker_exp_par_cases < intros.


Variables: P Q R S
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H1 : red_ker_exp (par P Q) R S @
============================
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))

red_ker_exp_par_cases < case H1.

Subgoal 1:

Variables: P Q R S1
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp P R S1 *
============================
(exists T, red_ker_exp P R T /\ str_eq (par S1 Q) (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq (par S1 Q) (par P T))

Subgoal 2 is:
(exists T, red_ker_exp P R T /\ str_eq (par P S1) (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq (par P S1) (par P T))

Subgoal 3 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < search.

Subgoal 2:

Variables: P Q R S1
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp Q R S1 *
============================
(exists T, red_ker_exp P R T /\ str_eq (par P S1) (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq (par P S1) (par P T))

Subgoal 3 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < search.

Subgoal 3:

Variables: P Q R1 S1 Q1
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
============================
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < apply IH to H2.

Subgoal 3:

Variables: P Q R1 S1 Q1
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H3 : (exists T, red_ker_exp P Q1 T /\ str_eq S1 (par T Q)) \/
(exists T, red_ker_exp Q Q1 T /\ str_eq S1 (par P T))
============================
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < case H3.

Subgoal 3.1:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp P Q1 T
H5 : str_eq S1 (par T Q)
============================
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 3.2 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < left.

Subgoal 3.1:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp P Q1 T
H5 : str_eq S1 (par T Q)
============================
exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)

Subgoal 3.2 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < exists par T R1.

Subgoal 3.1:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp P Q1 T
H5 : str_eq S1 (par T Q)
============================
red_ker_exp P (par Q1 R1) (par T R1) /\
str_eq (par S1 R1) (par (par T R1) Q)

Subgoal 3.2 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < split.

Subgoal 3.1.1:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp P Q1 T
H5 : str_eq S1 (par T Q)
============================
red_ker_exp P (par Q1 R1) (par T R1)

Subgoal 3.1.2 is:
str_eq (par S1 R1) (par (par T R1) Q)

Subgoal 3.2 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < search.

Subgoal 3.1.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp P Q1 T
H5 : str_eq S1 (par T Q)
============================
str_eq (par S1 R1) (par (par T R1) Q)

Subgoal 3.2 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < unfold 20.

Subgoal 3.1.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp P Q1 T
H5 : str_eq S1 (par T Q)
============================
exists Q1, str_eq (par S1 R1) Q1 /\ str_eq Q1 (par (par T R1) Q)

Subgoal 3.2 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < exists par (par R1 T) Q.

Subgoal 3.1.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp P Q1 T
H5 : str_eq S1 (par T Q)
============================
str_eq (par S1 R1) (par (par R1 T) Q) /\
str_eq (par (par R1 T) Q) (par (par T R1) Q)

Subgoal 3.2 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < search.

Subgoal 3.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp Q Q1 T
H5 : str_eq S1 (par P T)
============================
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par S1 R1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < right.

Subgoal 3.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp Q Q1 T
H5 : str_eq S1 (par P T)
============================
exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par S1 R1) (par P T)

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < exists par T R1.

Subgoal 3.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp Q Q1 T
H5 : str_eq S1 (par P T)
============================
red_ker_exp Q (par Q1 R1) (par T R1) /\
str_eq (par S1 R1) (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < split.

Subgoal 3.2.1:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp Q Q1 T
H5 : str_eq S1 (par P T)
============================
red_ker_exp Q (par Q1 R1) (par T R1)

Subgoal 3.2.2 is:
str_eq (par S1 R1) (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < search.

Subgoal 3.2.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp Q Q1 T
H5 : str_eq S1 (par P T)
============================
str_eq (par S1 R1) (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < unfold 20.

Subgoal 3.2.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp Q Q1 T
H5 : str_eq S1 (par P T)
============================
exists Q, str_eq (par S1 R1) Q /\ str_eq Q (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < exists par (par T R1) P.

Subgoal 3.2.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp Q Q1 T
H5 : str_eq S1 (par P T)
============================
str_eq (par S1 R1) (par (par T R1) P) /\
str_eq (par (par T R1) P) (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < split.

Subgoal 3.2.2.1:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp Q Q1 T
H5 : str_eq S1 (par P T)
============================
str_eq (par S1 R1) (par (par T R1) P)

Subgoal 3.2.2.2 is:
str_eq (par (par T R1) P) (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < search.

Subgoal 3.2.2.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp Q Q1 T
H5 : str_eq S1 (par P T)
============================
str_eq (par (par T R1) P) (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < unfold 20.

Subgoal 3.2.2.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp Q Q1 T
H5 : str_eq S1 (par P T)
============================
exists Q, str_eq (par (par T R1) P) Q /\ str_eq Q (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < exists par (par P T) R1.

Subgoal 3.2.2.2:

Variables: P Q R1 S1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) Q1 S1 *
H4 : red_ker_exp Q Q1 T
H5 : str_eq S1 (par P T)
============================
str_eq (par (par T R1) P) (par (par P T) R1) /\
str_eq (par (par P T) R1) (par P (par T R1))

Subgoal 4 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < search.

Subgoal 4:

Variables: P Q S1 Q1 R1
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) R1 S1 *
============================
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < apply IH to H2.

Subgoal 4:

Variables: P Q S1 Q1 R1
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) R1 S1 *
H3 : (exists T, red_ker_exp P R1 T /\ str_eq S1 (par T Q)) \/
(exists T, red_ker_exp Q R1 T /\ str_eq S1 (par P T))
============================
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < case H3.

Subgoal 4.1:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) R1 S1 *
H4 : red_ker_exp P R1 T
H5 : str_eq S1 (par T Q)
============================
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 4.2 is:
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < search.

Subgoal 4.2:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) R1 S1 *
H4 : red_ker_exp Q R1 T
H5 : str_eq S1 (par P T)
============================
(exists T, red_ker_exp P (par Q1 R1) T /\ str_eq (par Q1 S1) (par T Q)) \/
(exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < right.

Subgoal 4.2:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) R1 S1 *
H4 : red_ker_exp Q R1 T
H5 : str_eq S1 (par P T)
============================
exists T, red_ker_exp Q (par Q1 R1) T /\ str_eq (par Q1 S1) (par P T)

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < exists par Q1 T.

Subgoal 4.2:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) R1 S1 *
H4 : red_ker_exp Q R1 T
H5 : str_eq S1 (par P T)
============================
red_ker_exp Q (par Q1 R1) (par Q1 T) /\
str_eq (par Q1 S1) (par P (par Q1 T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < split.

Subgoal 4.2.1:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) R1 S1 *
H4 : red_ker_exp Q R1 T
H5 : str_eq S1 (par P T)
============================
red_ker_exp Q (par Q1 R1) (par Q1 T)

Subgoal 4.2.2 is:
str_eq (par Q1 S1) (par P (par Q1 T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < search.

Subgoal 4.2.2:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) R1 S1 *
H4 : red_ker_exp Q R1 T
H5 : str_eq S1 (par P T)
============================
str_eq (par Q1 S1) (par P (par Q1 T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < unfold 20.

Subgoal 4.2.2:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) R1 S1 *
H4 : red_ker_exp Q R1 T
H5 : str_eq S1 (par P T)
============================
exists Q, str_eq (par Q1 S1) Q /\ str_eq Q (par P (par Q1 T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < exists par Q1 (par P T).

Subgoal 4.2.2:

Variables: P Q S1 Q1 R1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) R1 S1 *
H4 : red_ker_exp Q R1 T
H5 : str_eq S1 (par P T)
============================
str_eq (par Q1 S1) (par Q1 (par P T)) /\
str_eq (par Q1 (par P T)) (par P (par Q1 T))

Subgoal 5 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < search.

Subgoal 5:

Variables: P Q R1 Q1
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) (Q1 n1) (R1 n1) *
============================
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < apply IH to H2.

Subgoal 5:

Variables: P Q R1 Q1
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) (Q1 n1) (R1 n1) *
H3 : (exists T, red_ker_exp P (Q1 n1) T /\ str_eq (R1 n1) (par T Q)) \/
(exists T, red_ker_exp Q (Q1 n1) T /\ str_eq (R1 n1) (par P T))
============================
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < case H3.

Subgoal 5.1:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_exp P (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par (T n1) Q)
============================
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

Subgoal 5.2 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < left.

Subgoal 5.1:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_exp P (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par (T n1) Q)
============================
exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)

Subgoal 5.2 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < exists nu T.

Subgoal 5.1:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_exp P (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par (T n1) Q)
============================
red_ker_exp P (nu Q1) (nu T) /\ str_eq (nu R1) (par (nu T) Q)

Subgoal 5.2 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < split.

Subgoal 5.1.1:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_exp P (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par (T n1) Q)
============================
red_ker_exp P (nu Q1) (nu T)

Subgoal 5.1.2 is:
str_eq (nu R1) (par (nu T) Q)

Subgoal 5.2 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < search.

Subgoal 5.1.2:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_exp P (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par (T n1) Q)
============================
str_eq (nu R1) (par (nu T) Q)

Subgoal 5.2 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < unfold 20.

Subgoal 5.1.2:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_exp P (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par (T n1) Q)
============================
exists Q1, str_eq (nu R1) Q1 /\ str_eq Q1 (par (nu T) Q)

Subgoal 5.2 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < exists nu (x\par (T x) Q).

Subgoal 5.1.2:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_exp P (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par (T n1) Q)
============================
str_eq (nu R1) (nu (x\par (T x) Q)) /\
str_eq (nu (x\par (T x) Q)) (par (nu T) Q)

Subgoal 5.2 is:
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < search.

Subgoal 5.2:

Variables: P Q R1 Q1 T
IH : forall P Q R S, red_ker_exp (par P Q) R S * ->
(exists T, red_ker_exp P R T /\ str_eq S (par T Q)) \/
(exists T, red_ker_exp Q R T /\ str_eq S (par P T))
H2 : red_ker_exp (par P Q) (Q1 n1) (R1 n1) *
H4 : red_ker_exp Q (Q1 n1) (T n1)
H5 : str_eq (R1 n1) (par P (T n1))
============================
(exists T, red_ker_exp P (nu Q1) T /\ str_eq (nu R1) (par T Q)) \/
(exists T, red_ker_exp Q (nu Q1) T /\ str_eq (nu R1) (par P T))

red_ker_exp_par_cases < search.
Proof completed.

Abella < Theorem red_ker_tensor_nu_cases :
forall P Q R, red_ker_tensor (nu P) Q R ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S)).



============================
forall P Q R, red_ker_tensor (nu P) Q R ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))

red_ker_tensor_nu_cases < induction on 1.


IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
============================
forall P Q R, red_ker_tensor (nu P) Q R @ ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))

red_ker_tensor_nu_cases < intros.


Variables: P Q R
IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
H1 : red_ker_tensor (nu P) Q R @
============================
exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S)

red_ker_tensor_nu_cases < case H1.

Subgoal 1:

Variables: P Q R1
IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_tensor (P n1) Q (R1 n1) *
============================
exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq (nu R1) (nu S)

Subgoal 2 is:
exists S1, nabla x, red_ker_tensor (P x) (par Q1 R1) (S1 x) /\
str_eq (par S R1) (nu S1)

Subgoal 3 is:
exists S1, nabla x, red_ker_tensor (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_tensor (P x) (nu Q1) (S x) /\
str_eq (nu R1) (nu S)

red_ker_tensor_nu_cases < search.

Subgoal 2:

Variables: P R1 S Q1
IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_tensor (nu P) Q1 S *
============================
exists S1, nabla x, red_ker_tensor (P x) (par Q1 R1) (S1 x) /\
str_eq (par S R1) (nu S1)

Subgoal 3 is:
exists S1, nabla x, red_ker_tensor (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_tensor (P x) (nu Q1) (S x) /\
str_eq (nu R1) (nu S)

red_ker_tensor_nu_cases < apply IH to H2.

Subgoal 2:

Variables: P R1 S Q1 S1
IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_tensor (nu P) Q1 S *
H3 : red_ker_tensor (P n1) Q1 (S1 n1)
H4 : str_eq S (nu S1)
============================
exists S1, nabla x, red_ker_tensor (P x) (par Q1 R1) (S1 x) /\
str_eq (par S R1) (nu S1)

Subgoal 3 is:
exists S1, nabla x, red_ker_tensor (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_tensor (P x) (nu Q1) (S x) /\
str_eq (nu R1) (nu S)

red_ker_tensor_nu_cases < exists x\par (S1 x) R1.

Subgoal 2:

Variables: P R1 S Q1 S1
IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_tensor (nu P) Q1 S *
H3 : red_ker_tensor (P n1) Q1 (S1 n1)
H4 : str_eq S (nu S1)
============================
nabla x, red_ker_tensor (P x) (par Q1 R1) (par (S1 x) R1) /\
str_eq (par S R1) (nu (x\par (S1 x) R1))

Subgoal 3 is:
exists S1, nabla x, red_ker_tensor (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_tensor (P x) (nu Q1) (S x) /\
str_eq (nu R1) (nu S)

red_ker_tensor_nu_cases < intros.

Subgoal 2:

Variables: P R1 S Q1 S1
IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_tensor (nu P) Q1 S *
H3 : red_ker_tensor (P n1) Q1 (S1 n1)
H4 : str_eq S (nu S1)
============================
red_ker_tensor (P n1) (par Q1 R1) (par (S1 n1) R1) /\
str_eq (par S R1) (nu (x\par (S1 x) R1))

Subgoal 3 is:
exists S1, nabla x, red_ker_tensor (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_tensor (P x) (nu Q1) (S x) /\
str_eq (nu R1) (nu S)

red_ker_tensor_nu_cases < split.

Subgoal 2.1:

Variables: P R1 S Q1 S1
IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_tensor (nu P) Q1 S *
H3 : red_ker_tensor (P n1) Q1 (S1 n1)
H4 : str_eq S (nu S1)
============================
red_ker_tensor (P n1) (par Q1 R1) (par (S1 n1) R1)

Subgoal 2.2 is:
str_eq (par S R1) (nu (x\par (S1 x) R1))

Subgoal 3 is:
exists S1, nabla x, red_ker_tensor (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_tensor (P x) (nu Q1) (S x) /\
str_eq (nu R1) (nu S)

red_ker_tensor_nu_cases < search.

Subgoal 2.2:

Variables: P R1 S Q1 S1
IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_tensor (nu P) Q1 S *
H3 : red_ker_tensor (P n1) Q1 (S1 n1)
H4 : str_eq S (nu S1)
============================
str_eq (par S R1) (nu (x\par (S1 x) R1))

Subgoal 3 is:
exists S1, nabla x, red_ker_tensor (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_tensor (P x) (nu Q1) (S x) /\
str_eq (nu R1) (nu S)

red_ker_tensor_nu_cases < unfold 20.

Subgoal 2.2:

Variables: P R1 S Q1 S1
IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_tensor (nu P) Q1 S *
H3 : red_ker_tensor (P n1) Q1 (S1 n1)
H4 : str_eq S (nu S1)
============================
exists Q, str_eq (par S R1) Q /\ str_eq Q (nu (x\par (S1 x) R1))

Subgoal 3 is:
exists S1, nabla x, red_ker_tensor (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_tensor (P x) (nu Q1) (S x) /\
str_eq (nu R1) (nu S)

red_ker_tensor_nu_cases < exists par (nu S1) R1.

Subgoal 2.2:

Variables: P R1 S Q1 S1
IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_tensor (nu P) Q1 S *
H3 : red_ker_tensor (P n1) Q1 (S1 n1)
H4 : str_eq S (nu S1)
============================
str_eq (par S R1) (par (nu S1) R1) /\
str_eq (par (nu S1) R1) (nu (x\par (S1 x) R1))

Subgoal 3 is:
exists S1, nabla x, red_ker_tensor (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_tensor (P x) (nu Q1) (S x) /\
str_eq (nu R1) (nu S)

red_ker_tensor_nu_cases < search.

Subgoal 3:

Variables: P S Q1 R1
IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_tensor (nu P) R1 S *
============================
exists S1, nabla x, red_ker_tensor (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_tensor (P x) (nu Q1) (S x) /\
str_eq (nu R1) (nu S)

red_ker_tensor_nu_cases < apply IH to H2.

Subgoal 3:

Variables: P S Q1 R1 S1
IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_tensor (nu P) R1 S *
H3 : red_ker_tensor (P n1) R1 (S1 n1)
H4 : str_eq S (nu S1)
============================
exists S1, nabla x, red_ker_tensor (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_tensor (P x) (nu Q1) (S x) /\
str_eq (nu R1) (nu S)

red_ker_tensor_nu_cases < search.

Subgoal 4:

Variables: P R1 Q1
IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_tensor (nu P) (Q1 n1) (R1 n1) *
============================
exists S, nabla x, red_ker_tensor (P x) (nu Q1) (S x) /\
str_eq (nu R1) (nu S)

red_ker_tensor_nu_cases < apply IH to H2.

Subgoal 4:

Variables: P R1 Q1 S
IH : forall P Q R, red_ker_tensor (nu P) Q R * ->
(exists S, nabla x, red_ker_tensor (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_tensor (nu P) (Q1 n1) (R1 n1) *
H3 : red_ker_tensor (P n2) (Q1 n1) (S n1 n2)
H4 : str_eq (R1 n1) (nu (S n1))
============================
exists S, nabla x, red_ker_tensor (P x) (nu Q1) (S x) /\
str_eq (nu R1) (nu S)

red_ker_tensor_nu_cases < search.
Proof completed.

Abella < Theorem red_ker_exp_nu_cases :
forall P Q R, red_ker_exp (nu P) Q R ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S)).



============================
forall P Q R, red_ker_exp (nu P) Q R ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))

red_ker_exp_nu_cases < induction on 1.


IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
============================
forall P Q R, red_ker_exp (nu P) Q R @ ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))

red_ker_exp_nu_cases < intros.


Variables: P Q R
IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
H1 : red_ker_exp (nu P) Q R @
============================
exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S)

red_ker_exp_nu_cases < case H1.

Subgoal 1:

Variables: P Q R1
IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_exp (P n1) Q (R1 n1) *
============================
exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq (nu R1) (nu S)

Subgoal 2 is:
exists S1, nabla x, red_ker_exp (P x) (par Q1 R1) (S1 x) /\
str_eq (par S R1) (nu S1)

Subgoal 3 is:
exists S1, nabla x, red_ker_exp (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_exp (P x) (nu Q1) (S x) /\ str_eq (nu R1) (nu S)

red_ker_exp_nu_cases < search.

Subgoal 2:

Variables: P R1 S Q1
IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_exp (nu P) Q1 S *
============================
exists S1, nabla x, red_ker_exp (P x) (par Q1 R1) (S1 x) /\
str_eq (par S R1) (nu S1)

Subgoal 3 is:
exists S1, nabla x, red_ker_exp (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_exp (P x) (nu Q1) (S x) /\ str_eq (nu R1) (nu S)

red_ker_exp_nu_cases < apply IH to H2.

Subgoal 2:

Variables: P R1 S Q1 S1
IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_exp (nu P) Q1 S *
H3 : red_ker_exp (P n1) Q1 (S1 n1)
H4 : str_eq S (nu S1)
============================
exists S1, nabla x, red_ker_exp (P x) (par Q1 R1) (S1 x) /\
str_eq (par S R1) (nu S1)

Subgoal 3 is:
exists S1, nabla x, red_ker_exp (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_exp (P x) (nu Q1) (S x) /\ str_eq (nu R1) (nu S)

red_ker_exp_nu_cases < exists x\par (S1 x) R1.

Subgoal 2:

Variables: P R1 S Q1 S1
IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_exp (nu P) Q1 S *
H3 : red_ker_exp (P n1) Q1 (S1 n1)
H4 : str_eq S (nu S1)
============================
nabla x, red_ker_exp (P x) (par Q1 R1) (par (S1 x) R1) /\
str_eq (par S R1) (nu (x\par (S1 x) R1))

Subgoal 3 is:
exists S1, nabla x, red_ker_exp (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_exp (P x) (nu Q1) (S x) /\ str_eq (nu R1) (nu S)

red_ker_exp_nu_cases < intros.

Subgoal 2:

Variables: P R1 S Q1 S1
IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_exp (nu P) Q1 S *
H3 : red_ker_exp (P n1) Q1 (S1 n1)
H4 : str_eq S (nu S1)
============================
red_ker_exp (P n1) (par Q1 R1) (par (S1 n1) R1) /\
str_eq (par S R1) (nu (x\par (S1 x) R1))

Subgoal 3 is:
exists S1, nabla x, red_ker_exp (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_exp (P x) (nu Q1) (S x) /\ str_eq (nu R1) (nu S)

red_ker_exp_nu_cases < split.

Subgoal 2.1:

Variables: P R1 S Q1 S1
IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_exp (nu P) Q1 S *
H3 : red_ker_exp (P n1) Q1 (S1 n1)
H4 : str_eq S (nu S1)
============================
red_ker_exp (P n1) (par Q1 R1) (par (S1 n1) R1)

Subgoal 2.2 is:
str_eq (par S R1) (nu (x\par (S1 x) R1))

Subgoal 3 is:
exists S1, nabla x, red_ker_exp (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_exp (P x) (nu Q1) (S x) /\ str_eq (nu R1) (nu S)

red_ker_exp_nu_cases < search.

Subgoal 2.2:

Variables: P R1 S Q1 S1
IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_exp (nu P) Q1 S *
H3 : red_ker_exp (P n1) Q1 (S1 n1)
H4 : str_eq S (nu S1)
============================
str_eq (par S R1) (nu (x\par (S1 x) R1))

Subgoal 3 is:
exists S1, nabla x, red_ker_exp (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_exp (P x) (nu Q1) (S x) /\ str_eq (nu R1) (nu S)

red_ker_exp_nu_cases < unfold 20.

Subgoal 2.2:

Variables: P R1 S Q1 S1
IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_exp (nu P) Q1 S *
H3 : red_ker_exp (P n1) Q1 (S1 n1)
H4 : str_eq S (nu S1)
============================
exists Q, str_eq (par S R1) Q /\ str_eq Q (nu (x\par (S1 x) R1))

Subgoal 3 is:
exists S1, nabla x, red_ker_exp (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_exp (P x) (nu Q1) (S x) /\ str_eq (nu R1) (nu S)

red_ker_exp_nu_cases < exists par (nu S1) R1.

Subgoal 2.2:

Variables: P R1 S Q1 S1
IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_exp (nu P) Q1 S *
H3 : red_ker_exp (P n1) Q1 (S1 n1)
H4 : str_eq S (nu S1)
============================
str_eq (par S R1) (par (nu S1) R1) /\
str_eq (par (nu S1) R1) (nu (x\par (S1 x) R1))

Subgoal 3 is:
exists S1, nabla x, red_ker_exp (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_exp (P x) (nu Q1) (S x) /\ str_eq (nu R1) (nu S)

red_ker_exp_nu_cases < search.

Subgoal 3:

Variables: P S Q1 R1
IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_exp (nu P) R1 S *
============================
exists S1, nabla x, red_ker_exp (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_exp (P x) (nu Q1) (S x) /\ str_eq (nu R1) (nu S)

red_ker_exp_nu_cases < apply IH to H2.

Subgoal 3:

Variables: P S Q1 R1 S1
IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_exp (nu P) R1 S *
H3 : red_ker_exp (P n1) R1 (S1 n1)
H4 : str_eq S (nu S1)
============================
exists S1, nabla x, red_ker_exp (P x) (par Q1 R1) (S1 x) /\
str_eq (par Q1 S) (nu S1)

Subgoal 4 is:
exists S, nabla x, red_ker_exp (P x) (nu Q1) (S x) /\ str_eq (nu R1) (nu S)

red_ker_exp_nu_cases < search.

Subgoal 4:

Variables: P R1 Q1
IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_exp (nu P) (Q1 n1) (R1 n1) *
============================
exists S, nabla x, red_ker_exp (P x) (nu Q1) (S x) /\ str_eq (nu R1) (nu S)

red_ker_exp_nu_cases < apply IH to H2.

Subgoal 4:

Variables: P R1 Q1 S
IH : forall P Q R, red_ker_exp (nu P) Q R * ->
(exists S, nabla x, red_ker_exp (P x) Q (S x) /\ str_eq R (nu S))
H2 : red_ker_exp (nu P) (Q1 n1) (R1 n1) *
H3 : red_ker_exp (P n2) (Q1 n1) (S n1 n2)
H4 : str_eq (R1 n1) (nu (S n1))
============================
exists S, nabla x, red_ker_exp (P x) (nu Q1) (S x) /\ str_eq (nu R1) (nu S)

red_ker_exp_nu_cases < search.
Proof completed.

Abella < Theorem red_ker_tensor_out2_no_com_case :
forall P Q, nabla a b c, red_ker_tensor (out2 a b c) (P b c) (Q a b c) ->
false.



============================
forall P Q, nabla a b c, red_ker_tensor (out2 a b c) (P b c) (Q a b c) ->
false

red_ker_tensor_out2_no_com_case < induction on 1.


IH : forall P Q, nabla a b c, red_ker_tensor (out2 a b c) (P b c) (Q a b c) * ->
false
============================
forall P Q, nabla a b c, red_ker_tensor (out2 a b c) (P b c) (Q a b c) @ ->
false

red_ker_tensor_out2_no_com_case < intros.


Variables: P Q
IH : forall P Q, nabla a b c, red_ker_tensor (out2 a b c) (P b c) (Q a b c) * ->
false
H1 : red_ker_tensor (out2 n1 n2 n3) (P n2 n3) (Q n1 n2 n3) @
============================
false

red_ker_tensor_out2_no_com_case < case H1.

Subgoal 1:

Variables: P3 S P2
IH : forall P Q, nabla a b c, red_ker_tensor (out2 a b c) (P b c) (Q a b c) * ->
false
H2 : red_ker_tensor (out2 n1 n2 n3) (P2 n3 n2) (S n3 n2 n1) *
============================
false

Subgoal 2 is:
false

Subgoal 3 is:
false

red_ker_tensor_out2_no_com_case < apply IH to H2.

Subgoal 2:

Variables: S P2 P3
IH : forall P Q, nabla a b c, red_ker_tensor (out2 a b c) (P b c) (Q a b c) * ->
false
H2 : red_ker_tensor (out2 n1 n2 n3) (P3 n3 n2) (S n3 n2 n1) *
============================
false

Subgoal 3 is:
false

red_ker_tensor_out2_no_com_case < apply IH to H2.

Subgoal 3:

Variables: R P2
IH : forall P Q, nabla a b c, red_ker_tensor (out2 a b c) (P b c) (Q a b c) * ->
false
H2 : red_ker_tensor (out2 n1 n2 n3) (P2 n3 n2 n4) (R n3 n2 n1 n4) *
============================
false

red_ker_tensor_out2_no_com_case < apply IH to H2.
Proof completed.

Abella < Theorem red_ker_exp_out2_case :
forall P Q, nabla a b c, red_ker_exp (out2 a b c) (P a b c) (Q a b c) ->
false.



============================
forall P Q, nabla a b c, red_ker_exp (out2 a b c) (P a b c) (Q a b c) ->
false

red_ker_exp_out2_case < induction on 1.


IH : forall P Q, nabla a b c, red_ker_exp (out2 a b c) (P a b c) (Q a b c) * ->
false
============================
forall P Q, nabla a b c, red_ker_exp (out2 a b c) (P a b c) (Q a b c) @ ->
false

red_ker_exp_out2_case < intros.


Variables: P Q
IH : forall P Q, nabla a b c, red_ker_exp (out2 a b c) (P a b c) (Q a b c) * ->
false
H1 : red_ker_exp (out2 n1 n2 n3) (P n1 n2 n3) (Q n1 n2 n3) @
============================
false

red_ker_exp_out2_case < case H1.

Subgoal 1:

Variables: R S Q1
IH : forall P Q, nabla a b c, red_ker_exp (out2 a b c) (P a b c) (Q a b c) * ->
false
H2 : red_ker_exp (out2 n1 n2 n3) (Q1 n3 n2 n1) (S n3 n2 n1) *
============================
false

Subgoal 2 is:
false

Subgoal 3 is:
false

red_ker_exp_out2_case < apply IH to H2.

Subgoal 2:

Variables: S Q1 R
IH : forall P Q, nabla a b c, red_ker_exp (out2 a b c) (P a b c) (Q a b c) * ->
false
H2 : red_ker_exp (out2 n1 n2 n3) (R n3 n2 n1) (S n3 n2 n1) *
============================
false

Subgoal 3 is:
false

red_ker_exp_out2_case < apply IH to H2.

Subgoal 3:

Variables: R Q1
IH : forall P Q, nabla a b c, red_ker_exp (out2 a b c) (P a b c) (Q a b c) * ->
false
H2 : red_ker_exp (out2 n1 n2 n3) (Q1 n3 n2 n1 n4) (R n3 n2 n1 n4) *
============================
false

red_ker_exp_out2_case < apply IH to H2.
Proof completed.

Abella < Theorem red_ker_exp_in2_case :
forall P Q R, nabla a, red_ker_exp (in2 a (P a)) (Q a) (R a) -> false.



============================
forall P Q R, nabla a, red_ker_exp (in2 a (P a)) (Q a) (R a) -> false

red_ker_exp_in2_case < induction on 1.


IH : forall P Q R, nabla a, red_ker_exp (in2 a (P a)) (Q a) (R a) * -> false
============================
forall P Q R, nabla a, red_ker_exp (in2 a (P a)) (Q a) (R a) @ -> false

red_ker_exp_in2_case < intros.


Variables: P Q R
IH : forall P Q R, nabla a, red_ker_exp (in2 a (P a)) (Q a) (R a) * -> false
H1 : red_ker_exp (in2 n1 (P n1)) (Q n1) (R n1) @
============================
false

red_ker_exp_in2_case < case H1.

Subgoal 1:

Variables: P R1 S Q1
IH : forall P Q R, nabla a, red_ker_exp (in2 a (P a)) (Q a) (R a) * -> false
H2 : red_ker_exp (in2 n1 (P n1)) (Q1 n1) (S n1) *
============================
false

Subgoal 2 is:
false

Subgoal 3 is:
false

red_ker_exp_in2_case < apply IH to H2.

Subgoal 2:

Variables: P S Q1 R1
IH : forall P Q R, nabla a, red_ker_exp (in2 a (P a)) (Q a) (R a) * -> false
H2 : red_ker_exp (in2 n1 (P n1)) (R1 n1) (S n1) *
============================
false

Subgoal 3 is:
false

red_ker_exp_in2_case < apply IH to H2.

Subgoal 3:

Variables: P R1 Q1
IH : forall P Q R, nabla a, red_ker_exp (in2 a (P a)) (Q a) (R a) * -> false
H2 : red_ker_exp (in2 n1 (P n1)) (Q1 n1 n2) (R1 n1 n2) *
============================
false

red_ker_exp_in2_case < apply IH to H2.
Proof completed.

Abella < Theorem red_ker_exp_in_no_com_case :
forall P Q R, nabla a, red_ker_exp (in a (P a)) Q (R a) -> false.



============================
forall P Q R, nabla a, red_ker_exp (in a (P a)) Q (R a) -> false

red_ker_exp_in_no_com_case < induction on 1.


IH : forall P Q R, nabla a, red_ker_exp (in a (P a)) Q (R a) * -> false
============================
forall P Q R, nabla a, red_ker_exp (in a (P a)) Q (R a) @ -> false

red_ker_exp_in_no_com_case < intros.


Variables: P Q R
IH : forall P Q R, nabla a, red_ker_exp (in a (P a)) Q (R a) * -> false
H1 : red_ker_exp (in n1 (P n1)) Q (R n1) @
============================
false

red_ker_exp_in_no_com_case < case H1.

Subgoal 1:

Variables: P Q3 S Q2
IH : forall P Q R, nabla a, red_ker_exp (in a (P a)) Q (R a) * -> false
H2 : red_ker_exp (in n1 (P n1)) Q2 (S n1) *
============================
false

Subgoal 2 is:
false

Subgoal 3 is:
false

red_ker_exp_in_no_com_case < apply IH to H2.

Subgoal 2:

Variables: P S Q2 Q3
IH : forall P Q R, nabla a, red_ker_exp (in a (P a)) Q (R a) * -> false
H2 : red_ker_exp (in n1 (P n1)) Q3 (S n1) *
============================
false

Subgoal 3 is:
false

red_ker_exp_in_no_com_case < apply IH to H2.

Subgoal 3:

Variables: P R1 Q2
IH : forall P Q R, nabla a, red_ker_exp (in a (P a)) Q (R a) * -> false
H2 : red_ker_exp (in n1 (P n1)) (Q2 n2) (R1 n1 n2) *
============================
false

red_ker_exp_in_no_com_case < apply IH to H2.
Proof completed.

Abella < Theorem red_ker_tensor_in_case :
forall P Q R, nabla a, red_ker_tensor (in a (P a)) (Q a) (R a) -> false.



============================
forall P Q R, nabla a, red_ker_tensor (in a (P a)) (Q a) (R a) -> false

red_ker_tensor_in_case < induction on 1.


IH : forall P Q R, nabla a, red_ker_tensor (in a (P a)) (Q a) (R a) * ->
false
============================
forall P Q R, nabla a, red_ker_tensor (in a (P a)) (Q a) (R a) @ -> false

red_ker_tensor_in_case < intros.


Variables: P Q R
IH : forall P Q R, nabla a, red_ker_tensor (in a (P a)) (Q a) (R a) * ->
false
H1 : red_ker_tensor (in n1 (P n1)) (Q n1) (R n1) @
============================
false

red_ker_tensor_in_case < case H1.

Subgoal 1:

Variables: P R1 S Q1
IH : forall P Q R, nabla a, red_ker_tensor (in a (P a)) (Q a) (R a) * ->
false
H2 : red_ker_tensor (in n1 (P n1)) (Q1 n1) (S n1) *
============================
false

Subgoal 2 is:
false

Subgoal 3 is:
false

red_ker_tensor_in_case < apply IH to H2.

Subgoal 2:

Variables: P S Q1 R1
IH : forall P Q R, nabla a, red_ker_tensor (in a (P a)) (Q a) (R a) * ->
false
H2 : red_ker_tensor (in n1 (P n1)) (R1 n1) (S n1) *
============================
false

Subgoal 3 is:
false

red_ker_tensor_in_case < apply IH to H2.

Subgoal 3:

Variables: P R1 Q1
IH : forall P Q R, nabla a, red_ker_tensor (in a (P a)) (Q a) (R a) * ->
false
H2 : red_ker_tensor (in n1 (P n1)) (Q1 n1 n2) (R1 n1 n2) *
============================
false

red_ker_tensor_in_case < apply IH to H2.
Proof completed.

Abella <