let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a <> 0 holds
while=0 (a,I) is_halting_on s,P

let s be State of SCM+FSA; :: thesis: for I being MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a <> 0 holds
while=0 (a,I) is_halting_on s,P

let I be MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st s . a <> 0 holds
while=0 (a,I) is_halting_on s,P

let a be read-write Int-Location; :: thesis: ( s . a <> 0 implies while=0 (a,I) is_halting_on s,P )
assume A1: s . a <> 0 ; :: thesis: while=0 (a,I) is_halting_on s,P
set i = a =0_goto 3;
set s1 = Initialize s;
set P1 = P +* (while=0 (a,I));
A2: IC in dom () by MEMSTR_0:15;
A3: IC () = IC () by
.= 0 by FUNCOP_1:72 ;
set loc5 = (card I) + 4;
set s5 = Comput ((P +* (while=0 (a,I))),(),3);
set s4 = Comput ((P +* (while=0 (a,I))),(),2);
set s2 = Comput ((P +* (while=0 (a,I))),(),1);
A4: 1 in dom (while=0 (a,I)) by SCMFSA_X:5;
not a in dom () by SCMFSA_2:102;
then A5: (Initialize s) . a = s . a by FUNCT_4:11;
A6: (P +* (while=0 (a,I))) /. (IC ()) = (P +* (while=0 (a,I))) . (IC ()) by PBOOLE:143;
0 in dom (while=0 (a,I)) by AFINSQ_1:65;
then (P +* (while=0 (a,I))) . 0 = (while=0 (a,I)) . 0 by FUNCT_4:13
.= a =0_goto 3 by SCMFSA_X:10 ;
then A7: CurInstr ((P +* (while=0 (a,I))),()) = a =0_goto 3 by A3, A6;
A8: Comput ((P +* (while=0 (a,I))),(),(0 + 1)) = Following ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(),0))) by EXTPRO_1:3
.= Exec ((a =0_goto 3),()) by A7 ;
A9: IC (Comput ((P +* (while=0 (a,I))),(),1)) = 0 + 1 by ;
A10: (P +* (while=0 (a,I))) /. (IC (Comput ((P +* (while=0 (a,I))),(),1))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(),1))) by PBOOLE:143;
(P +* (while=0 (a,I))) . 1 = (while=0 (a,I)) . 1 by
.= goto 2 by SCMFSA_X:10 ;
then A11: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(),1))) = goto 2 by ;
A12: Comput ((P +* (while=0 (a,I))),(),(1 + 1)) = Following ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(),1))) by EXTPRO_1:3
.= Exec ((goto 2),(Comput ((P +* (while=0 (a,I))),(),1))) by A11 ;
A13: IC (Comput ((P +* (while=0 (a,I))),(),2)) = 2 by ;
A14: 2 in dom (while=0 (a,I)) by SCMFSA_X:5;
A15: (card I) + 4 in dom (while=0 (a,I)) by SCMFSA_X:6;
A16: (P +* (while=0 (a,I))) /. (IC (Comput ((P +* (while=0 (a,I))),(),2))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(),2))) by PBOOLE:143;
(P +* (while=0 (a,I))) . 2 = (while=0 (a,I)) . 2 by
.= goto ((card I) + 4) by SCMFSA_X:12 ;
then A17: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(),2))) = goto ((card I) + 4) by ;
A18: Comput ((P +* (while=0 (a,I))),(),(2 + 1)) = Following ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(),2))) by EXTPRO_1:3
.= Exec ((goto ((card I) + 4)),(Comput ((P +* (while=0 (a,I))),(),2))) by A17 ;
A19: IC (Comput ((P +* (while=0 (a,I))),(),3)) = (card I) + 4 by ;
A20: (P +* (while=0 (a,I))) /. (IC (Comput ((P +* (while=0 (a,I))),(),3))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(),3))) by PBOOLE:143;
(P +* (while=0 (a,I))) . ((card I) + 4) = (while=0 (a,I)) . ((card I) + 4) by
.= halt SCM+FSA by SCMFSA_X:11 ;
then CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(),3))) = halt SCM+FSA by ;
then P +* (while=0 (a,I)) halts_on Initialize s by EXTPRO_1:29;
hence while=0 (a,I) is_halting_on s,P by SCMFSA7B:def 7; :: thesis: verum
thus verum ; :: thesis: verum