let I be InitHalting keepInt0_1 Program of SCM+FSA ; :: thesis: for J being InitHalting Program of SCM+FSA
for s being State of SCM+FSA st Initialized (I ';' J) c= s holds
( IC (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I) & DataPart (Computation s,((LifeSpan (s +* I)) + 1)) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) & ProgramPart (Relocated J,(card I)) c= Computation s,((LifeSpan (s +* I)) + 1) & (Computation s,((LifeSpan (s +* I)) + 1)) . (intloc 0 ) = 1 & s is halting & LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) & ( J is keeping_0 implies (Result s) . (intloc 0 ) = 1 ) )
let J be InitHalting Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA st Initialized (I ';' J) c= s holds
( IC (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I) & DataPart (Computation s,((LifeSpan (s +* I)) + 1)) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) & ProgramPart (Relocated J,(card I)) c= Computation s,((LifeSpan (s +* I)) + 1) & (Computation s,((LifeSpan (s +* I)) + 1)) . (intloc 0 ) = 1 & s is halting & LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) & ( J is keeping_0 implies (Result s) . (intloc 0 ) = 1 ) )
let s be State of SCM+FSA ; :: thesis: ( Initialized (I ';' J) c= s implies ( IC (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I) & DataPart (Computation s,((LifeSpan (s +* I)) + 1)) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) & ProgramPart (Relocated J,(card I)) c= Computation s,((LifeSpan (s +* I)) + 1) & (Computation s,((LifeSpan (s +* I)) + 1)) . (intloc 0 ) = 1 & s is halting & LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) & ( J is keeping_0 implies (Result s) . (intloc 0 ) = 1 ) ) )
set s1 = s +* I;
set s3 = (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J);
set m1 = LifeSpan (s +* I);
set m3 = LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J));
set D = Int-Locations \/ FinSeq-Locations ;
assume A1: Initialized (I ';' J) c= s ; :: thesis: ( IC (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I) & DataPart (Computation s,((LifeSpan (s +* I)) + 1)) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) & ProgramPart (Relocated J,(card I)) c= Computation s,((LifeSpan (s +* I)) + 1) & (Computation s,((LifeSpan (s +* I)) + 1)) . (intloc 0 ) = 1 & s is halting & LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) & ( J is keeping_0 implies (Result s) . (intloc 0 ) = 1 ) )
then A2: Initialized I c= s +* I by SCMFSA6A:52;
A3: (I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) c= s by A1, FUNCT_4:15;
A4: s = s +* (Initialized (I ';' J)) by A1, FUNCT_4:79;
((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )) c= (I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then A5: ((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )) c= s by A3, XBOOLE_1:1;
then A6: s +* I = (s +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) +* I by FUNCT_4:79
.= (s +* I) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by Th19
.= s +* (I +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) by FUNCT_4:15
.= s +* (Initialized I) by FUNCT_4:15 ;
A7: s +* I is halting by A2, Th5;
A8: DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) +* (DataPart (Initialized J)) by FUNCT_4:75;

A9: now

let x be set ; :: thesis: ( x in dom (DataPart (Initialized J)) implies (DataPart (Initialized J)) . b₁ = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b₁ )
assume x in dom (DataPart (Initialized J)) ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b₁
then A10: x in (dom (Initialized J)) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90, SCMFSA_2:127;
then A11: ( x in dom (Initialized J) & x in Int-Locations \/ FinSeq-Locations ) by XBOOLE_0:def 4;

per cases ( x in dom J or x = intloc 0 or x = IC SCM+FSA ) by A11, SCMFSA6A:44;

suppose A12: x in dom J ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b₁

dom J c= NAT by RELAT_1:def 18;
then reconsider l = x as Instruction-Location of SCM+FSA by A12, AMI_1:def 4;
(DataPart (Initialized J)) . l = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . l by A11, SCMFSA6A:37;
hence (DataPart (Initialized J)) . x = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . x ; :: thesis: verum

end;

suppose A13: x = intloc 0 ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b₁

