(* ------------------------------------------------------------------------- *)
(*      1- la formalizzazione del calcolo ed alcune proprietà di base        *)
(*      2- la dimostrazione dei lemmi di supporto alla dimostrazione finale  *)
(*  ->  3- la dimostrazione conclusiva di un lemma interessante              *)
(* ------------------------------------------------------------------------- *)

needs "/home/stefano/Desktop/GCS/lemma setup.ml";;

(* ------------------------------------------------------------------------- *)
(* Si vuol dimostrare che se uno termine p congruente ad un termine q può    *)
(* fare un'azione l ed andare in un termine p', allora anche q può fare una  *)
(* azione l' congruente ad l ed andare in uno stato q' congruente a p'.      *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* La dimostrazione procede per analisi dei casi sulla congruenza rafforzata *)
(* e, dove necessario, per analisi dei casi della riduzione.                 *)
(* ------------------------------------------------------------------------- *)

g `!p p' q l. REDUCTION p l p' /\ p CONGRUENCE q ==> (?l' q'. REDUCTION q l' q' /\ p' CONGRUENCE q' /\ l LABEL_CONGRUENCE l')`;;
e (SUBGOAL_THEN `!p q . p CONGRUENCE q ==> (!p' l. REDUCTION p l p' ==> (?l' q'. REDUCTION q l' q' /\ p' CONGRUENCE q' /\ l LABEL_CONGRUENCE l'))`
     (fun th -> MESON_TAC[th]));;
e (MATCH_MP_TAC CONGRUENCE_INDUCT_STRONG);;
e (REPEAT CONJ_TAC);;
(*Caso Congruence Trans*)
e (MESON_TAC[CONGRUENCE_TRANS; LABEL_CONGRUENCE_TRANS]);;
(*Caso Nil*)
e (REWRITE_TAC[NOT_REDUCTION_NIL]);;
(*Caso Var a*)
e (REWRITE_TAC[NOT_REDUCTION_VAR]);;
(*Caso Send*)
e (REPEAT STRIP_TAC);;
e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"]);;
e (STRIP_TAC);;
e (POP_ASSUM SUBST_ALL_TAC);;
e (POP_ASSUM SUBST_ALL_TAC);;
e (POP_ASSUM SUBST_ALL_TAC);;
e (POP_ASSUM SUBST_ALL_TAC);;
e (EXISTS_TAC `Out c' q`);;
e (EXISTS_TAC `Nil`);;
e (REWRITE_TAC [CONGRUENCE_REFL; REDUCTION_SEND]);;
e (MATCH_MP_TAC LABEL_CONGRUENCE_OUT);;
e (ASM_REWRITE_TAC[]);;
(*Caso Recv*)
e (REPEAT STRIP_TAC);;
e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"]);;
e (STRIP_TAC);;
e (POP_ASSUM SUBST_ALL_TAC);;
e (POP_ASSUM SUBST_ALL_TAC);;
e (POP_ASSUM SUBST_ALL_TAC);;
e (EXISTS_TAC `In c'`);;
e (EXISTS_TAC `q:hocore`);;
e (ASM_REWRITE_TAC [LABEL_CONGRUENCE_REFL; REDUCTION_RECV]);;
(*Caso Parallel*)
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (X_GEN_TAC `r:hocore`);;
e (GEN_TAC);;
e (STRIP_TAC);;
e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"]);;
e (STRIP_TAC);;
	(*1*)	
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_ASSUM (fun hp2 -> FIRST_X_ASSUM (fun hp1 -> STRIP_ASSUME_TAC (MATCH_MP hp1 hp2))));;
	e (EXISTS_TAC `Tau`);;
	e (EXISTS_TAC `q'' || q'`);;
	e (REWRITE_TAC[LABEL_CONGRUENCE_REFL]);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_TAU);;
	e (POP_ASSUM (MP_TAC o GEN_REWRITE_RULE I [LABEL_CONGRUENCE_CASES]));;
	e (REWRITE_TAC[distinctness "label"; injectivity "label"]);;
	e (DISCH_THEN SUBST_ALL_TAC);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_PARALLEL);;
	e (ASM_REWRITE_TAC[]);;
	(*2*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_ASSUM (fun hp2 -> FIRST_X_ASSUM (fun hp1 -> STRIP_ASSUME_TAC (MATCH_MP hp1 hp2))));;
	e (EXISTS_TAC `Tau`);;
	e (EXISTS_TAC `p' || q''`);;
	e (REWRITE_TAC[LABEL_CONGRUENCE_REFL]);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_TAU);;
	e (POP_ASSUM (MP_TAC o GEN_REWRITE_RULE I [LABEL_CONGRUENCE_CASES]));;
	e (REWRITE_TAC[distinctness "label"; injectivity "label"]);;
	e (DISCH_THEN SUBST_ALL_TAC);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_PARALLEL);;
	e (ASM_REWRITE_TAC[]);;
	(*3*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_ASSUM (fun hp2 -> FIRST_X_ASSUM (fun hp1 -> STRIP_ASSUME_TAC (MATCH_MP hp1 hp2))));;
	e (EXISTS_TAC `l':label`);;
	e (POP_ASSUM (MP_TAC o GEN_REWRITE_RULE I [LABEL_CONGRUENCE_CASES]));;
	e (REWRITE_TAC[distinctness "label"; injectivity "label"]);;
	e (STRIP_TAC);;
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (ASM_SIMP_TAC[LABEL_CONGRUENCE_RULES]);;
	e (EXISTS_TAC `q'' || q'`);;
	e (ASM_SIMP_TAC[CONGRUENCE_RULES]);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_OUT);;
	e (ASM_REWRITE_TAC[]);;
	(*4*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_ASSUM (fun hp2 -> FIRST_X_ASSUM (fun hp1 -> STRIP_ASSUME_TAC (MATCH_MP hp1 hp2))));;
	e (EXISTS_TAC `l':label`);;
	e (POP_ASSUM (MP_TAC o GEN_REWRITE_RULE I [LABEL_CONGRUENCE_CASES]));;
	e (REWRITE_TAC[distinctness "label"; injectivity "label"]);;
	e (STRIP_TAC);;
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (ASM_SIMP_TAC[LABEL_CONGRUENCE_RULES]);;
	e (EXISTS_TAC `p' || q''`);;
	e (ASM_SIMP_TAC[CONGRUENCE_RULES]);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_OUT);;
	e (ASM_REWRITE_TAC[]);;
	(*5*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_ASSUM (fun hp2 -> FIRST_X_ASSUM (fun hp1 -> STRIP_ASSUME_TAC (MATCH_MP hp1 hp2))));;
	e (EXISTS_TAC `l':label`);;
	e (POP_ASSUM (MP_TAC o GEN_REWRITE_RULE I [LABEL_CONGRUENCE_CASES]));;
	e (REWRITE_TAC[distinctness "label"; injectivity "label"]);;
	e (STRIP_TAC);;
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (ASM_SIMP_TAC[LABEL_CONGRUENCE_RULES]);;
	e (EXISTS_TAC `q'' || BUMP q'`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_IN);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_PARALLEL);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC BUMP_CONGRUENCE);;
	e (ASM_REWRITE_TAC[]);;
	(*6*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_ASSUM (fun hp2 -> FIRST_X_ASSUM (fun hp1 -> STRIP_ASSUME_TAC (MATCH_MP hp1 hp2))));;
	e (EXISTS_TAC `l':label`);;
	e (POP_ASSUM (MP_TAC o GEN_REWRITE_RULE I [LABEL_CONGRUENCE_CASES]));;
	e (REWRITE_TAC[distinctness "label"; injectivity "label"]);;
	e (STRIP_TAC);;
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (ASM_SIMP_TAC[LABEL_CONGRUENCE_RULES]);;
	e (EXISTS_TAC `BUMP p' || q''`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_IN);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_PARALLEL);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC BUMP_CONGRUENCE);;
	e (ASM_REWRITE_TAC[]);;
	(*7*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_ASSUM (fun hp2 -> FIRST_X_ASSUM (fun hp1 -> STRIP_ASSUME_TAC (MATCH_MP hp1 hp2))));;
	e (FIRST_ASSUM (fun hp2 -> FIRST_X_ASSUM (fun hp1 -> STRIP_ASSUME_TAC (MATCH_MP hp1 hp2))));;
	e (POP_ASSUM (MP_TAC o GEN_REWRITE_RULE I [LABEL_CONGRUENCE_CASES]));;
	e (REWRITE_TAC[distinctness "label"; injectivity "label"]);;
	e (STRIP_TAC);;
	e (FIRST_X_ASSUM (MP_TAC o GEN_REWRITE_RULE I [LABEL_CONGRUENCE_CASES]));;
	e (REWRITE_TAC[distinctness "label"; injectivity "label"]);;
	e (STRIP_TAC);;
	e (EXISTS_TAC `Tau`);;
	e (REWRITE_TAC[LABEL_CONGRUENCE_REFL]);;
	e (EXISTS_TAC `(q''''' || SUBST1 q'''' q'''''')`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_LSYNC);;
	e (EXISTS_TAC `c'':channel`);;
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_PARALLEL);;
	e (ASM_REWRITE_TAC[]);;
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (ASM_MESON_TAC[SUBST1_CONGRUENCE]);;
	(*8*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_ASSUM (fun hp2 -> FIRST_X_ASSUM (fun hp1 -> STRIP_ASSUME_TAC (MATCH_MP hp1 hp2))));;
	e (FIRST_ASSUM (fun hp2 -> FIRST_X_ASSUM (fun hp1 -> STRIP_ASSUME_TAC (MATCH_MP hp1 hp2))));;
	e (POP_ASSUM (MP_TAC o GEN_REWRITE_RULE I [LABEL_CONGRUENCE_CASES]));;
	e (REWRITE_TAC[distinctness "label"; injectivity "label"]);;
	e (STRIP_TAC);;
	e (FIRST_X_ASSUM (MP_TAC o GEN_REWRITE_RULE I [LABEL_CONGRUENCE_CASES]));;
	e (REWRITE_TAC[distinctness "label"; injectivity "label"]);;
	e (STRIP_TAC);;
	e (EXISTS_TAC `Tau`);;
	e (REWRITE_TAC[LABEL_CONGRUENCE_REFL]);;
	e (EXISTS_TAC `(SUBST1 q'''' q'''''' || q''''')`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_RSYNC);;
	e (EXISTS_TAC `c'':channel`);;
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_PARALLEL);;
	e (ASM_REWRITE_TAC[]);;
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (ASM_MESON_TAC[SUBST1_CONGRUENCE]);;
(*Caso Parallel Sym*)
e (REPEAT STRIP_TAC);;
e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"]);;
e (STRIP_TAC);;
	(*1*)
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (EXISTS_TAC `Tau`);;
	e (EXISTS_TAC `(q' || p''')`);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_SYM; LABEL_CONGRUENCE_REFL]);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_TAU);;
	e (ASM_REWRITE_TAC[]);;
	(*2*)
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (EXISTS_TAC `Tau`);;
	e (EXISTS_TAC `(p''' || q')`);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_SYM; LABEL_CONGRUENCE_REFL]);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_TAU);;
	e (ASM_REWRITE_TAC[]);;
	(*3*)
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (EXISTS_TAC `Out c r`);;
	e (EXISTS_TAC `(q' || p''')`);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_SYM; LABEL_CONGRUENCE_REFL]);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_OUT);;
	e (ASM_REWRITE_TAC[]);;
	(*4*)
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (EXISTS_TAC `Out c r`);;
	e (EXISTS_TAC `(p''' || q')`);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_SYM; LABEL_CONGRUENCE_REFL]);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_OUT);;
	e (ASM_REWRITE_TAC[]);;
	(*5*)
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (EXISTS_TAC `In c`);;
	e (EXISTS_TAC `(BUMP q' || p''')`);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_SYM; LABEL_CONGRUENCE_REFL]);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_IN);;
	e (ASM_REWRITE_TAC[]);;
	(*6*)
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (EXISTS_TAC `In c`);;
	e (EXISTS_TAC `(p''' || BUMP q')`);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_SYM; LABEL_CONGRUENCE_REFL]);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_IN);;
	e (ASM_REWRITE_TAC[]);;
	(*7*)
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (EXISTS_TAC `Tau`);;
	e (EXISTS_TAC `( (SUBST1 q'' r) || p''')`);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_SYM; LABEL_CONGRUENCE_REFL]);;
	e (MATCH_MP_TAC REDUCTION_RSYNC);;
	e (EXISTS_TAC `c:channel`);;
	e (ASM_REWRITE_TAC[]);;
	(*8*)
	e (REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC));;
	e (EXISTS_TAC `Tau`);;
	e (EXISTS_TAC `( p''' || SUBST1 q'' r)`);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_SYM; LABEL_CONGRUENCE_REFL]);;
	e (MATCH_MP_TAC REDUCTION_LSYNC);;
	e (EXISTS_TAC `c:channel`);;
	e (ASM_REWRITE_TAC[]);;
