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 & while>0 (a,I) is_closed_on s )
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 & while>0 (a,I) is_closed_on s )
let a be read-write Int-Location ; :: thesis: ( s . a <= 0 implies ( while>0 (a,I) is_halting_on s & while>0 (a,I) is_closed_on s ) )
assume A1: s . a <= 0 ; :: thesis: ( while>0 (a,I) is_halting_on s & while>0 (a,I) is_closed_on s )
set i = a >0_goto 4;
set s1 = s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)));
A2: IC SCM+FSA in dom ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
A3: IC (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = IC ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by A2, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
set loc5 = (card I) + 5;
set s5 = Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4);
set s4 = Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3);
set s3 = Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2);
set s2 = Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1);
A4: 1 in dom (while>0 (a,I)) by Th10;
A5: 2 in dom (while>0 (a,I)) by Th37;
not a in dom ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by SCMFSA6B:12;
then A6: (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . a = s . a by FUNCT_4:12;
while>0 (a,I) c= (while>0 (a,I)) +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
then A7: dom (while>0 (a,I)) c= dom ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
Y: (ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) /. (IC (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) = (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . (IC (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) by COMPOS_1:38;
A8: 0 in dom (while>0 (a,I)) by Th10;
then (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . 0 = ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . 0 by A7, FUNCT_4:14
.= (while>0 (a,I)) . 0 by A8, COMPOS_1:145
.= a >0_goto 4 by Th11 ;
then A9: CurInstr ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) = a >0_goto 4 by A3, Y;
A10: Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(0 + 1)) = Following ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),0))) by EXTPRO_1:4
.= Following ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) by EXTPRO_1:3
.= Exec ((a >0_goto 4),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) by A9 ;
A11: IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) . (IC SCM+FSA)
.= succ 0 by A1, A3, A10, A6, SCMFSA_2:97
.= 0 + 1 ;
Y: (ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))) /. (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) . (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))) by COMPOS_1:38;
(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) . 1 = (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . 1 by AMI_1:54
.= ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . 1 by A7, A4, FUNCT_4:14
.= (while>0 (a,I)) . 1 by A4, COMPOS_1:145
.= goto 2 by Th11 ;
then A12: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))) = goto 2 by A11, Y;
T: ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) by AMI_1:123;
A13: Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + 1)) = Following ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))) by EXTPRO_1:4
.= Exec ((goto 2),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))) by A12, T ;
A14: IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) . (IC SCM+FSA)
.= 2 by A13, SCMFSA_2:95 ;
Y: (ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) /. (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) . (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) by COMPOS_1:38;
(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) . 2 = (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . 2 by AMI_1:54
.= ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . 2 by A7, A5, FUNCT_4:14
.= (while>0 (a,I)) . 2 by A5, COMPOS_1:145
.= goto 3 by Th41 ;
then A15: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) = goto 3 by A14, Y;
T: ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) by AMI_1:123;
A16: Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(2 + 1)) = Following ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) by EXTPRO_1:4
.= Exec ((goto 3),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) by A15, T ;
A17: IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) . (IC SCM+FSA)
.= 3 by A16, SCMFSA_2:95 ;
A18: 3 in dom (while>0 (a,I)) by Th37;
A19: (card I) + 5 in dom (while>0 (a,I)) by Th38;
Y: (ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) /. (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) . (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) by COMPOS_1:38;
(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) . 3 = (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . 3 by AMI_1:54
.= ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . 3 by A7, A18, FUNCT_4:14
.= (while>0 (a,I)) . 3 by A18, COMPOS_1:145
.= goto ((card I) + 5) by Th40 ;
then A20: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) = goto ((card I) + 5) by A17, Y;
T: ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) by AMI_1:123;
A21: Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(3 + 1)) = Following ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) by EXTPRO_1:4
.= Exec ((goto ((card I) + 5)),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) by A20, T ;
A22: IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) . (IC SCM+FSA)
.= (card I) + 5 by A21, SCMFSA_2:95 ;
Y: (ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4))) /. (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4))) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) . (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4))) by COMPOS_1:38;
TX: ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) by AMI_1:123;
(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) . ((card I) + 5) = (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . ((card I) + 5) by AMI_1:54
.= ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . ((card I) + 5) by A7, A19, FUNCT_4:14
.= (while>0 (a,I)) . ((card I) + 5) by A19, COMPOS_1:145
.= halt SCM+FSA by Th39 ;
then A23: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4))) = halt SCM+FSA by A22, Y;
then ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) halts_on s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by TX, EXTPRO_1:30;
hence while>0 (a,I) is_halting_on s by SCMFSA7B:def 8; :: thesis: while>0 (a,I) is_closed_on s
TX: ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) by AMI_1:123;
now
let k be Element of NAT ; :: thesis: IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while>0 (a,I))
A24: ( 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 A24, NAT_1:28;
suppose k = 0 ; :: thesis: IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while>0 (a,I))
hence IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while>0 (a,I)) by A8, A3, EXTPRO_1:3; :: thesis: verum
end;
suppose k = 1 ; :: thesis: IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while>0 (a,I))
hence IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while>0 (a,I)) by A11, Th10; :: thesis: verum
end;
suppose k = 2 ; :: thesis: IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while>0 (a,I))
hence IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while>0 (a,I)) by A14, Th37; :: thesis: verum
end;
suppose k = 3 ; :: thesis: IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while>0 (a,I))
hence IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while>0 (a,I)) by A17, Th37; :: thesis: verum
end;
suppose k >= 4 ; :: thesis: IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while>0 (a,I))
hence IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while>0 (a,I)) by A19, A22, A23, TX, EXTPRO_1:6; :: thesis: verum
end;
end;
end;
hence while>0 (a,I) is_closed_on s by SCMFSA7B:def 7; :: thesis: verum