69 

    69 

    70 lemma alpha5_symp:

    70 lemma alpha5_symp:

    71 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>

    71 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>

    72 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>

    72 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>

    73 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"

    73 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"

    74 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)

    76 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)

    75 apply (simp_all add: alpha5_inj)

    77 apply (simp_all add: alpha5_inj)

    76 apply (erule exE)

    78 apply (erule exE)

    77 apply (rule_tac x="- pi" in exI)

    79 apply (rule_tac x="- pi" in exI)

    78 apply (simp add: alpha_gen)

    80 apply (simp add: alpha_gen)

    87 apply (frule_tac p="- pi" in alpha5_eqvt(1))

    89 apply (frule_tac p="- pi" in alpha5_eqvt(1))

    88 apply simp

    90 apply simp

    89 apply (rotate_tac 6)

    91 apply (rotate_tac 6)

    90 apply simp

    92 apply simp

    91 apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1])

    93 apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1])

    93 done

    95 done

    94 

    96 

    95 lemma alpha5_transp:

    97 lemma alpha5_transp:

    96 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and>

    98 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and>

    97 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and>

    99 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and>