let I be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) & s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting & LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 & I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s )
let s be State of SCM+FSA ; :: thesis: ( I is_closed_on s & I is_halting_on s implies ( IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) & s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting & LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 & I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s ) )
assume A1: I is_closed_on s ; :: thesis: ( not I is_halting_on s or ( IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) & s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting & LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 & I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s ) )
assume A2: I is_halting_on s ; :: thesis: ( IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) & s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting & LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 & I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s )
set s1 = s +* (I +* (Start-At (insloc 0 )));
set s2 = s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )));
I ';' (Stop SCM+FSA ) c= (I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )) by Th9;
then A3: dom (I ';' (Stop SCM+FSA )) c= dom ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
card (I ';' (Stop SCM+FSA )) = (card I) + 1 by Th17, SCMFSA6A:61;
then card I < card (I ';' (Stop SCM+FSA )) by NAT_1:13;
then A4: insloc (card I) in dom (I ';' (Stop SCM+FSA )) by SCMFSA6A:15;
A5: dom (ProgramPart (Stop SCM+FSA )) = dom (Stop SCM+FSA ) by AMI_1:105;
then insloc (0 + (card I)) in { (m + (card I)) where m is Element of NAT : m in dom (ProgramPart (Stop SCM+FSA )) } by Th16;
then A6: insloc (0 + (card I)) in dom (ProgramPart (Relocated (Stop SCM+FSA ),(card I))) by SCMFSA_5:3;
A7: ProgramPart (Relocated (Stop SCM+FSA ),(card I)) c= Relocated (Stop SCM+FSA ),(card I) by RELAT_1:88;
A8: ( DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) & IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) ) by A1, A2, Th42;
hence ( IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) ) by A1, A2, Th36; :: thesis: ( s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting & LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 & I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s )
A9: (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . (insloc (card I)) = ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) . (insloc (card I)) by A3, A4, FUNCT_4:14
.= (I ';' (Stop SCM+FSA )) . (insloc (card I)) by A4, SCMFSA6B:7
.= (ProgramPart (Relocated (Stop SCM+FSA ),(card I))) . (insloc (card I)) by A6, FUNCT_4:14
.= (Relocated (Stop SCM+FSA ),(card I)) . (insloc (0 + (card I))) by A6, A7, GRFUNC_1:8
.= IncAddr (halt SCM+FSA ),(card I) by A5, Th16A, SCMFSA_5:7, SCMNORM:2
.= halt SCM+FSA by SCMFSA_4:8 ;
A10: CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) . (insloc (card I)) by A1, A2, A8, Th36
.= halt SCM+FSA by A9, AMI_1:54 ;
hence A11: s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting by AMI_1:def 20; :: thesis: ( LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 & I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s )
now
let k be Element of NAT ; :: thesis: ( k < (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 implies CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA )
assume k < (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 ; :: thesis: CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA
then A12: k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) by NAT_1:13;
then CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA by A1, A2, Th35;
hence CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA by A1, A2, A12, Th42; :: thesis: verum
end;
then for k being Element of NAT st CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA holds
(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 <= k ;
hence LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 by A10, A11, AMI_1:def 46; :: thesis: ( I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s )
defpred S1[ Element of NAT ] means ( ( LifeSpan (s +* (I +* (Start-At (insloc 0 )))) < $1 implies IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),$1) = insloc (card I) ) & IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),$1) in dom (I ';' (Stop SCM+FSA )) );
A13: now
let k be Element of NAT ; :: thesis: ( k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) implies IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) in dom (I ';' (Stop SCM+FSA )) )
assume A14: k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) ; :: thesis: IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) in dom (I ';' (Stop SCM+FSA ))
then IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k) by A1, A2, Th35, AMI_1:121;
then A15: ( IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) & IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) in dom I ) by A1, A2, A14, Th42, SCMFSA7B:def 7;
dom I c= dom (I ';' (Stop SCM+FSA )) by SCMFSA6A:56;
hence IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) in dom (I ';' (Stop SCM+FSA )) by A15; :: thesis: verum
end;
card (I ';' (Stop SCM+FSA )) = (card I) + 1 by Th17, SCMFSA6A:61;
then A16: (card I) + 0 < card (I ';' (Stop SCM+FSA )) by XREAL_1:8;
then A17: insloc (card I) in dom (I ';' (Stop SCM+FSA )) by SCMFSA6A:15;
A18: S1[ 0 ] by A13, NAT_1:2;
A19: now
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[b1 + 1] )
assume A20: S1[k] ; :: thesis: S1[b1 + 1]
per cases ( k < LifeSpan (s +* (I +* (Start-At (insloc 0 )))) or k = LifeSpan (s +* (I +* (Start-At (insloc 0 )))) or k > LifeSpan (s +* (I +* (Start-At (insloc 0 )))) ) by XXREAL_0:1;
suppose k < LifeSpan (s +* (I +* (Start-At (insloc 0 )))) ; :: thesis: S1[b1 + 1]
then k + 1 <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) by NAT_1:13;
hence S1[k + 1] by A13; :: thesis: verum
end;
suppose k = LifeSpan (s +* (I +* (Start-At (insloc 0 )))) ; :: thesis: S1[b1 + 1]
hence S1[k + 1] by A1, A2, A8, A17, Th36; :: thesis: verum
end;
suppose A21: k > LifeSpan (s +* (I +* (Start-At (insloc 0 )))) ; :: thesis: S1[b1 + 1]
A22: now
assume k + 1 > LifeSpan (s +* (I +* (Start-At (insloc 0 )))) ; :: thesis: IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(k + 1)) = insloc (card I)
A23: CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA by A20, A21, A9, AMI_1:54;
thus IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(k + 1)) = IC (Following (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k)) by AMI_1:14
.= insloc (card I) by A23, A20, A21, AMI_1:def 8 ; :: thesis: verum
end;
k + 1 > k + 0 by XREAL_1:8;
hence S1[k + 1] by A16, A21, A22, SCMFSA6A:15, XXREAL_0:2; :: thesis: verum
end;
end;
end;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A18, A19);
 hence I ';' (Stop SCM+FSA ) is_closed_on s by SCMFSA7B:def 7; :: thesis: I ';' (Stop SCM+FSA ) is_halting_on s
thus I ';' (Stop SCM+FSA ) is_halting_on s by A11, SCMFSA7B:def 8; :: thesis: verum