set D = Int-Locations \/ FinSeq-Locations ;
let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA
for a being read-write Int-Location st I is_closed_on s & I is_halting_on s & s . a = 0 holds
( IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) = 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 holds
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) ) )
let I be Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st I is_closed_on s & I is_halting_on s & s . a = 0 holds
( IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) = 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 holds
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) ) )
let a be read-write Int-Location ; :: thesis: ( I is_closed_on s & I is_halting_on s & s . a = 0 implies ( IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) = 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 holds
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) ) ) )
assume A1: I is_closed_on s ; :: thesis: ( not I is_halting_on s or not s . a = 0 or ( IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) = 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 holds
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) ) ) )
set sI = s +* (I +* (Start-At 0 ,SCM+FSA ));
set s1 = s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ));
defpred S1[ Nat] means ( $1 <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) implies ( IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + $1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),$1)) + 4 & DataPart (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + $1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),$1) ) );
assume A2: I is_halting_on s ; :: thesis: ( not s . a = 0 or ( IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) = 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 holds
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) ) ) )
A3: now
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
now
A5: k + 0 < k + 1 by XREAL_1:8;
assume k + 1 <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) ; :: thesis: ( IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) )
then k < LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) by A5, XXREAL_0:2;
hence ( IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) ) by A1, A2, A4, Th19; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
reconsider l = LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) as Element of NAT ;
set loc4 = (card I) + 4;
set i = a =0_goto 4;
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;
A6: IC SCM+FSA in dom ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )) by SF_MASTR:65;
A7: IC (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))) = (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))) . (IC SCM+FSA ) by AMI_1:def 15
.= ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )) . (IC SCM+FSA ) by A6, FUNCT_4:14
.= 0 by SF_MASTR:66 ;
not a in dom ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )) by SCMFSA6B:12;
then A8: (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))) . a = s . a by FUNCT_4:12;
assume A9: s . a = 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 ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) = 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 holds
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) ) )
A10: 0 in dom (while=0 a,I) by Th10;
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 AMI_1:150;
while=0 a,I c= (while=0 a,I) +* (Start-At 0 ,SCM+FSA ) by SCMFSA8A:9;
then A11: dom (while=0 a,I) c= dom ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )) by GRFUNC_1:8;
then (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))) . 0 = ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )) . 0 by A10, FUNCT_4:14
.= (while=0 a,I) . 0 by A10, SCMFSA6B:7
.= a =0_goto 4 by Th11 ;
then A12: 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 A7, Y, AMI_1:def 16;
A13: 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 A12, AMI_1:def 18 ;
then ( ( for c being Int-Location holds (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),1) . c = (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))) . c ) & ( for f being FinSeq-Location holds (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),1) . f = (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))) . f ) ) by SCMFSA_2:96;
then A14: DataPart (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),1) = DataPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))) by SCMFSA6A:38
.= DataPart s by SCMFSA8A:11
.= DataPart (s +* (I +* (Start-At 0 ,SCM+FSA ))) by SCMFSA8A:11 ;
A15: 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 ) by AMI_1:def 15
.= 4 by A9, A13, A8, SCMFSA_2:96 ;
A16: S1[ 0 ]
proof
assume 0 <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) ; :: thesis: ( IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + 0 )) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),0 )) + 4 & DataPart (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + 0 )) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),0 ) )
A17: IC SCM+FSA in dom (I +* (Start-At 0 ,SCM+FSA )) by SF_MASTR:65;
IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),0 ) = IC (s +* (I +* (Start-At 0 ,SCM+FSA ))) by AMI_1:13
.= (s +* (I +* (Start-At 0 ,SCM+FSA ))) . (IC SCM+FSA ) by AMI_1:def 15
.= (I +* (Start-At 0 ,SCM+FSA )) . (IC SCM+FSA ) by A17, FUNCT_4:14
.= 0 by SF_MASTR:66 ;
hence ( IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + 0 )) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),0 )) + 4 & DataPart (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + 0 )) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),0 ) ) by A15, A14, AMI_1:13; :: thesis: verum
end;
A18: for k being Element of NAT holds S1[k] from NAT_1:sch 1(A16, A3);
 set s4 = Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(((1 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) + 1) + 1);
