let s be State of SCM+FSA ; :: thesis: for I being keepInt0_1 Program of SCM+FSA st s +* I is halting holds
for J being InitClosed Program of SCM+FSA st Initialized (I ';' J) c= s holds
for k being Element of NAT holds (Computation ((Result (s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Computation ((Result (s +* I)) +* (Initialized J)),k)) + (card I))), Computation (s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT
let I be keepInt0_1 Program of SCM+FSA ; :: thesis: ( s +* I is halting implies for J being InitClosed Program of SCM+FSA st Initialized (I ';' J) c= s holds
for k being Element of NAT holds (Computation ((Result (s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Computation ((Result (s +* I)) +* (Initialized J)),k)) + (card I))), Computation (s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT )
assume A1: s +* I is halting ; :: thesis: for J being InitClosed Program of SCM+FSA st Initialized (I ';' J) c= s holds
for k being Element of NAT holds (Computation ((Result (s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Computation ((Result (s +* I)) +* (Initialized J)),k)) + (card I))), Computation (s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT
let J be InitClosed Program of SCM+FSA ; :: thesis: ( Initialized (I ';' J) c= s implies for k being Element of NAT holds (Computation ((Result (s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Computation ((Result (s +* I)) +* (Initialized J)),k)) + (card I))), Computation (s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT )
assume A2: Initialized (I ';' J) c= s ; :: thesis: for k being Element of NAT holds (Computation ((Result (s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Computation ((Result (s +* I)) +* (Initialized J)),k)) + (card I))), Computation (s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT
set SA0 = Start-At (insloc 0 );
set ISA0 = Initialized I;
set sISA0 = s +* (Initialized I);
set RI = Result (s +* (Initialized I));
set JSA0 = Initialized J;
set RIJ = (Result (s +* (Initialized I))) +* (Initialized J);
set sIJSA0 = s +* (Initialized (I ';' J));
A3: s = s +* (Initialized (I ';' J)) by A2, FUNCT_4:79;
A5: Directed I c= I ';' J by SCMFSA6A:55;
A6: s +* (Initialized (I ';' J)) = s +* ((I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) by FUNCT_4:15
.= (s +* (I ';' J)) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:15 ;
then A7: s +* (Initialized (I ';' J)) = (s +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) +* (I ';' J) by Th19;
then A8: I ';' J c= s by A3, FUNCT_4:26;
then A9: Directed I c= s by A5, XBOOLE_1:1;
A10: ((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )) c= s by A3, A6, FUNCT_4:26;
A11: s +* (Initialized I) = s +* (I +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) by FUNCT_4:15
.= (s +* I) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:15
.= (s +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) +* I by Th19
.= s +* I by A10, FUNCT_4:79 ;
A12: Initialized I c= s +* (Initialized I) by FUNCT_4:26;
A13: s +* (Initialized (I ';' J)) = s +* (I ';' J) by A7, A10, FUNCT_4:79;
A14: now
set s1 = ((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)));
set s2 = Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 );
thus IC (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)))) = (IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I) by AMI_1:111
.= (IC (((Result (s +* (Initialized I))) +* (J +* ((intloc 0 ) .--> 1))) +* (Start-At (insloc 0 )))) + (card I) by FUNCT_4:15
.= (insloc 0 ) + (card I) by AMI_1:111
.= IC (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) by A1, A3, A6, A9, A11, Th21, FUNCT_4:26 ; :: thesis: ( ( for a being Int-Location holds (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)))) . a = (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . a ) & ( for f being FinSeq-Location holds (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)))) . f = (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . f ) )
A15: DataPart (Computation s,(LifeSpan (s +* (Initialized I)))) = DataPart (Computation s,((LifeSpan (s +* (Initialized I))) + 1)) by A1, A3, A6, A9, A11, Th22, FUNCT_4:26;
hereby :: thesis: for f being FinSeq-Location holds (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)))) . f = (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . f
let a be Int-Location ; :: thesis: (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)))) . b1 = (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . b1
not a in dom (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I))) by SCMFSA6B:9;
then A16: (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)))) . a = ((Result (s +* (Initialized I))) +* (Initialized J)) . a by FUNCT_4:12;
A17: (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) . a = (Computation (s +* (Initialized (I ';' J))),(LifeSpan (s +* (Initialized I)))) . a by A1, A11, Th24, SCMFSA6A:30
.= (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . a by A3, A15, SCMFSA6A:38 ;
per cases ( a <> intloc 0 or a = intloc 0 ) ;
suppose a <> intloc 0 ; :: thesis: (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)))) . b1 = (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . b1
then not a in dom (Initialized J) by SCMFSA6A:48;
hence (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)))) . a = (Result (s +* (Initialized I))) . a by A16, FUNCT_4:12
.= (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . a by A1, A11, A17, AMI_1:122 ;
:: thesis: verum
end;
suppose A18: a = intloc 0 ; :: thesis: (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)))) . b1 = (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . b1
then a in dom (Initialized J) by SCMFSA6A:45;
hence (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)))) . a = (Initialized J) . a by A16, FUNCT_4:14
.= 1 by A18, SCMFSA6A:46
.= (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . a by A12, A17, A18, Def3 ;
:: thesis: verum
end;
end;
end;
let f be FinSeq-Location ; :: thesis: (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)))) . f = (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . f
A19: not f in dom (Initialized J) by SCMFSA6A:49;
not f in dom (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I))) by SCMFSA6B:10;
hence (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)))) . f = ((Result (s +* (Initialized I))) +* (Initialized J)) . f by FUNCT_4:12
.= (Result (s +* (Initialized I))) . f by A19, FUNCT_4:12
.= (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) . f by A1, A11, AMI_1:122
.= (Computation (s +* (Initialized (I ';' J))),(LifeSpan (s +* (Initialized I)))) . f by A1, A11, Th24, SCMFSA6A:31
.= (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . f by A3, A15, SCMFSA6A:38 ;
:: thesis: verum
end;
defpred S1[ Element of NAT ] means (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),$1) +* (Start-At ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),$1)) + (card I))), Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + $1) equal_outside NAT ;
Computation ((Result (s +* (Initialized I))) +* (Initialized J)),0 = (Result (s +* (Initialized I))) +* (Initialized J) by AMI_1:13;
then A20: S1[ 0 ] by A14, SCMFSA6A:28;
A21: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A22: (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I))), Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k) equal_outside NAT ; :: thesis: S1[k + 1]
set k1 = k + 1;
set CRk = Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k;
set CRSk = (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I)));
set CIJk = Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k);
set CRk1 = Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1);
set CRSk1 = (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)));
set CIJk1 = Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1));
A23: IncAddr (CurInstr (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)),(card I) = CurInstr (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k))
proof
A24: now
thus CurInstr (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)) = (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)) . (IC ((Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I))))) by A22, AMI_1:121
.= (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)) . ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I)) by AMI_1:111 ; :: thesis: verum
end;
reconsider ii = IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k) as Element of NAT by ORDINAL1:def 13;
Initialized J c= (Result (s +* (Initialized I))) +* (Initialized J) by FUNCT_4:26;
then A25: IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k) in dom J by Def1;
then A26: ii in dom (IncAddr J,(card I)) by SCMFSA_4:def 6;
then A27: (Shift (IncAddr J,(card I)),(card I)) . ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I)) = (IncAddr J,(card I)) . ii by VALUED_1:def 12
.= IncAddr (pi J,ii),(card I) by A25, SCMFSA_4:24 ;
ProgramPart (Relocated J,(card I)) c= I ';' J by FUNCT_4:26;
then A28: ProgramPart (Relocated J,(card I)) c= s +* (Initialized (I ';' J)) by A3, A8, XBOOLE_1:1;
A29: now
thus ProgramPart (Relocated J,(card I)) = IncAddr [(Shift (ProgramPart J),(card I))],(card I) by SCMFSA_5:2
.= IncAddr (Shift J,(card I)),(card I) by AMI_1:105
.= Shift (IncAddr J,(card I)),(card I) by SCMFSA_4:35 ; :: thesis: verum
end;
dom (Shift (IncAddr J,(card I)),(card I)) = { (il + (card I)) where il is Element of NAT : il in dom (IncAddr J,(card I)) } by VALUED_1:def 12;
then A30: (IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I) in dom (Shift (IncAddr J,(card I)),(card I)) by A26;
A31: now
(Result (s +* (Initialized I))) +* (Initialized J) = (Result (s +* (Initialized I))) +* (J +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) by FUNCT_4:15
.= ((Result (s +* (Initialized I))) +* J) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:15
.= ((Result (s +* (Initialized I))) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) +* J by Th19 ;
hence J c= Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k by AMI_1:81, FUNCT_4:26; :: thesis: verum
end;
pi J,ii = J . (IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) by A25, AMI_1:def 47
.= (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k) . (IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) by A25, A31, GRFUNC_1:8 ;
hence IncAddr (CurInstr (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)),(card I) = (s +* (Initialized (I ';' J))) . ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I)) by A27, A28, A29, A30, GRFUNC_1:8
.= CurInstr (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)) by A24, AMI_1:54 ;
:: thesis: verum
end;
A32: now
Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1)) = Computation (s +* (Initialized (I ';' J))),((((LifeSpan (s +* (Initialized I))) + 1) + k) + 1) ;
then Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1)) = Following (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)) by AMI_1:14;
hence Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1)) = Exec (CurInstr (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k))),(Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)) ; :: thesis: verum
end;
Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k),(Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I))) equal_outside NAT by A22, FUNCT_7:28;
then Exec (CurInstr (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k))),(Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)), Exec (IncAddr (CurInstr (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)),(card I)),((Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I)))) equal_outside NAT by A23, SCMFSA6A:32;
then A33: Exec (CurInstr (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k))),(Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)),(Following (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) +* (Start-At ((IC (Following (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k))) + (card I))) equal_outside NAT by SCMFSA_4:28;
A34: now
IC ((Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)))) = (IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I) by AMI_1:111
.= (IC (Following (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k))) + (card I) by AMI_1:14 ;
hence IC ((Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)))) = IC ((Following (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) +* (Start-At ((IC (Following (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k))) + (card I)))) by AMI_1:111
.= IC (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1))) by A32, A33, AMI_1:121 ;
:: thesis: verum
end;
A35: now
let a be Int-Location ; :: thesis: ((Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)))) . a = (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1))) . a
thus ((Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)))) . a = (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) . a by SCMFSA_3:11
.= (Following (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) . a by AMI_1:14
.= ((Following (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) +* (Start-At ((IC (Following (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k))) + (card I)))) . a by SCMFSA_3:11
.= (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1))) . a by A32, A33, SCMFSA6A:30 ; :: thesis: verum
end;
now
let f be FinSeq-Location ; :: thesis: ((Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)))) . f = (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1))) . f
thus ((Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)))) . f = (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) . f by SCMFSA_3:12
.= (Following (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) . f by AMI_1:14
.= ((Following (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k)) +* (Start-At ((IC (Following (Computation ((Result (s +* (Initialized I))) +* (Initialized J)),k))) + (card I)))) . f by SCMFSA_3:12
.= (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1))) . f by A32, A33, SCMFSA6A:31 ; :: thesis: verum
end;
hence S1[k + 1] by A34, A35, SCMFSA6A:28; :: thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A20, A21);
 hence for k being Element of NAT holds (Computation ((Result (s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Computation ((Result (s +* I)) +* (Initialized J)),k)) + (card I))), Computation (s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT by A11, A13; :: thesis: verum