let ss be State of ; :: thesis: for I, J being Program of
for a being read-write Int-Location st ss . (intloc 0 ) = 1 & ss . a > 0 & Directed I is_pseudo-closed_on ss holds
DataPart (IExec (if>0 a,I,J),ss) = DataPart (IExec (I ';' (Stop SCM+FSA )),ss)
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
let I, J be Program of ; :: thesis: for a being read-write Int-Location st ss . (intloc 0 ) = 1 & ss . a > 0 & Directed I is_pseudo-closed_on ss holds
DataPart (IExec (if>0 a,I,J),ss) = DataPart (IExec (I ';' (Stop SCM+FSA )),ss)
let a be read-write Int-Location ; :: thesis: ( ss . (intloc 0 ) = 1 & ss . a > 0 & Directed I is_pseudo-closed_on ss implies DataPart (IExec (if>0 a,I,J),ss) = DataPart (IExec (I ';' (Stop SCM+FSA )),ss) )
set I0 = Directed I;
set s = Initialize ss;
set I1 = I ';' (Stop SCM+FSA );
set s00 = (Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )));
set s3 = (Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )));
set s4 = Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1;
set i = a >0_goto (insloc ((card J) + 3));
assume A1: ss . (intloc 0 ) = 1 ; :: thesis: ( not ss . a > 0 or not Directed I is_pseudo-closed_on ss or DataPart (IExec (if>0 a,I,J),ss) = DataPart (IExec (I ';' (Stop SCM+FSA )),ss) )
set s1 = (Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )));
assume ss . a > 0 ; :: thesis: ( not Directed I is_pseudo-closed_on ss or DataPart (IExec (if>0 a,I,J),ss) = DataPart (IExec (I ';' (Stop SCM+FSA )),ss) )
then A2: (Initialize ss) . a > 0 by SCMFSA6C:3;
IC SCM+FSA in dom ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
then A3: IC ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) = ((if>0 a,I,J) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by FUNCT_4:14
.= insloc 0 by SF_MASTR:66 ;
A4: insloc 0 in dom (if>0 a,I,J) by Th54;
if>0 a,I,J c= (if>0 a,I,J) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then dom (if>0 a,I,J) c= dom ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
then A5: ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 0 ) = ((if>0 a,I,J) +* (Start-At (insloc 0 ))) . (insloc 0 ) by A4, FUNCT_4:14
.= (if>0 a,I,J) . (insloc 0 ) by A4, SCMFSA6B:7
.= a >0_goto (insloc ((card J) + 3)) by Th55 ;
A6: Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),(0 + 1) = Following (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),0 ) by AMI_1:14
.= Following ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) by AMI_1:13
.= Exec (a >0_goto (insloc ((card J) + 3))),((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) by A3, A5 ;
not a in dom ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by SCMFSA6B:12;
then ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) . a = (Initialize ss) . a by FUNCT_4:12;
then A7: IC (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) = insloc ((card J) + 3) by A2, A6, SCMFSA_2:97;
assume Directed I is_pseudo-closed_on ss ; :: thesis: DataPart (IExec (if>0 a,I,J),ss) = DataPart (IExec (I ';' (Stop SCM+FSA )),ss)
then A8: Directed I is_pseudo-closed_on Initialize ss by A1, Th53;
then A9: LifeSpan ((Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = pseudo-LifeSpan (Initialize ss),(Directed I) by Th58;
DataPart (Initialize ss) = DataPart ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))) by SCMFSA8A:11;
then A10: Directed I is_pseudo-closed_on (Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 ))) by A8, Th52;
A11: DataPart ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))) = DataPart ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) by SCMFSA6A:39, SCMFSA8A:14;

A12: now

let f be FinSeq-Location ; :: thesis: ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))) . f = (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) . f
thus ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))) . f = ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) . f by A11, SCMFSA6A:38
.= (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) . f by A6, SCMFSA_2:97 ; :: thesis: verum

end;

now

let a be Int-Location ; :: thesis: ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))) . a = (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) . a
thus ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))) . a = ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) . a by A11, SCMFSA6A:38
.= (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) . a by A6, SCMFSA_2:97 ; :: thesis: verum

end;