thus (DataPart (Initialized J)) . x = (Initialized J) . x by A11, FUNCT_1:72, SCMFSA_2:127
.= 1 by A13, SCMFSA6A:46
.= (Computation (s +* I),(LifeSpan (s +* I))) . x by A2, A13, Def3
.= (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . x by A11, FUNCT_1:72, SCMFSA_2:127 ; :: thesis: verum

end;

suppose x = IC SCM+FSA ; :: thesis: (DataPart (Initialized J)) . b₁ = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . b₁

hence (DataPart (Initialized J)) . x = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . x by A10, SCMFSA6A:37, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

Initialized J c= (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) by FUNCT_4:26;
then dom (Initialized J) c= dom ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by GRFUNC_1:8;
then A14: dom (Initialized J) c= the carrier of SCM+FSA by AMI_1:79;
dom (DataPart (Initialized J)) = (dom (Initialized J)) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90, SCMFSA_2:127;
then dom (DataPart (Initialized J)) c= the carrier of SCM+FSA /\ (Int-Locations \/ FinSeq-Locations ) by A14, XBOOLE_1:26;
then dom (DataPart (Initialized J)) c= (dom (Computation (s +* I),(LifeSpan (s +* I)))) /\ (Int-Locations \/ FinSeq-Locations ) by AMI_1:79;
then dom (DataPart (Initialized J)) c= dom (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) by RELAT_1:90, SCMFSA_2:127;
then DataPart (Initialized J) c= DataPart (Computation (s +* I),(LifeSpan (s +* I))) by A9, GRFUNC_1:8;
then DataPart (Computation (s +* I),(LifeSpan (s +* I))) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by A8, LATTICE2:8;
then A15: DataPart (Computation s,(LifeSpan (s +* I))) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by A4, A6, A7, Th24, SCMFSA6A:39;
A16: (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) is halting by Th5, FUNCT_4:26;
A17: dom (Directed I) = dom I by FUNCT_4:105;
A18: Directed I c= I ';' J by SCMFSA6A:55;
A19: I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
A20: (s +* I) +* (Directed I) = s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A17, FUNCT_4:20
.= (s +* (Initialized (I ';' J))) +* (Directed I) by A1, LATTICE2:8
.= s +* ((Initialized (I ';' J)) +* (Directed I)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by A18, A19, LATTICE2:8, XBOOLE_1:1
.= s by A1, LATTICE2:8 ;
then A21: Directed I c= s by FUNCT_4:26;
thus A22: IC (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I) by A5, A7, A20, Th21, FUNCT_4:26; :: thesis: ( DataPart (Computation s,((LifeSpan (s +* I)) + 1)) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) & ProgramPart (Relocated J,(card I)) c= Computation s,((LifeSpan (s +* I)) + 1) & (Computation s,((LifeSpan (s +* I)) + 1)) . (intloc 0 ) = 1 & s is halting & LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) & ( J is keeping_0 implies (Result s) . (intloc 0 ) = 1 ) )
thus A23: DataPart (Computation s,((LifeSpan (s +* I)) + 1)) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by A2, A5, A15, A21, Th5, Th22; :: thesis: ( ProgramPart (Relocated J,(card I)) c= Computation s,((LifeSpan (s +* I)) + 1) & (Computation s,((LifeSpan (s +* I)) + 1)) . (intloc 0 ) = 1 & s is halting & LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) & ( J is keeping_0 implies (Result s) . (intloc 0 ) = 1 ) )
reconsider m = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))) as Element of NAT ;
set s4 = Computation s,((LifeSpan (s +* I)) + 1);
A24: Initialized J c= (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) by FUNCT_4:26;
I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
then A25: I ';' J c= s by A1, XBOOLE_1:1;
ProgramPart (Relocated J,(card I)) c= I ';' J by FUNCT_4:26;
then ProgramPart (Relocated J,(card I)) c= s by A25, XBOOLE_1:1;
then A26: [(ProgramPart (Relocated J,(card I)))] c= Computation s,((LifeSpan (s +* I)) + 1) by AMI_1:81;
hence ProgramPart (Relocated J,(card I)) c= Computation s,((LifeSpan (s +* I)) + 1) ; :: thesis: ( (Computation s,((LifeSpan (s +* I)) + 1)) . (intloc 0 ) = 1 & s is halting & LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) & ( J is keeping_0 implies (Result s) . (intloc 0 ) = 1 ) )
A27: intloc 0 in dom (Initialized J) by SCMFSA6A:45;
intloc 0 in Int-Locations by SCMFSA_2:9;
then A28: intloc 0 in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
hence (Computation s,((LifeSpan (s +* I)) + 1)) . (intloc 0 ) = (DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))) . (intloc 0 ) by A23, FUNCT_1:72, SCMFSA_2:127
.= ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) . (intloc 0 ) by A28, FUNCT_1:72, SCMFSA_2:127
.= (Initialized J) . (intloc 0 ) by A27, FUNCT_4:14
.= 1 by SCMFSA6A:46 ;
:: thesis: ( s is halting & LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) & ( J is keeping_0 implies (Result s) . (intloc 0 ) = 1 ) )

A29: now

