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 SF_MASTR:65;
A3: IC (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) . (IC SCM+FSA )
.= ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) . (IC SCM+FSA ) by A2, FUNCT_4:14
.= 0 by SF_MASTR:66 ;
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, SCMFSA6B:7
.= 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 AMI_1:14
.= Following (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) by AMI_1:13
.= 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, SCMFSA6B:7
.= 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 AMI_1:14
.= 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, SCMFSA6B:7
.= 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 AMI_1:14
.= 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, SCMFSA6B:7
.= 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 AMI_1:14
.= 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, SCMFSA6B:7
.= 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, AMI_1:146;
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, AMI_1:13; :: 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, AMI_1:52; :: thesis: verum
end;
end;
end;
hence while>0 a,I is_closed_on s by SCMFSA7B:def 7; :: thesis: verum