then A13: DataPart ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))) = DataPart (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) by A12, SCMFSA6A:38;
card (if>0 a,I,J) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:15
.= (((card I) + (card J)) + 3) + 1 ;
then ((card I) + (card J)) + 3 < card (if>0 a,I,J) by NAT_1:13;
then A14: insloc (((card I) + (card J)) + 3) in dom (if>0 a,I,J) by SCMFSA6A:15;
A15: card (((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) = (card ((Macro (a >0_goto (insloc ((card J) + 3)))) ';' J)) + (card (Goto (insloc ((card I) + 1)))) by SCMFSA6A:61
.= (card ((Macro (a >0_goto (insloc ((card J) + 3)))) ';' J)) + 1 by SCMFSA8A:29
.= ((card (Macro (a >0_goto (insloc ((card J) + 3))))) + (card J)) + 1 by SCMFSA6A:61
.= ((card J) + 2) + 1 by SCMFSA7B:6
.= (card J) + (2 + 1) ;
(Initialize ss) +* (Initialized (if>0 a,I,J)) = (Initialize (Initialize ss)) +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
then A16: (Initialize ss) +* (Initialized (if>0 a,I,J)) = (Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by Th15;
A17: if>0 a,I,J c= (Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by FUNCT_4:26, SCMFSA6B:5;
A18: if>0 a,I,J c= (if>0 a,I,J) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
(if>0 a,I,J) +* (Start-At (insloc 0 )) c= (Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then A19: if>0 a,I,J c= (Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by A18, XBOOLE_1:1;
A20: (Directed I) +* (Start-At (insloc 0 )) c= (Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
A21: if>0 a,I,J = ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) by SCMFSA8B:def 2;
then if>0 a,I,J = (((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' (I ';' (Stop SCM+FSA )) by SCMFSA6A:67;
then ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= if>0 a,I,J by A15, FUNCT_4:26;
then ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= (Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by A19, XBOOLE_1:1;
then ProgramPart [(ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)))] c= Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1 by AMI_1:99;
then A22: ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1 by AMI_1:105;
ProgramPart (Relocated (Directed I),((card J) + 3)) c= ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) by Th12, SCMFSA6A:55;
then A23: ProgramPart (Relocated (Directed I),((card J) + 3)) c= Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1 by A22, XBOOLE_1:1;
IC (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),((pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1)) = IC (Computation (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1),(pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I))) by AMI_1:51
.= (IC (Computation ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)))) + ((card J) + 3) by A20, A10, A23, A7, A13, Th51
.= (IC (Computation ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (Initialize ss),(Directed I)))) + ((card J) + 3) by A8, Th50
.= (insloc (card (ProgramPart (Directed I)))) + ((card J) + 3) by A8, SCMFSA8A:def 5
.= (insloc (card (Directed I))) + ((card J) + 3) by AMI_1:105
.= insloc ((card I) + ((card J) + 3)) by SCMFSA8A:34
.= insloc (((card I) + (card J)) + 3) ;
then A24: CurInstr (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),((pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1)) = ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc (((card I) + (card J)) + 3)) by AMI_1:54
.= (if>0 a,I,J) . (insloc (((card I) + (card J)) + 3)) by A17, A14, GRFUNC_1:8
.= halt SCM+FSA by Th62 ;
then A25: ProgramPart ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) halts_on (Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by AMI_1:146;

now

set J1 = (((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I;
let k be Element of NAT ; :: thesis: ( CurInstr (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA implies (pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 <= k )
assume A26: CurInstr (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA ; :: thesis: (pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 <= k
assume not (pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 <= k ; :: thesis: contradiction
then A27: k <= pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I) by NAT_1:13;
A28: insloc 0 in dom (if>0 a,I,J) by Th54;
A29: InsCode (a >0_goto (insloc ((card J) + 3))) = 8 by SCMFSA_2:49;
CurInstr (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),0 ) = CurInstr ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) by AMI_1:13
.= ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 0 ) by Th31
.= (if>0 a,I,J) . (insloc 0 ) by A28, Th26
.= a >0_goto (insloc ((card J) + 3)) by Th55 ;
then consider k1 being Nat such that
A30: k1 + 1 = k by A26, A29, NAT_1:6, SCMFSA_2:124;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
reconsider n = IC (Computation ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),k1) as Element of NAT by ORDINAL1:def 13;
k1 < k by A30, XREAL_1:31;
then A31: k1 < pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I) by A27, XXREAL_0:2;
then k1 < pseudo-LifeSpan (Initialize ss),(Directed I) by A8, Th50;
then insloc n in dom (Directed I) by A8, SCMFSA8A:31;
then n < card (Directed I) by SCMFSA6A:15;
then n + ((card J) + 3) < (card (Directed I)) + ((card J) + 3) by XREAL_1:8;
then A32: n + ((card J) + 3) < (card I) + ((card J) + 3) by SCMFSA8A:34;
A33: IC (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k) = IC (Computation (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1),k1) by A30, AMI_1:51
.= (IC (Computation ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),k1)) + ((card J) + 3) by A20, A10, A23, A7, A13, A31, Th51 ;
card ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) = (card (((Macro (a >0_goto (insloc ((card J) + 3)))) ';' J) ';' (Goto (insloc ((card I) + 1))))) + (card I) by SCMFSA6A:61
.= ((card ((Macro (a >0_goto (insloc ((card J) + 3)))) ';' J)) + (card (Goto (insloc ((card I) + 1))))) + (card I) by SCMFSA6A:61
.= ((card ((Macro (a >0_goto (insloc ((card J) + 3)))) ';' J)) + 1) + (card I) by SCMFSA8A:29
.= (((card (Macro (a >0_goto (insloc ((card J) + 3))))) + (card J)) + 1) + (card I) by SCMFSA6A:61
.= ((2 + (card J)) + 1) + (card I) by SCMFSA7B:6
.= ((card I) + (card J)) + 3 ;
then IC (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) by A33, A32, SCMFSA6A:15;
then A34: IC (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (Directed ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) by FUNCT_4:105;
then A35: (Directed ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) . (IC (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k)) in rng (Directed ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) by FUNCT_1:def 5;
card (if>0 a,I,J) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:15
.= (((card I) + (card J)) + 3) + 1 ;
then ((card I) + (card J)) + 3 < card (if>0 a,I,J) by XREAL_1:31;
then n + ((card J) + 3) < card (if>0 a,I,J) by A32, XXREAL_0:2;
then A36: IC (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if>0 a,I,J) by A33, SCMFSA6A:15;
A37: CurInstr (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k) = ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) . (IC (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k)) by AMI_1:54
.= (if>0 a,I,J) . (IC (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k)) by A36, Th26 ;
Directed ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) c= if>0 a,I,J by A21, SCMFSA6A:55;
then (if>0 a,I,J) . (IC (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k)) = (Directed ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) . (IC (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k)) by A34, GRFUNC_1:8;
hence contradiction by A26, A35, A37, AMI_1:def 53; :: thesis: verum

end;

then A38: LifeSpan ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) = (pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 by A24, A25, AMI_1:def 46;
(Initialize ss) +* (Initialized (I ';' (Stop SCM+FSA ))) = (Initialize (Initialize ss)) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
then A39: (Initialize ss) +* (Initialized (I ';' (Stop SCM+FSA ))) = (Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) by Th15;
A40: (Directed I) ';' (Stop SCM+FSA ) = I ';' (Stop SCM+FSA ) by SCMFSA8A:41;
Directed (Directed I) = Directed I by SCMFSA6A:63;
then A41: DataPart (Computation ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (Initialize ss),(Directed I))) = DataPart (Computation ((Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (Initialize ss),(Directed I))) by A8, A40, Th58;
I ';' (Stop SCM+FSA ) is_halting_on Initialize ss by A8, Th58;
then A42: ProgramPart ((Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on (Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) by SCMFSA7B:def 8;
thus DataPart (IExec (if>0 a,I,J),ss) = DataPart (IExec (if>0 a,I,J),(Initialize ss)) by Th17
.= DataPart ((Result ((Initialize ss) +* (Initialized (if>0 a,I,J)))) +* ((Initialize ss) | NAT )) by SCMFSA6B:def 1
.= DataPart (Result ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))))) by A16, Th35
.= DataPart (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))))) by A25, AMI_1:122
.= DataPart (Computation (Computation ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1),(pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I))) by A38, AMI_1:51
.= DataPart (Computation ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan ((Initialize ss) +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I))) by A20, A10, A23, A7, A13, Th51
.= DataPart (Computation ((Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))))) by A8, A9, A41, Th50
.= DataPart (Result ((Initialize ss) +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) by A42, AMI_1:122
.= DataPart ((Result ((Initialize ss) +* (Initialized (I ';' (Stop SCM+FSA ))))) +* ((Initialize ss) | NAT )) by A39, Th35
.= DataPart (IExec (I ';' (Stop SCM+FSA )),(Initialize ss)) by SCMFSA6B:def 1
.= DataPart (IExec (I ';' (Stop SCM+FSA )),ss) by Th17 ; :: thesis: verum