let k be Element of NAT ; :: thesis: ( ((LifeSpan (s +* I)) + 1) + k < m implies not CurInstr (Computation s,(((LifeSpan (s +* I)) + 1) + k)) = halt SCM+FSA )
assume ((LifeSpan (s +* I)) + 1) + k < m ; :: thesis: not CurInstr (Computation s,(((LifeSpan (s +* I)) + 1) + k)) = halt SCM+FSA
then A30: k < LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by XREAL_1:8;
assume A31: CurInstr (Computation s,(((LifeSpan (s +* I)) + 1) + k)) = halt SCM+FSA ; :: thesis: contradiction
IncAddr (CurInstr (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),k)),(card I) = CurInstr (Computation (Computation s,((LifeSpan (s +* I)) + 1)),k) by A22, A23, A24, A26, Th12
.= halt SCM+FSA by A31, AMI_1:51 ;
then InsCode (CurInstr (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),k)) = 0 by SCMFSA_2:124, SCMFSA_4:22;
then CurInstr (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),k) = halt SCM+FSA by SCMFSA_2:122;
hence contradiction by A16, A30, AMI_1:def 46; :: thesis: verum

end;

IncAddr (CurInstr (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))))),(card I) = CurInstr (Computation (Computation s,((LifeSpan (s +* I)) + 1)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)))) by A22, A23, A24, A26, Th12;
then IncAddr (CurInstr (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))))),(card I) = CurInstr (Computation s,(((LifeSpan (s +* I)) + 1) + (LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))))) by AMI_1:51;
then A32: CurInstr (Computation s,m) = IncAddr (halt SCM+FSA ),(card I) by A16, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;

now

let k be Element of NAT ; :: thesis: ( k < m implies CurInstr (Computation s,b₁) <> halt SCM+FSA )
assume A33: k < m ; :: thesis: CurInstr (Computation s,b₁) <> halt SCM+FSA

per cases ( k <= LifeSpan (s +* I) or LifeSpan (s +* I) < k ) ;

suppose k <= LifeSpan (s +* I) ; :: thesis: CurInstr (Computation s,b₁) <> halt SCM+FSA

hence CurInstr (Computation s,k) <> halt SCM+FSA by A2, A20, Th23; :: thesis: verum

end;

suppose LifeSpan (s +* I) < k ; :: thesis: CurInstr (Computation s,b₁) <> halt SCM+FSA

then (LifeSpan (s +* I)) + 1 <= k by NAT_1:13;
then consider kk being Nat such that
A34: ((LifeSpan (s +* I)) + 1) + kk = k by NAT_1:10;
reconsider kk = kk as Element of NAT by ORDINAL1:def 13;
((LifeSpan (s +* I)) + 1) + kk = k by A34;
hence CurInstr (Computation s,k) <> halt SCM+FSA by A29, A33; :: thesis: verum

end;

end;

end;

then A35: for k being Element of NAT st CurInstr (Computation s,k) = halt SCM+FSA holds
m <= k ;
thus A36: s is halting by A32, AMI_1:def 20; :: thesis: ( LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) & ( J is keeping_0 implies (Result s) . (intloc 0 ) = 1 ) )
then A37: LifeSpan s = m by A32, A35, AMI_1:def 46;
s +* I = s +* (Initialized I) by A1, SCMFSA6A:51;
then Initialized I c= s +* I by FUNCT_4:26;
hence LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) by A37, Th5, AMI_1:122; :: thesis: ( J is keeping_0 implies (Result s) . (intloc 0 ) = 1 )
A38: Initialized J c= (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) by FUNCT_4:26;
A39: J +* (Start-At (insloc 0 )) c= (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) by FUNCT_4:26, SCMFSA6B:8;

hereby :: thesis: verum

assume A40: J is keeping_0 ; :: thesis: (Result s) . (intloc 0 ) = 1
A41: DataPart (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)))) = DataPart (Computation (Computation s,((LifeSpan (s +* I)) + 1)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)))) by A22, A23, A24, A26, Th12;
thus (Result s) . (intloc 0 ) = (Computation s,m) . (intloc 0 ) by A36, A37, AMI_1:122
.= (Computation (Computation s,((LifeSpan (s +* I)) + 1)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)))) . (intloc 0 ) by AMI_1:51
.= (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)))) . (intloc 0 ) by A41, SCMFSA6A:38
.= ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) . (intloc 0 ) by A39, A40, SCMFSA6B:def 4
.= (Initialized J) . (intloc 0 ) by A27, A38, GRFUNC_1:8
.= 1 by SCMFSA6A:46 ; :: thesis: verum

end;