(*Caso Parallel l_assoc*)
e (REPEAT STRIP_TAC);;
e (EXISTS_TAC `l:label`);;
e (REWRITE_TAC[LABEL_CONGRUENCE_REFL]);;
e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"]);;
e (REPEAT STRIP_TAC);;
	(*1*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (EXISTS_TAC `(p''' || q) || r`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_TAU);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_TAU);;
	e (ASM_REWRITE_TAC[]);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
	(*2*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
	e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"; distinctness "label"]);;
	e (REPEAT STRIP_TAC);;
		(*1*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `(p || p'') || r`);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_TAU);;
		e (MATCH_MP_TAC REDUCTION_RPARALLEL_TAU);;
		e (ASM_REWRITE_TAC[]);;
		(*2*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `(p || q) || p''`);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		e (MATCH_MP_TAC REDUCTION_RPARALLEL_TAU);;
		e (ASM_REWRITE_TAC[]);;
		(*3*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `(p || p'') || SUBST1 q'' r'`);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		e (MATCH_MP_TAC REDUCTION_LSYNC);;
		e (EXISTS_TAC `c:channel`);;
		e (ASM_SIMP_TAC[REDUCTION_RPARALLEL_OUT]);;
		(*4*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `SUBST1 (BUMP p || q'') r' || p''`);;
		e CONJ_TAC;;
		e (MATCH_MP_TAC REDUCTION_RSYNC);;
		e (EXISTS_TAC `c:channel`);;
		e (ASM_SIMP_TAC[REDUCTION_RPARALLEL_IN]);;
		e (REWRITE_TAC[SUBST1_PARALLEL; SUBST1_BUMP]);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
	(*3*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (EXISTS_TAC `(p''' || q) || r`);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_OUT);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_OUT);;
	e (ASM_REWRITE_TAC[]);;
	(*4*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;	
	e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
	e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"; distinctness "label"; injectivity "label"]);;
	e (REPEAT STRIP_TAC);;
		(*1*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `(p || p'') || r`);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_OUT);;
		e (MATCH_MP_TAC REDUCTION_RPARALLEL_OUT);;
		e (ASM_REWRITE_TAC[]);;
		(*2*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `(p || q) || p''`);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		e (MATCH_MP_TAC REDUCTION_RPARALLEL_OUT);;
		e (ASM_REWRITE_TAC[]);;
	(*5*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (REWRITE_TAC[BUMP_PARALLEL]);;
	e (EXISTS_TAC `(p''' || BUMP q) || BUMP r`);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_IN);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_IN);;
	e (ASM_REWRITE_TAC[]);;
	(*6*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
	e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"; distinctness "label"; injectivity "label"]);;
	e (REPEAT STRIP_TAC);;
		(*1*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `(BUMP p || p'') || BUMP r`);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_IN);;
		e (MATCH_MP_TAC REDUCTION_RPARALLEL_IN);;
		e (ASM_REWRITE_TAC[]);;
		(*2*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `(BUMP p || BUMP q) || p''`);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		e (REWRITE_TAC[PARALLEL_BUMP]);;
		e (MATCH_MP_TAC REDUCTION_RPARALLEL_IN);;
		e (ASM_REWRITE_TAC[]);;
	(* 7 *)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
	e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"; distinctness "label"; injectivity "label"]);;
	e (REPEAT STRIP_TAC);;
		(*1*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `(p''' || SUBST1 p'''' r') || SUBST1 (BUMP r) r'`);;
		e CONJ_TAC;;
		e (REWRITE_TAC[SUBST1_BUMP]);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_TAU);;
		e (MATCH_MP_TAC REDUCTION_LSYNC);;
		e (EXISTS_TAC `c:channel`);;
		e (ASM_REWRITE_TAC[]);;
		e (REWRITE_TAC[SUBST1_PARALLEL; SUBST1_BUMP; CONGRUENCE_PARALLEL_ASSOC]);;
		(*2*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `(p''' || SUBST1 (BUMP q) r') || SUBST1 p'''' r'`);;
		e CONJ_TAC;;
		e (MATCH_MP_TAC REDUCTION_LSYNC);;
		e (EXISTS_TAC `c:channel`);;
		e (ASM_REWRITE_TAC[]);;
		e (REWRITE_TAC[SUBST1_BUMP]);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_OUT);;
		e (ASM_REWRITE_TAC[]);;
		e (REWRITE_TAC[SUBST1_PARALLEL; SUBST1_BUMP; CONGRUENCE_PARALLEL_ASSOC]);;
	(*8*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (UNDISCH_TAC `REDUCTION p (In c) q''`);;
	e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
	e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"; distinctness "label"; injectivity "label"]);;
	e (REPEAT STRIP_TAC);;
		(*1*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `((SUBST1 q'' r'') || p'') || r`);;
		e (CONJ_TAC);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_TAU);;
		e (MATCH_MP_TAC REDUCTION_RSYNC);;
		e (EXISTS_TAC `c:channel`);;
		e (ASM_REWRITE_TAC[]);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		(*2*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `(SUBST1 (q'' || BUMP q)) r'' || p''`);;
		e (CONJ_TAC);;
		e (MATCH_MP_TAC REDUCTION_RSYNC);;
		e (EXISTS_TAC `c:channel`);;
		e (ASM_REWRITE_TAC[]);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_IN);;
		e (ASM_REWRITE_TAC[]);;
		e (REWRITE_TAC[SUBST1_PARALLEL; SUBST1_BUMP; CONGRUENCE_PARALLEL_ASSOC]);;
