513 definition blexer_simp where |
511 definition blexer_simp where |
514 "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then |
512 "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then |
515 decode (bmkeps (bders_simp (intern r) s)) r else None" |
513 decode (bmkeps (bders_simp (intern r) s)) r else None" |
516 |
514 |
517 |
515 |
|
516 lemma asize0: |
|
517 shows "0 < asize r" |
|
518 apply(induct r) |
|
519 apply(auto) |
|
520 done |
|
521 |
|
522 |
518 lemma bders_simp_append: |
523 lemma bders_simp_append: |
519 shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2" |
524 shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2" |
520 apply(induct s1 arbitrary: r s2) |
525 apply(induct s1 arbitrary: r s2) |
521 apply(simp) |
526 apply(simp) |
522 apply(simp) |
527 apply(simp) |
523 done |
528 done |
524 |
529 |
525 |
530 lemma bsimp_ASEQ_size: |
|
531 shows "asize (bsimp_ASEQ bs r1 r2) \<le> Suc (asize r1 + asize r2)" |
|
532 apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) |
|
533 apply(auto) |
|
534 done |
|
535 |
|
536 lemma fuse_size: |
|
537 shows "asize (fuse bs r) = asize r" |
|
538 apply(induct r) |
|
539 apply(auto) |
|
540 done |
|
541 |
|
542 lemma flts_size: |
|
543 shows "sum_list (map asize (flts rs)) \<le> sum_list (map asize rs)" |
|
544 apply(induct rs rule: flts.induct) |
|
545 apply(simp_all) |
|
546 by (metis (mono_tags, lifting) add_mono_thms_linordered_semiring(1) comp_apply fuse_size le_SucI order_refl sum_list_cong) |
|
547 |
|
548 |
|
549 lemma bsimp_AALTs_size: |
|
550 shows "asize (bsimp_AALTs bs rs) \<le> Suc (sum_list (map asize rs))" |
|
551 apply(induct rs rule: bsimp_AALTs.induct) |
|
552 apply(auto simp add: fuse_size) |
|
553 done |
|
554 |
|
555 lemma bsimp_size: |
|
556 shows "asize (bsimp r) \<le> asize r" |
|
557 apply(induct r) |
|
558 apply(simp_all) |
|
559 apply (meson Suc_le_mono add_mono_thms_linordered_semiring(1) bsimp_ASEQ_size le_trans) |
|
560 apply(rule le_trans) |
|
561 apply(rule bsimp_AALTs_size) |
|
562 apply(simp) |
|
563 apply(rule le_trans) |
|
564 apply(rule flts_size) |
|
565 by (simp add: sum_list_mono) |
|
566 |
|
567 fun nonalt :: "arexp \<Rightarrow> bool" |
|
568 where |
|
569 "nonalt (AALTs bs2 rs) = False" |
|
570 | "nonalt r = True" |
|
571 |
|
572 |
|
573 |
|
574 |
|
575 lemma bsimp_AALTs_size2: |
|
576 assumes "\<forall>r \<in> set rs. nonalt r" |
|
577 shows "asize (bsimp_AALTs bs rs) \<ge> sum_list (map asize rs)" |
|
578 using assms |
|
579 apply(induct rs rule: bsimp_AALTs.induct) |
|
580 apply(simp_all add: fuse_size) |
|
581 done |
|
582 |
|
583 lemma qq: |
|
584 shows "map (asize \<circ> fuse bs) rs = map asize rs" |
|
585 apply(induct rs) |
|
586 apply(auto simp add: fuse_size) |
|
587 done |
|
588 |
|
589 lemma flts_size2: |
|
590 assumes "\<exists>bs rs'. AALTs bs rs' \<in> set rs" |
|
591 shows "sum_list (map asize (flts rs)) < sum_list (map asize rs)" |
|
592 using assms |
|
593 apply(induct rs) |
|
594 apply(auto simp add: qq) |
|
595 apply (simp add: flts_size less_Suc_eq_le) |
|
596 apply(case_tac a) |
|
597 apply(auto simp add: qq) |
|
598 prefer 2 |
|
599 apply (simp add: flts_size le_imp_less_Suc) |
|
600 using less_Suc_eq by auto |
|
601 |
526 lemma L_bsimp_ASEQ: |
602 lemma L_bsimp_ASEQ: |
527 "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))" |
603 "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))" |
528 apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) |
604 apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) |
529 apply(simp_all) |
605 apply(simp_all) |
530 by (metis erase_fuse fuse.simps(4)) |
606 by (metis erase_fuse fuse.simps(4)) |
664 shows "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)" |
746 shows "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)" |
665 apply(induct rs arbitrary: bs) |
747 apply(induct rs arbitrary: bs) |
666 apply(simp) |
748 apply(simp) |
667 apply(simp) |
749 apply(simp) |
668 done |
750 done |
|
751 |
|
752 lemma fuse_empty: |
|
753 shows "fuse [] r = r" |
|
754 apply(induct r) |
|
755 apply(auto) |
|
756 done |
|
757 |
|
758 lemma flts_fuse: |
|
759 shows "map (fuse bs) (flts rs) = flts (map (fuse bs) rs)" |
|
760 apply(induct rs arbitrary: bs rule: flts.induct) |
|
761 apply(auto simp add: fuse_append) |
|
762 done |
|
763 |
|
764 lemma bsimp_ASEQ_fuse: |
|
765 shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2" |
|
766 apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct) |
|
767 apply(auto) |
|
768 done |
|
769 |
|
770 lemma bsimp_AALTs_fuse: |
|
771 assumes "\<forall>r \<in> set rs. fuse bs1 (fuse bs2 r) = fuse (bs1 @ bs2) r" |
|
772 shows "fuse bs1 (bsimp_AALTs bs2 rs) = bsimp_AALTs (bs1 @ bs2) rs" |
|
773 using assms |
|
774 apply(induct bs2 rs arbitrary: bs1 rule: bsimp_AALTs.induct) |
|
775 apply(auto) |
|
776 done |
|
777 |
|
778 |
|
779 |
|
780 lemma bsimp_fuse: |
|
781 shows "fuse bs (bsimp r) = bsimp (fuse bs r)" |
|
782 apply(induct r arbitrary: bs) |
|
783 apply(simp) |
|
784 apply(simp) |
|
785 apply(simp) |
|
786 prefer 3 |
|
787 apply(simp) |
|
788 apply(simp) |
|
789 apply (simp add: bsimp_ASEQ_fuse) |
|
790 apply(simp) |
|
791 by (simp add: bsimp_AALTs_fuse fuse_append) |
|
792 |
|
793 lemma bsimp_fuse_AALTs: |
|
794 shows "fuse bs (bsimp (AALTs [] rs)) = bsimp (AALTs bs rs)" |
|
795 apply(subst bsimp_fuse) |
|
796 apply(simp) |
|
797 done |
|
798 |
|
799 lemma bsimp_fuse_AALTs2: |
|
800 shows "fuse bs (bsimp_AALTs [] rs) = bsimp_AALTs bs rs" |
|
801 using bsimp_AALTs_fuse fuse_append by auto |
|
802 |
|
803 |
|
804 lemma bsimp_ASEQ_idem: |
|
805 assumes "bsimp (bsimp r1) = bsimp r1" "bsimp (bsimp r2) = bsimp r2" |
|
806 shows "bsimp (bsimp_ASEQ x1 (bsimp r1) (bsimp r2)) = bsimp_ASEQ x1 (bsimp r1) (bsimp r2)" |
|
807 using assms |
|
808 apply(case_tac "bsimp r1 = AZERO") |
|
809 apply(simp) |
|
810 apply(case_tac "bsimp r2 = AZERO") |
|
811 apply(simp) |
|
812 apply (metis bnullable.elims(2) bnullable.elims(3) bsimp.simps(3) bsimp_ASEQ.simps(2) bsimp_ASEQ.simps(3) bsimp_ASEQ.simps(4) bsimp_ASEQ.simps(5) bsimp_ASEQ.simps(6)) |
|
813 apply(case_tac "\<exists>bs. bsimp r1 = AONE bs") |
|
814 apply(auto)[1] |
|
815 apply(subst bsimp_ASEQ2) |
|
816 apply(subst bsimp_ASEQ2) |
|
817 apply (metis assms(2) bsimp_fuse) |
|
818 apply(subst bsimp_ASEQ1) |
|
819 apply(auto) |
|
820 done |
|
821 |
|
822 |
|
823 fun nonnested :: "arexp \<Rightarrow> bool" |
|
824 where |
|
825 "nonnested (AALTs bs2 []) = True" |
|
826 | "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False" |
|
827 | "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)" |
|
828 | "nonnested r = True" |
|
829 |
|
830 |
|
831 lemma k0: |
|
832 shows "flts (r # rs1) = flts [r] @ flts rs1" |
|
833 apply(induct r arbitrary: rs1) |
|
834 apply(auto) |
|
835 done |
|
836 |
|
837 lemma k00: |
|
838 shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2" |
|
839 apply(induct rs1 arbitrary: rs2) |
|
840 apply(auto) |
|
841 by (metis append.assoc k0) |
|
842 |
|
843 lemma k0a: |
|
844 shows "flts [AALTs bs rs] = map (fuse bs) rs" |
|
845 apply(simp) |
|
846 done |
|
847 |
|
848 fun spill where |
|
849 "spill (AALTs bs rs) = map (fuse bs) rs" |
|
850 |
|
851 lemma k0a2: |
|
852 assumes "\<not> nonalt r" |
|
853 shows "flts [r] = spill r" |
|
854 using assms |
|
855 apply(case_tac r) |
|
856 apply(simp_all) |
|
857 done |
|
858 |
|
859 lemma k0b: |
|
860 assumes "nonalt r" "r \<noteq> AZERO" |
|
861 shows "flts [r] = [r]" |
|
862 using assms |
|
863 apply(case_tac r) |
|
864 apply(simp_all) |
|
865 done |
|
866 |
|
867 lemma nn1: |
|
868 assumes "nonnested (AALTs bs rs)" |
|
869 shows "\<nexists>bs1 rs1. flts rs = [AALTs bs1 rs1]" |
|
870 using assms |
|
871 apply(induct rs rule: flts.induct) |
|
872 apply(auto) |
|
873 done |
|
874 |
|
875 lemma nn1q: |
|
876 assumes "nonnested (AALTs bs rs)" |
|
877 shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set (flts rs)" |
|
878 using assms |
|
879 apply(induct rs rule: flts.induct) |
|
880 apply(auto) |
|
881 done |
|
882 |
|
883 lemma nn1qq: |
|
884 assumes "nonnested (AALTs bs rs)" |
|
885 shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set rs" |
|
886 using assms |
|
887 apply(induct rs rule: flts.induct) |
|
888 apply(auto) |
|
889 done |
|
890 |
|
891 lemma nn10: |
|
892 assumes "nonnested (AALTs cs rs)" |
|
893 shows "nonnested (AALTs (bs @ cs) rs)" |
|
894 using assms |
|
895 apply(induct rs arbitrary: cs bs) |
|
896 apply(simp_all) |
|
897 apply(case_tac a) |
|
898 apply(simp_all) |
|
899 done |
|
900 |
|
901 lemma nn11a: |
|
902 assumes "nonalt r" |
|
903 shows "nonalt (fuse bs r)" |
|
904 using assms |
|
905 apply(induct r) |
|
906 apply(auto) |
|
907 done |
|
908 |
|
909 |
|
910 lemma nn1a: |
|
911 assumes "nonnested r" |
|
912 shows "nonnested (fuse bs r)" |
|
913 using assms |
|
914 apply(induct bs r arbitrary: rule: fuse.induct) |
|
915 apply(simp_all add: nn10) |
|
916 done |
|
917 |
|
918 lemma n0: |
|
919 shows "nonnested (AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)" |
|
920 apply(induct rs arbitrary: bs) |
|
921 apply(auto) |
|
922 apply (metis list.set_intros(1) nn1qq nonalt.elims(3)) |
|
923 apply (metis list.set_intros(2) nn1qq nonalt.elims(3)) |
|
924 by (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7)) |
|
925 |
|
926 |
|
927 |
|
928 |
|
929 lemma nn1c: |
|
930 assumes "\<forall>r \<in> set rs. nonnested r" |
|
931 shows "\<forall>r \<in> set (flts rs). nonalt r" |
|
932 using assms |
|
933 apply(induct rs rule: flts.induct) |
|
934 apply(auto) |
|
935 apply(rule nn11a) |
|
936 by (metis nn1qq nonalt.elims(3)) |
|
937 |
|
938 lemma nn1bb: |
|
939 assumes "\<forall>r \<in> set rs. nonalt r" |
|
940 shows "nonnested (bsimp_AALTs bs rs)" |
|
941 using assms |
|
942 apply(induct bs rs rule: bsimp_AALTs.induct) |
|
943 apply(auto) |
|
944 apply (metis nn11a nonalt.simps(1) nonnested.elims(3)) |
|
945 using n0 by auto |
|
946 |
|
947 lemma nn1b: |
|
948 shows "nonnested (bsimp r)" |
|
949 apply(induct r) |
|
950 apply(simp_all) |
|
951 apply(case_tac "bsimp r1 = AZERO") |
|
952 apply(simp) |
|
953 apply(case_tac "bsimp r2 = AZERO") |
|
954 apply(simp) |
|
955 apply(subst bsimp_ASEQ0) |
|
956 apply(simp) |
|
957 apply(case_tac "\<exists>bs. bsimp r1 = AONE bs") |
|
958 apply(auto)[1] |
|
959 apply(subst bsimp_ASEQ2) |
|
960 apply (simp add: nn1a) |
|
961 apply(subst bsimp_ASEQ1) |
|
962 apply(auto) |
|
963 apply(rule nn1bb) |
|
964 apply(auto) |
|
965 by (metis (mono_tags, hide_lams) imageE nn1c set_map) |
|
966 |
|
967 lemma rt: |
|
968 shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)" |
|
969 apply(induct rs) |
|
970 apply(simp) |
|
971 apply(simp) |
|
972 apply(subst k0) |
|
973 apply(simp) |
|
974 by (smt add_le_cancel_right add_mono bsimp_size flts.simps(1) flts_size k0 le_iff_add list.simps(9) map_append sum_list.Cons sum_list.append trans_le_add1) |
|
975 |
|
976 lemma flts_idem: |
|
977 assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r" |
|
978 shows "flts (map bsimp (flts (map bsimp rs))) = flts (map bsimp rs)" |
|
979 using assms |
|
980 apply(induct rs) |
|
981 apply(simp) |
|
982 apply(simp) |
|
983 apply(subst k0) |
|
984 apply(subst (2) k0) |
|
985 apply(case_tac "bsimp a = AZERO") |
|
986 apply(simp) |
|
987 apply(case_tac "nonalt (bsimp a)") |
|
988 thm k0 k0a k0b |
|
989 apply(subst k0b) |
|
990 apply(simp) |
|
991 apply(simp) |
|
992 apply(simp) |
|
993 apply(subst k0b) |
|
994 apply(simp) |
|
995 apply(simp) |
|
996 apply(simp) |
|
997 apply(subst k0) |
|
998 apply(subst k0b) |
|
999 apply(simp) |
|
1000 apply(simp) |
|
1001 apply(simp) |
|
1002 apply(simp) |
|
1003 apply(simp add: k00) |
|
1004 apply(subst k0a2) |
|
1005 apply(simp) |
|
1006 apply(subst k0a2) |
|
1007 apply(simp) |
|
1008 apply(case_tac a) |
|
1009 apply(simp_all) |
|
1010 sorry |
|
1011 |
|
1012 lemma bsimp_AALTs_idem: |
|
1013 (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r \<and> nonalt (bsimp r)" *) |
|
1014 (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r" *) |
|
1015 shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))" |
|
1016 apply(induct rs arbitrary: bs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct) |
|
1017 apply(case_tac x) |
|
1018 apply(simp) |
|
1019 apply(simp) |
|
1020 apply(case_tac "\<exists>bs' rs'. a = AALTs bs' rs'") |
|
1021 apply(clarify) |
|
1022 apply(case_tac list) |
|
1023 apply(simp) |
|
1024 apply(simp) |
|
1025 |
|
1026 apply(drule_tac x="flts (rs' @ list)" in spec) |
|
1027 apply(erule impE) |
|
1028 prefer 2 |
|
1029 apply(case_tac a) |
|
1030 apply(simp) |
|
1031 apply(case_tac list) |
|
1032 apply(simp) |
|
1033 apply(simp) |
|
1034 apply(case_tac list) |
|
1035 apply(simp) |
|
1036 apply(simp) |
|
1037 apply(case_tac list) |
|
1038 apply(simp) |
|
1039 apply(simp) |
|
1040 prefer 3 |
|
1041 apply(case_tac list) |
|
1042 apply(simp) |
|
1043 apply(simp) |
|
1044 apply(case_tac list) |
|
1045 apply(simp) |
|
1046 |
|
1047 |
|
1048 apply(simp) |
|
1049 |
|
1050 apply(case_tac "flts (map bsimp list)") |
|
1051 apply(simp) |
|
1052 apply(simp) |
|
1053 |
|
1054 |
|
1055 |
|
1056 prefer 2 |
|
1057 apply(simp) |
|
1058 |
|
1059 apply(subst k0) |
|
1060 apply(subst (2) k0) |
|
1061 |
|
1062 apply(case_tac a) |
|
1063 apply(simp_all) |
|
1064 |
|
1065 prefer 2 |
|
1066 apply(simp) |
|
1067 apply(case_tac r) |
|
1068 apply(auto) |
|
1069 apply(case_tac "bsimp x42 = AZERO") |
|
1070 apply(simp) |
|
1071 apply(case_tac "bsimp x43 = AZERO") |
|
1072 apply(simp) |
|
1073 apply(subst bsimp_ASEQ0) |
|
1074 apply(subst bsimp_ASEQ0) |
|
1075 apply(simp) |
|
1076 apply(case_tac "\<exists>bs. bsimp x42 = AONE bs") |
|
1077 apply(auto)[1] |
|
1078 apply(subst bsimp_ASEQ2) |
|
1079 apply(subst bsimp_ASEQ2) |
|
1080 prefer 2 |
|
1081 apply(subst bsimp_ASEQ1) |
|
1082 apply(auto) |
|
1083 apply(subst bsimp_ASEQ1) |
|
1084 apply(auto) |
|
1085 apply(subst (asm) bsimp_ASEQ2) |
|
1086 apply(subst (asm) bsimp_ASEQ2) |
|
1087 using flts_fuse bsimp_fuse bsimp_fuse_AALTs bsimp_fuse_AALTs2 bsimp_AALTs.simps flts.simps |
|
1088 |
|
1089 apply(case_tac x43) |
|
1090 apply(simp_all) |
|
1091 prefer 3 |
|
1092 oops |
|
1093 |
|
1094 lemma bsimp_idem: |
|
1095 shows "bsimp (bsimp r) = bsimp r" |
|
1096 apply(induct r taking: "asize" rule: measure_induct) |
|
1097 apply(case_tac x) |
|
1098 apply(simp) |
|
1099 apply(simp) |
|
1100 apply(simp) |
|
1101 prefer 3 |
|
1102 apply(simp) |
|
1103 apply(simp) |
|
1104 apply (simp add: bsimp_ASEQ_idem) |
|
1105 apply(clarify) |
|
1106 apply(case_tac x52) |
|
1107 apply(simp) |
|
1108 apply(simp) |
|
1109 apply(subst k0) |
|
1110 apply(subst (2) k0) |
|
1111 apply(case_tac "bsimp a = AZERO") |
|
1112 apply(simp) |
|
1113 apply(frule_tac x="AALTs x51 (flts (map bsimp list))" in spec) |
|
1114 apply(drule mp) |
|
1115 apply(simp) |
|
1116 apply (meson add_le_cancel_right asize0 le_trans not_le rt trans_le_add2) |
|
1117 apply(simp) |
|
1118 apply(subst (asm) flts_idem) |
|
1119 apply(auto)[1] |
|
1120 apply(drule_tac x="r" in spec) |
|
1121 apply (metis add.commute add_lessD1 not_add_less1 not_less_eq sum_list_map_remove1) |
|
1122 apply(simp) |
|
1123 apply(subst flts_idem) |
|
1124 apply(auto)[1] |
|
1125 apply(drule_tac x="r" in spec) |
|
1126 apply (metis add.commute add_lessD1 not_add_less1 not_less_eq sum_list_map_remove1) |
|
1127 apply(simp) |
|
1128 apply(case_tac "nonalt (bsimp a)") |
|
1129 apply(subst k0b) |
|
1130 apply(simp) |
|
1131 apply(simp) |
|
1132 apply(subst k0b) |
|
1133 apply(simp) |
|
1134 apply(simp) |
|
1135 apply(auto)[1] |
|
1136 apply(frule_tac x="AALTs x51 (bsimp a # flts (map bsimp list))" in spec) |
|
1137 apply(drule mp) |
|
1138 apply(simp) |
|
1139 prefer 2 |
|
1140 apply(simp) |
|
1141 apply(subst (asm) k0) |
|
1142 apply(subst (asm) flts_idem) |
|
1143 apply(auto)[1] |
|
1144 apply (simp add: sum_list_map_remove1) |
|
1145 apply(subst (asm) k0b) |
|
1146 apply(simp) |
|
1147 apply(simp) |
|
1148 apply(simp) |
|
1149 apply(subst k0) |
|
1150 apply(subst flts_idem) |
|
1151 apply(auto)[1] |
|
1152 apply (simp add: sum_list_map_remove1) |
|
1153 apply(subst k0b) |
|
1154 apply(simp) |
|
1155 apply(simp) |
|
1156 apply(simp) |
|
1157 lemma XX_bder: |
|
1158 shows "bsimp (bder c (bsimp r)) = (bsimp \<circ> bder c) r" |
|
1159 apply(induct r) |
|
1160 apply(simp) |
|
1161 apply(simp) |
|
1162 apply(simp) |
|
1163 prefer 3 |
|
1164 apply(simp) |
|
1165 prefer 2 |
|
1166 apply(simp) |
|
1167 apply(case_tac x2a) |
|
1168 apply(simp) |
|
1169 apply(simp) |
|
1170 apply(auto)[1] |
|
1171 |
669 |
1172 |
670 lemma q3a: |
1173 lemma q3a: |
671 assumes "\<exists>r \<in> set rs. bnullable r" |
1174 assumes "\<exists>r \<in> set rs. bnullable r" |
672 shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)" |
1175 shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)" |
673 using assms |
1176 using assms |