equal
deleted
inserted
replaced
739 \begin{lemma}\label{optimised} Let @{text x} be of permutation type. |
739 \begin{lemma}\label{optimised} Let @{text x} be of permutation type. |
740 We have that @{thm (concl) finite_supp_unique[no_vars]} |
740 We have that @{thm (concl) finite_supp_unique[no_vars]} |
741 provided @{thm (prem 1) finite_supp_unique[no_vars]}, |
741 provided @{thm (prem 1) finite_supp_unique[no_vars]}, |
742 @{thm (prem 2) finite_supp_unique[no_vars]}, and for |
742 @{thm (prem 2) finite_supp_unique[no_vars]}, and for |
743 all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a} |
743 all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a} |
744 and @{text b} having the same sort, then \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}} |
744 and @{text b} having the same sort, \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}} |
745 \end{lemma} |
745 \end{lemma} |
746 |
746 |
747 \begin{proof} |
747 \begin{proof} |
748 By Lemma \ref{supports}@{text ".iii)"} we have to show that for every finite |
748 By Lemma \ref{supports}@{text ".iii)"} we have to show that for every finite |
749 set @{text S'} that supports @{text x}, \mbox{@{text "S \<subseteq> S'"}} holds. We will |
749 set @{text S'} that supports @{text x}, \mbox{@{text "S \<subseteq> S'"}} holds. We will |