( bubble-sort (fsloc 0) is keepInt0_1 & bubble-sort (fsloc 0) is InitHalting ) by Lm26;