theorem :: SCMISORT:31

( insert-sort (fsloc 0) is keepInt0_1 & insert-sort (fsloc 0) is InitHalting ) by Lm12;