let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA
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 SCM+FSA
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 SCM+FSA; :: 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 = s +* (Initialize (while>0 (a,I)));
set P1 = P +* (while>0 (a,I));
A2: ProgramPart (while>0 (a,I)) = while>0 (a,I) by RELAT_1:209;
A3: IC in dom (Initialize (while>0 (a,I))) by COMPOS_1:141;
A4: IC (s +* (Initialize (while>0 (a,I)))) = IC (Initialize (while>0 (a,I))) by A3, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
set loc5 = (card I) + 5;
set s5 = Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),4);
set s4 = Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3);
set s3 = Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2);
set s2 = Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1);
A5: 1 in dom (while>0 (a,I)) by Th10;
A6: 2 in dom (while>0 (a,I)) by Th37;
not a in dom (Initialize (while>0 (a,I))) by SCMFSA6B:12;
then A7: (s +* (Initialize (while>0 (a,I)))) . a = s . a by FUNCT_4:12;
A8: (P +* (while>0 (a,I))) /. (IC (s +* (Initialize (while>0 (a,I))))) = (P +* (while>0 (a,I))) . (IC (s +* (Initialize (while>0 (a,I))))) by PBOOLE:158;
A9: 0 in dom (while>0 (a,I)) by Th10;
then (P +* (while>0 (a,I))) . 0 = (while>0 (a,I)) . 0 by FUNCT_4:14
.= (while>0 (a,I)) . 0
.= a >0_goto 4 by Th11 ;
then A10: CurInstr ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I))))) = a >0_goto 4 by A4, A8;
A11: Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(0 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),0))) by EXTPRO_1:4
.= Following ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I))))) by EXTPRO_1:3
.= Exec ((a >0_goto 4),(s +* (Initialize (while>0 (a,I))))) by A10 ;
A12: IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1)) = (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1)) . (IC )
.= succ 0 by A1, A4, A11, A7, SCMFSA_2:97
.= 0 + 1 ;
A13: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1))) by PBOOLE:158;
(P +* (while>0 (a,I))) . 1 = (P +* (while>0 (a,I))) . 1
.= (while>0 (a,I)) . 1 by A5, FUNCT_4:14
.= (while>0 (a,I)) . 1
.= goto 2 by Th11 ;
then A14: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1))) = goto 2 by A12, A13;
A15: Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(1 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1))) by EXTPRO_1:4
.= Exec ((goto 2),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1))) by A14 ;
A16: IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2)) = (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2)) . (IC )
.= 2 by A15, SCMFSA_2:95 ;
A17: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2))) by PBOOLE:158;
(P +* (while>0 (a,I))) . 2 = (P +* (while>0 (a,I))) . 2
.= (while>0 (a,I)) . 2 by A6, FUNCT_4:14
.= (while>0 (a,I)) . 2
.= goto 3 by Th41 ;
then A18: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2))) = goto 3 by A16, A17;
A19: Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(2 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2))) by EXTPRO_1:4
.= Exec ((goto 3),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2))) by A18 ;
A20: IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3)) = (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3)) . (IC )
.= 3 by A19, SCMFSA_2:95 ;
A21: 3 in dom (while>0 (a,I)) by Th37;
A22: (card I) + 5 in dom (while>0 (a,I)) by Th38;
A23: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3))) by PBOOLE:158;
(P +* (while>0 (a,I))) . 3 = (P +* (while>0 (a,I))) . 3
.= (while>0 (a,I)) . 3 by A21, FUNCT_4:14
.= (while>0 (a,I)) . 3
.= goto ((card I) + 5) by Th40 ;
then A24: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3))) = goto ((card I) + 5) by A20, A23;
A25: Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(3 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3))) by EXTPRO_1:4
.= Exec ((goto ((card I) + 5)),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3))) by A24 ;
A26: IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),4)) = (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),4)) . (IC )
.= (card I) + 5 by A25, SCMFSA_2:95 ;
A27: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),4))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),4))) by PBOOLE:158;
(P +* (while>0 (a,I))) . ((card I) + 5) = (P +* (while>0 (a,I))) . ((card I) + 5)
.= (while>0 (a,I)) . ((card I) + 5) by A22, FUNCT_4:14
.= halt SCM+FSA by Th39 ;
then A28: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),4))) = halt SCM+FSA by A26, A27;
then P +* (while>0 (a,I)) halts_on s +* (Initialize (while>0 (a,I))) by EXTPRO_1:30;
hence while>0 (a,I) is_halting_on s,P by SCMFSA7B:def 8, A2; :: thesis: while>0 (a,I) is_closed_on s,P

now

let k be Element of NAT ; :: thesis: IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),b₁)) in dom (while>0 (a,I))
A29: ( 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 A29, NAT_1:28;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

hence IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),k)) in dom (while>0 (a,I)) by A22, A26, A28, EXTPRO_1:6; :: thesis: verum

end;

end;

end;

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