(*Caso parallel r_assoc*)
e (REPEAT STRIP_TAC);;
e (EXISTS_TAC `l:label`);;
e (REWRITE_TAC[LABEL_CONGRUENCE_REFL]);;
e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"]);;
e (REPEAT STRIP_TAC);;
	(*1*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
	e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"; distinctness "label"; injectivity "label"]);;
	e (REPEAT STRIP_TAC);;
		(*1*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `p'' || q || r`);;
		e (CONJ_TAC);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_TAU);;
		e (ASM_REWRITE_TAC[]);;
		e (MATCH_MP_TAC CONGRUENCE_SYM);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		(*2*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `p || p'' || r`);;
		e (CONJ_TAC);;
		e (MATCH_MP_TAC REDUCTION_RPARALLEL_TAU);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_TAU);;
		e (ASM_REWRITE_TAC[]);;
		e (MATCH_MP_TAC CONGRUENCE_SYM);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		(*3*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `p'' || SUBST1 (q'' || BUMP r) r'`);;
		e (CONJ_TAC);;
		e (MATCH_MP_TAC REDUCTION_LSYNC);;
		e (EXISTS_TAC `c:channel`);;
		e (ASM_REWRITE_TAC[]);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_IN);;
		e (ASM_REWRITE_TAC[]);;
		e (REWRITE_TAC[SUBST1_PARALLEL; SUBST1_BUMP]);;
		e (MATCH_MP_TAC CONGRUENCE_SYM);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		(*4*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC ` SUBST1 q'' r' || (p'' || r)`);;
		e (CONJ_TAC);;
		e (MATCH_MP_TAC REDUCTION_RSYNC);;
		e (EXISTS_TAC `c:channel`);;
		e (ASM_REWRITE_TAC[]);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_OUT);;
		e (ASM_REWRITE_TAC[]);;
		e (MATCH_MP_TAC CONGRUENCE_SYM);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
	(*2*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (EXISTS_TAC `p || (q || p''')`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_TAU);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_TAU);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_SYM);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
	(*3*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
	e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"; distinctness "label"; injectivity "label"]);;
	e (REPEAT STRIP_TAC);;
		(*1*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `p'' || (q || r)`);;
		e (CONJ_TAC);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_OUT);;
		e (ASM_REWRITE_TAC[]);;
		e (MATCH_MP_TAC CONGRUENCE_SYM);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		(*2*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `p || (p'' || r)`);;
		e (CONJ_TAC);;
		e (MATCH_MP_TAC REDUCTION_RPARALLEL_OUT);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_OUT);;
		e (ASM_REWRITE_TAC[]);;
		e (MATCH_MP_TAC CONGRUENCE_SYM);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
	(*4*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (EXISTS_TAC `p || (q || p''')`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_OUT);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_OUT);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_SYM);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
	(*5*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
	e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"; distinctness "label"; injectivity "label"]);;
	e (REPEAT STRIP_TAC);;
		(*1*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `p'' || BUMP (q || r)`);;
		e (CONJ_TAC);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_IN);;
		e (ASM_REWRITE_TAC[]);;
		e (REWRITE_TAC[BUMP_PARALLEL]);;
		e (MATCH_MP_TAC CONGRUENCE_SYM);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		(*2*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `BUMP p || (p'' || BUMP r)`);;
		e (CONJ_TAC);;
		e (MATCH_MP_TAC REDUCTION_RPARALLEL_IN);;
		e (MATCH_MP_TAC REDUCTION_LPARALLEL_IN);;
		e (ASM_REWRITE_TAC[]);;
		e (MATCH_MP_TAC CONGRUENCE_SYM);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
	(*6*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (EXISTS_TAC `BUMP p || (BUMP q || p''')`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_IN);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_IN);;
	e (ASM_REWRITE_TAC[]);;
	e (REWRITE_TAC[BUMP_PARALLEL]);;
	e (MATCH_MP_TAC CONGRUENCE_SYM);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
	(*7*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (UNDISCH_TAC `REDUCTION r (In c) q''`);;
	e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
	e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"; distinctness "label"; injectivity "label"]);;
	e (REPEAT STRIP_TAC);;
		(*1*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `p'' || SUBST1 ((BUMP q) || q'') r''`);;
		e (CONJ_TAC);;
		e (MATCH_MP_TAC REDUCTION_LSYNC);;
		e (EXISTS_TAC `c:channel`);;
		e (ASM_REWRITE_TAC[]);;
		e (MATCH_MP_TAC REDUCTION_RPARALLEL_IN);;
		e (ASM_REWRITE_TAC[]);;
		e (REWRITE_TAC[SUBST1_PARALLEL; SUBST1_BUMP]);;
		e (MATCH_MP_TAC CONGRUENCE_SYM);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		(*2*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `p || (p'' || SUBST1 q'' r'')`);;
		e (CONJ_TAC);;
		e (MATCH_MP_TAC REDUCTION_RPARALLEL_TAU);;
		e (MATCH_MP_TAC REDUCTION_LSYNC);;
		e (EXISTS_TAC `c:channel`);;
		e (ASM_REWRITE_TAC[]);;
		e (MATCH_MP_TAC CONGRUENCE_SYM);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
	(*8*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
	e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"; distinctness "label"; injectivity "label"]);;
	e (REPEAT STRIP_TAC);;
		(*1*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `(SUBST1 p'''' r') || ((SUBST1 (BUMP q) r') || p''')`);;
		e (CONJ_TAC);;
		e (MATCH_MP_TAC REDUCTION_RSYNC);;
		e (EXISTS_TAC `c:channel`);;
		e (ASM_REWRITE_TAC[]);;
		e (REWRITE_TAC[SUBST1_BUMP]);;
		e (MATCH_MP_TAC REDUCTION_RPARALLEL_OUT);;
		e (ASM_REWRITE_TAC[]);;
		e (REWRITE_TAC[SUBST1_PARALLEL; SUBST1_BUMP]);;
		e (MATCH_MP_TAC CONGRUENCE_SYM);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
		(*2*)
		e (FIRST_X_ASSUM SUBST_ALL_TAC);;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
		e (EXISTS_TAC `p || ((SUBST1 p'''' r') || p''')`);;
		e (CONJ_TAC);;
		e (MATCH_MP_TAC REDUCTION_RPARALLEL_TAU);;
		e (MATCH_MP_TAC REDUCTION_RSYNC);;
		e (EXISTS_TAC `c:channel`);;
		e (ASM_REWRITE_TAC[]);;
		e (REWRITE_TAC[SUBST1_PARALLEL; SUBST1_BUMP]);;
		e (MATCH_MP_TAC CONGRUENCE_SYM);;
		e (REWRITE_TAC[CONGRUENCE_PARALLEL_ASSOC]);;
(*Caso parallel l_nil*)
e (REPEAT STRIP_TAC);;
e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"]);;
e (REPEAT STRIP_TAC);;
	(*1*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (EXISTS_TAC `Tau`);;
	e (EXISTS_TAC `p''':hocore`);;
	e (ASM_REWRITE_TAC[LABEL_CONGRUENCE_REFL; CONGRUENCE_PARALLEL_RNIL]);;
	(*2*)
	e (ASM_MESON_TAC[NOT_REDUCTION_NIL]);;
	(*3*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (EXISTS_TAC `Out c r`);;
	e (EXISTS_TAC `p''':hocore`);;
	e (ASM_REWRITE_TAC[LABEL_CONGRUENCE_REFL; CONGRUENCE_PARALLEL_RNIL]);;
	(*4*)
	e (ASM_MESON_TAC[NOT_REDUCTION_NIL]);;
	(*5*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (FIRST_X_ASSUM (SUBST_ALL_TAC o GSYM));;
	e (EXISTS_TAC `In c`);;
	e (EXISTS_TAC `p''':hocore`);;
	e (ASM_REWRITE_TAC[LABEL_CONGRUENCE_REFL; BUMP; RENAME; CONGRUENCE_PARALLEL_RNIL]);;
	(*6-8*)
	e (ASM_MESON_TAC[NOT_REDUCTION_NIL]);;
	e (ASM_MESON_TAC[NOT_REDUCTION_NIL]);;
	e (ASM_MESON_TAC[NOT_REDUCTION_NIL]);;
(*Caso parallel r_nil*)
e (REPEAT STRIP_TAC);;
e (EXISTS_TAC `l:label`);;
e (REWRITE_TAC[LABEL_CONGRUENCE_REFL]);;
e (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [REDUCTION_CASES]));;
e (REWRITE_TAC[distinctness "hocore"; injectivity "hocore"]);;
e (REPEAT STRIP_TAC);;
	(*1*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (EXISTS_TAC `p' || BUMP Nil`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_IN);;
	e (REWRITE_TAC[REDUCTION_RECV]);;
	e (REWRITE_TAC[BUMP; RENAME]);;
	e (MATCH_MP_TAC CONGRUENCE_SYM);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_RNIL]);;
	(*2*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (EXISTS_TAC `Nil || Nil`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_OUT);;
	e (REWRITE_TAC[REDUCTION_SEND]);;
	e (MATCH_MP_TAC CONGRUENCE_SYM);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_RNIL]);;
	(*3*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (EXISTS_TAC `(p''' || q) || Nil`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_TAU);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_TAU);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_SYM);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_RNIL]);;
	(*4*)	
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (EXISTS_TAC `(q || p''') || Nil`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_TAU);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_TAU);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_SYM);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_RNIL]);;
	(*5*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (EXISTS_TAC `(p''' || q) || Nil`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_OUT);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_OUT);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_SYM);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_RNIL]);;
	(*6*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (EXISTS_TAC `(q || p''') || Nil`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_OUT);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_OUT);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_SYM);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_RNIL]);;
	(*7*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (EXISTS_TAC `(p''' || BUMP q) || BUMP Nil`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_IN);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_IN);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_TRANS);;
	e (EXISTS_TAC `(p''' || BUMP q ) || Nil`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC CONGRUENCE_SYM);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_RNIL]);;
	e (REWRITE_TAC[BUMP; RENAME; CONGRUENCE_REFL]);;
	(*8*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (EXISTS_TAC `(BUMP q || p''') || BUMP Nil`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_IN);;
	e (MATCH_MP_TAC REDUCTION_RPARALLEL_IN);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_TRANS);;
	e (EXISTS_TAC `(BUMP q || p''') || Nil`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC CONGRUENCE_SYM);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_RNIL]);;
	e (REWRITE_TAC[BUMP; RENAME; CONGRUENCE_REFL]);;
	(*9*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (EXISTS_TAC `(p''' || SUBST1 q' r) || Nil`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_TAU);;
	e (MATCH_MP_TAC REDUCTION_LSYNC);;
	e (EXISTS_TAC `c:channel`);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_SYM);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_RNIL]);;
	(*10*)
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (FIRST_X_ASSUM SUBST_ALL_TAC);;
	e (EXISTS_TAC `(SUBST1 q' r || p''') || Nil`);;
	e (CONJ_TAC);;
	e (MATCH_MP_TAC REDUCTION_LPARALLEL_TAU);;
	e (MATCH_MP_TAC REDUCTION_RSYNC);;
	e (EXISTS_TAC `c:channel`);;
	e (ASM_REWRITE_TAC[]);;
	e (MATCH_MP_TAC CONGRUENCE_SYM);;
	e (REWRITE_TAC[CONGRUENCE_PARALLEL_RNIL]);;
let CONGRUENCE_THRU_REDUCTION = top_thm();;