let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being Program of
for a being read-write Int-Location st s . a <= 0 holds
( while>0 (a,I) is_halting_on s,P & while>0 (a,I) is_closed_on s,P )
let s be State of SCM+FSA; :: thesis: for I being Program of
for a being read-write Int-Location st s . a <= 0 holds
( while>0 (a,I) is_halting_on s,P & while>0 (a,I) is_closed_on s,P )
let I be Program of ; :: thesis: for a being read-write Int-Location st s . a <= 0 holds
( while>0 (a,I) is_halting_on s,P & while>0 (a,I) is_closed_on s,P )
let a be read-write Int-Location; :: thesis: ( s . a <= 0 implies ( while>0 (a,I) is_halting_on s,P & while>0 (a,I) is_closed_on s,P ) )
assume A1: s . a <= 0 ; :: thesis: ( while>0 (a,I) is_halting_on s,P & while>0 (a,I) is_closed_on s,P )
set i = a >0_goto 4;
set s1 = Initialize s;
set P1 = P +* (while>0 (a,I));
IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
then A2: IC in dom (Start-At (0,SCM+FSA)) ;
A3: IC (Initialize s) = IC (Start-At (0,SCM+FSA)) by A2, FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
set loc5 = (card I) + 5;
set s5 = Comput ((P +* (while>0 (a,I))),(Initialize s),4);
set s4 = Comput ((P +* (while>0 (a,I))),(Initialize s),3);
set s3 = 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 Th10;
A5: 2 in dom (while>0 (a,I)) by Th32;
not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
then A6: (Initialize s) . a = s . a by FUNCT_4:11;
A7: (P +* (while>0 (a,I))) /. (IC (Initialize s)) = (P +* (while>0 (a,I))) . (IC (Initialize s)) by PBOOLE:143;
A8: 0 in dom (while>0 (a,I)) by Th10;
then (P +* (while>0 (a,I))) . 0 = (while>0 (a,I)) . 0 by FUNCT_4:13
.= a >0_goto 4 by Th11 ;
then A9: CurInstr ((P +* (while>0 (a,I))),(Initialize s)) = a >0_goto 4 by A3, A7;
A10: 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
.= Following ((P +* (while>0 (a,I))),(Initialize s))
.= Exec ((a >0_goto 4),(Initialize s)) by A9 ;
A11: IC (Comput ((P +* (while>0 (a,I))),(Initialize s),1)) = succ 0 by A1, A3, A10, A6, SCMFSA_2:71
.= 0 + 1 ;
A12: (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 Th11 ;
then A13: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),1))) = goto 2 by A11, A12;
A14: 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 A13 ;
A15: IC (Comput ((P +* (while>0 (a,I))),(Initialize s),2)) = 2 by A14, SCMFSA_2:69;
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 A5, FUNCT_4:13
.= goto 3 by Th36 ;
then A17: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),2))) = goto 3 by A15, 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 3),(Comput ((P +* (while>0 (a,I))),(Initialize s),2))) by A17 ;
A19: IC (Comput ((P +* (while>0 (a,I))),(Initialize s),3)) = 3 by A18, SCMFSA_2:69;
A20: 3 in dom (while>0 (a,I)) by Th32;
A21: (card I) + 5 in dom (while>0 (a,I)) by Th33;
A22: (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))) . 3 = (while>0 (a,I)) . 3 by A20, FUNCT_4:13
.= goto ((card I) + 5) by Th35 ;
then A23: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),3))) = goto ((card I) + 5) by A19, A22;
A24: Comput ((P +* (while>0 (a,I))),(Initialize s),(3 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),3))) by EXTPRO_1:3
.= Exec ((goto ((card I) + 5)),(Comput ((P +* (while>0 (a,I))),(Initialize s),3))) by A23 ;
A25: IC (Comput ((P +* (while>0 (a,I))),(Initialize s),4)) = (card I) + 5 by A24, SCMFSA_2:69;
A26: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(Initialize s),4))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(Initialize s),4))) by PBOOLE:143;
(P +* (while>0 (a,I))) . ((card I) + 5) = (while>0 (a,I)) . ((card I) + 5) by A21, FUNCT_4:13
.= halt SCM+FSA by Th34 ;
then A27: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),4))) = halt SCM+FSA by A25, A26;
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: while>0 (a,I) is_closed_on s,P

now :: thesis: for k being Element of NAT holds IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I))

let k be Element of NAT ; :: thesis: IC (Comput ((P +* (while>0 (a,I))),(Initialize s),b₁)) in dom (while>0 (a,I))
A28: ( k <= 3 or k >= 3 + 1 ) by NAT_1:13;

per cases ( k = 0 or k = 1 or k = 2 or k = 3 or k >= 4 ) by A28, NAT_1:27;

suppose k = 0 ; :: thesis: IC (Comput ((P +* (while>0 (a,I))),(Initialize s),b₁)) in dom (while>0 (a,I))

hence IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) by A8, A3, EXTPRO_1:2; :: thesis: verum

end;

suppose k = 1 ; :: thesis: IC (Comput ((P +* (while>0 (a,I))),(Initialize s),b₁)) in dom (while>0 (a,I))

hence IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) by A11, Th10; :: thesis: verum

end;

suppose k = 2 ; :: thesis: IC (Comput ((P +* (while>0 (a,I))),(Initialize s),b₁)) in dom (while>0 (a,I))

hence IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) by A15, Th32; :: thesis: verum

end;

suppose k = 3 ; :: thesis: IC (Comput ((P +* (while>0 (a,I))),(Initialize s),b₁)) in dom (while>0 (a,I))

hence IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) by A19, Th32; :: thesis: verum

end;

suppose k >= 4 ; :: thesis: IC (Comput ((P +* (while>0 (a,I))),(Initialize s),b₁)) in dom (while>0 (a,I))

hence IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) by A21, A25, A27, EXTPRO_1:5; :: thesis: verum

end;

end;

end;

hence while>0 (a,I) is_closed_on s,P by SCMFSA7B:def 6; :: thesis: verum