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