set s3 = Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) + 1);
A19: (card I) + 4 in dom (while=0 a,I) by Th13;
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 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))));
S1[l] by A18;
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 ))),(1 + (LifeSpan (s +* (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 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))))) = goto ((card I) + 4) by A1, A2, Th20;
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 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))))) by AMI_1:144;
A21: Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) + 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 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))))) by AMI_1:14
.= Exec (goto ((card I) + 4)),(Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))))) by A20, T, AMI_1:def 18 ;
A22: IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + (LifeSpan (s +* (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 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) + 1)) . (IC SCM+FSA ) by AMI_1:def 15
.= (card I) + 4 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 ))),((1 + (LifeSpan (s +* (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 + (LifeSpan (s +* (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 + (LifeSpan (s +* (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 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) + 1))) by AMI_1:150;
(Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) + 1)) . ((card I) + 4) = (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))) . ((card I) + 4) by AMI_1:54
.= ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )) . ((card I) + 4) by A11, A19, FUNCT_4:14
.= (while=0 a,I) . ((card I) + 4) by A19, SCMFSA6B:7
.= goto 0 by Th21 ;
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 ))),((1 + (LifeSpan (s +* (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 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) + 1)) = goto 0 by A22, Y, AMI_1:def 16;
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 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) + 1)) by AMI_1:144;
A24: Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(((1 + (LifeSpan (s +* (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 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) + 1)) by AMI_1:14
.= Exec (goto 0 ),(Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) + 1)) by A23, T, AMI_1:def 18 ;
A25: IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(((1 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) + 1) + 1)) = (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(((1 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) + 1) + 1)) . (IC SCM+FSA ) by AMI_1:def 15
.= 0 by A24, SCMFSA_2:95 ;
hence IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) = 0 ; :: thesis: for k being Element of NAT st k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 holds
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)
A26: (((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + 1) + 1 = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + (2 + 1) ;
A27: now
let k be Element of NAT ; :: thesis: ( k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 & k <> 0 implies 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) )
assume A28: k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 ; :: thesis: ( k <> 0 implies 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) )
assume 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)
then consider n being Nat such that
A29: k = n + 1 by NAT_1:6;
( k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 or k >= ((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + 1 ) by NAT_1:13;
then A30: ( k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 or k = ((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + 1 or k > ((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + 1 ) by XXREAL_0:1;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
per cases ( k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 or k = ((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + 1 or k >= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 ) by A26, A30, NAT_1:13;
suppose k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 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)
then n <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) by A29, XREAL_1:8;
then A31: IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + n)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n)) + 4 by A18;
reconsider m = IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) as Element of NAT ;
m in dom I by A1, SCMFSA7B:def 7;
then m < card I by SCMFSA6A:15;
then A32: m + 4 < (card I) + 6 by XREAL_1:10;
card (while=0 a,I) = (card I) + 6 by Th4;
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 A29, A31, A32, SCMFSA6A:15; :: thesis: verum
end;
suppose k = ((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + 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 A22, Th13; :: thesis: verum
end;
suppose k >= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 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)
then k = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 by A28, XXREAL_0:1;
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 A25, Th10; :: thesis: verum
end;
end;
end;
now
let k be Element of NAT ; :: thesis: ( k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 implies 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) )
assume A33: k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 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)
per cases ( k = 0 or k <> 0 ) ;
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 A10, A7, AMI_1:13; :: thesis: verum
end;
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 A27, A33; :: thesis: verum
end;
end;
end;
hence for k being Element of NAT st k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 holds
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) ; :: thesis: verum