let I be Instruction of SCM+FSA ; :: thesis: ( InsCode I = 0 implies I = halt SCM+FSA )
assume InsCode I = 0 ; :: thesis: I = halt SCM+FSA
then I = halt SCM by Th119, AMI_3:71;
then I is halting by Th103;
hence I = halt SCM+FSA by Th121; :: thesis: verum