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 (Start-At (0,SCM+FSA)) by MEMSTR_0:15;

A3: IC (Initialize s) = IC (Start-At (0,SCM+FSA)) by A2, FUNCT_4:13

.= 0 by FUNCOP_1:72 ;

set loc5 = (card I) + 4;

set s5 = Comput ((P +* (while=0 (a,I))),(Initialize s),3);

set s4 = Comput ((P +* (while=0 (a,I))),(Initialize s),2);

set s2 = Comput ((P +* (while=0 (a,I))),(Initialize s),1);

A4: 1 in dom (while=0 (a,I)) by SCMFSA_X:5;

not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;

then A5: (Initialize s) . a = s . a by FUNCT_4:11;

A6: (P +* (while=0 (a,I))) /. (IC (Initialize s)) = (P +* (while=0 (a,I))) . (IC (Initialize s)) 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))),(Initialize s)) = a =0_goto 3 by A3, A6;

A8: Comput ((P +* (while=0 (a,I))),(Initialize s),(0 + 1)) = Following ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),0))) by EXTPRO_1:3

.= Exec ((a =0_goto 3),(Initialize s)) by A7 ;

A9: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),1)) = 0 + 1 by A1, A3, A8, A5, SCMFSA_2:70;

A10: (P +* (while=0 (a,I))) /. (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),1))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),1))) by PBOOLE:143;

(P +* (while=0 (a,I))) . 1 = (while=0 (a,I)) . 1 by A4, FUNCT_4:13

.= goto 2 by SCMFSA_X:10 ;

then A11: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),1))) = goto 2 by A9, A10;

A12: Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + 1)) = Following ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),1))) by EXTPRO_1:3

.= Exec ((goto 2),(Comput ((P +* (while=0 (a,I))),(Initialize s),1))) by A11 ;

A13: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),2)) = 2 by A12, SCMFSA_2:69;

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))),(Initialize s),2))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),2))) by PBOOLE:143;

(P +* (while=0 (a,I))) . 2 = (while=0 (a,I)) . 2 by A14, FUNCT_4:13

.= goto ((card I) + 4) by SCMFSA_X:12 ;

then A17: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),2))) = goto ((card I) + 4) by A13, A16;

A18: Comput ((P +* (while=0 (a,I))),(Initialize s),(2 + 1)) = Following ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),2))) by EXTPRO_1:3

.= Exec ((goto ((card I) + 4)),(Comput ((P +* (while=0 (a,I))),(Initialize s),2))) by A17 ;

A19: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),3)) = (card I) + 4 by A18, SCMFSA_2:69;

A20: (P +* (while=0 (a,I))) /. (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),3))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),3))) by PBOOLE:143;

(P +* (while=0 (a,I))) . ((card I) + 4) = (while=0 (a,I)) . ((card I) + 4) by A15, FUNCT_4:13

.= halt SCM+FSA by SCMFSA_X:11 ;

then CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),3))) = halt SCM+FSA by A19, A20;

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

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 (Start-At (0,SCM+FSA)) by MEMSTR_0:15;

A3: IC (Initialize s) = IC (Start-At (0,SCM+FSA)) by A2, FUNCT_4:13

.= 0 by FUNCOP_1:72 ;

set loc5 = (card I) + 4;

set s5 = Comput ((P +* (while=0 (a,I))),(Initialize s),3);

set s4 = Comput ((P +* (while=0 (a,I))),(Initialize s),2);

set s2 = Comput ((P +* (while=0 (a,I))),(Initialize s),1);

A4: 1 in dom (while=0 (a,I)) by SCMFSA_X:5;

not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;

then A5: (Initialize s) . a = s . a by FUNCT_4:11;

A6: (P +* (while=0 (a,I))) /. (IC (Initialize s)) = (P +* (while=0 (a,I))) . (IC (Initialize s)) 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))),(Initialize s)) = a =0_goto 3 by A3, A6;

A8: Comput ((P +* (while=0 (a,I))),(Initialize s),(0 + 1)) = Following ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),0))) by EXTPRO_1:3

.= Exec ((a =0_goto 3),(Initialize s)) by A7 ;

A9: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),1)) = 0 + 1 by A1, A3, A8, A5, SCMFSA_2:70;

A10: (P +* (while=0 (a,I))) /. (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),1))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),1))) by PBOOLE:143;

(P +* (while=0 (a,I))) . 1 = (while=0 (a,I)) . 1 by A4, FUNCT_4:13

.= goto 2 by SCMFSA_X:10 ;

then A11: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),1))) = goto 2 by A9, A10;

A12: Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + 1)) = Following ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),1))) by EXTPRO_1:3

.= Exec ((goto 2),(Comput ((P +* (while=0 (a,I))),(Initialize s),1))) by A11 ;

A13: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),2)) = 2 by A12, SCMFSA_2:69;

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))),(Initialize s),2))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),2))) by PBOOLE:143;

(P +* (while=0 (a,I))) . 2 = (while=0 (a,I)) . 2 by A14, FUNCT_4:13

.= goto ((card I) + 4) by SCMFSA_X:12 ;

then A17: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),2))) = goto ((card I) + 4) by A13, A16;

A18: Comput ((P +* (while=0 (a,I))),(Initialize s),(2 + 1)) = Following ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),2))) by EXTPRO_1:3

.= Exec ((goto ((card I) + 4)),(Comput ((P +* (while=0 (a,I))),(Initialize s),2))) by A17 ;

A19: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),3)) = (card I) + 4 by A18, SCMFSA_2:69;

A20: (P +* (while=0 (a,I))) /. (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),3))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),3))) by PBOOLE:143;

(P +* (while=0 (a,I))) . ((card I) + 4) = (while=0 (a,I)) . ((card I) + 4) by A15, FUNCT_4:13

.= halt SCM+FSA by SCMFSA_X:11 ;

then CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),3))) = halt SCM+FSA by A19, A20;

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