let P be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for I being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st I is_halting_on s,P & s . a > 0 holds
( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) ) )
set D = Int-Locations \/ FinSeq-Locations;
let s be State of SCM+FSA; for I being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st I is_halting_on s,P & s . a > 0 holds
( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) ) )
let I be really-closed MacroInstruction of SCM+FSA ; for a being read-write Int-Location st I is_halting_on s,P & s . a > 0 holds
( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) ) )
let a be read-write Int-Location; ( I is_halting_on s,P & s . a > 0 implies ( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) ) ) )
set sI = Initialize s;
set PI = P +* I;
set s1 = Initialize s;
set P1 = P +* (while>0 (a,I));
defpred S1[ Nat] means ( $1 <= LifeSpan ((P +* I),(Initialize s)) implies ( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + $1))) = (IC (Comput ((P +* I),(Initialize s),$1))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + $1))) = DataPart (Comput ((P +* I),(Initialize s),$1)) ) );
assume A1:
I is_halting_on s,P
; ( not s . a > 0 or ( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) ) ) )
A2:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A3:
S1[
k]
;
S1[k + 1]now ( k + 1 <= LifeSpan ((P +* I),(Initialize s)) implies ( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) ) )A4:
k + 0 < k + 1
by XREAL_1:6;
assume
k + 1
<= LifeSpan (
(P +* I),
(Initialize s))
;
( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) )then
k < LifeSpan (
(P +* I),
(Initialize s))
by A4, XXREAL_0:2;
hence
(
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 3 &
DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) )
by A1, A3, Th13;
verum end; hence
S1[
k + 1]
;
verum end;
reconsider l = LifeSpan ((P +* I),(Initialize s)) as Element of NAT by ORDINAL1:def 12;
set loc4 = (card I) + 3;
set i = a >0_goto 3;
set s2 = Comput ((P +* (while>0 (a,I))),(Initialize s),1);
IC in dom (Start-At (0,SCM+FSA))
by MEMSTR_0:15;
then A5: IC (Initialize s) =
IC (Start-At (0,SCM+FSA))
by FUNCT_4:13
.=
0
by FUNCOP_1:72
;
not a in dom (Start-At (0,SCM+FSA))
by SCMFSA_2:102;
then A6:
(Initialize s) . a = s . a
by FUNCT_4:11;
assume A7:
s . a > 0
; ( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) ) )
A8:
0 in dom (while>0 (a,I))
by AFINSQ_1:65;
A9:
(P +* (while>0 (a,I))) /. (IC (Initialize s)) = (P +* (while>0 (a,I))) . (IC (Initialize s))
by PBOOLE:143;
(P +* (while>0 (a,I))) . 0 =
(while>0 (a,I)) . 0
by A8, FUNCT_4:13
.=
a >0_goto 3
by SCMFSA_X:10
;
then A10:
CurInstr ((P +* (while>0 (a,I))),(Initialize s)) = a >0_goto 3
by A5, A9;
A11: Comput ((P +* (while>0 (a,I))),(Initialize s),(0 + 1)) =
Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),0)))
by EXTPRO_1:3
.=
Exec ((a >0_goto 3),(Initialize s))
by A10
;
then
( ( for c being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialize s),1)) . c = (Initialize s) . c ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialize s),1)) . f = (Initialize s) . f ) )
by SCMFSA_2:71;
then A12:
DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),1)) = DataPart (Initialize s)
by SCMFSA_M:2;
A13:
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),1)) = 3
by A7, A11, A6, SCMFSA_2:71;
A14:
S1[ 0 ]
proof
assume
0 <= LifeSpan (
(P +* I),
(Initialize s))
;
( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + 0))) = (IC (Comput ((P +* I),(Initialize s),0))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + 0))) = DataPart (Comput ((P +* I),(Initialize s),0)) )
A15:
IC in dom (Start-At (0,SCM+FSA))
by MEMSTR_0:15;
IC (Comput ((P +* I),(Initialize s),0)) =
IC (Start-At (0,SCM+FSA))
by A15, FUNCT_4:13
.=
0
by FUNCOP_1:72
;
hence
(
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + 0))) = (IC (Comput ((P +* I),(Initialize s),0))) + 3 &
DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + 0))) = DataPart (Comput ((P +* I),(Initialize s),0)) )
by A13, A12;
verum
end;
A16:
for k being Nat holds S1[k]
from NAT_1:sch 2(A14, A2);
set s4 = Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1));
set s3 = Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))));
set s2 = Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))));
S1[l]
by A16;
then A17:
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0
by A1, Th14;
A18:
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0
by A17;
A19: Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1)) =
Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))))
by EXTPRO_1:3
.=
Exec ((goto 0),(Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))))
by A18
;
A20:
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + (LifeSpan ((P +* I),(Initialize s)))) + 1))) = 0
by A19, SCMFSA_2:69;
hence
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0
; for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I))
A21:
now for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 & k <> 0 holds
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I))let k be
Nat;
( k <= (LifeSpan ((P +* I),(Initialize s))) + 2 & k <> 0 implies IC (Comput ((P +* (while>0 (a,I))),(Initialize s),b1)) in dom (while>0 (a,I)) )assume A22:
k <= (LifeSpan ((P +* I),(Initialize s))) + 2
;
( k <> 0 implies IC (Comput ((P +* (while>0 (a,I))),(Initialize s),b1)) in dom (while>0 (a,I)) )assume
k <> 0
;
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),b1)) in dom (while>0 (a,I))then consider n being
Nat such that A23:
k = n + 1
by NAT_1:6;
(
k <= (LifeSpan ((P +* I),(Initialize s))) + 1 or
k >= ((LifeSpan ((P +* I),(Initialize s))) + 1) + 1 )
by NAT_1:13;
then A24:
(
k <= (LifeSpan ((P +* I),(Initialize s))) + 1 or
k = (LifeSpan ((P +* I),(Initialize s))) + 2 )
by A22, XXREAL_0:1;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
per cases
( k <= (LifeSpan ((P +* I),(Initialize s))) + 1 or k >= (LifeSpan ((P +* I),(Initialize s))) + 2 )
by A24;
suppose
k <= (LifeSpan ((P +* I),(Initialize s))) + 1
;
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),b1)) in dom (while>0 (a,I))then
n <= LifeSpan (
(P +* I),
(Initialize s))
by A23, XREAL_1:6;
then A25:
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + n))) = (IC (Comput ((P +* I),(Initialize s),n))) + 3
by A16;
reconsider m =
IC (Comput ((P +* I),(Initialize s),n)) as
Element of
NAT ;
A26:
I c= P +* I
by FUNCT_4:25;
IC (Initialize s) = 0
by MEMSTR_0:def 11;
then
IC (Initialize s) in dom I
by AFINSQ_1:65;
then
m in dom I
by AMISTD_1:21, A26;
then
m < card I
by AFINSQ_1:66;
then A27:
m + 3
< (card I) + 5
by XREAL_1:8;
card (while>0 (a,I)) = (card I) + 5
by SCMFSA_X:4;
hence
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I))
by A23, A25, A27, AFINSQ_1:66;
verum end; end; end;
now for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I))let k be
Nat;
( k <= (LifeSpan ((P +* I),(Initialize s))) + 2 implies IC (Comput ((P +* (while>0 (a,I))),(Initialize s),b1)) in dom (while>0 (a,I)) )assume A28:
k <= (LifeSpan ((P +* I),(Initialize s))) + 2
;
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),b1)) in dom (while>0 (a,I)) end;
hence
for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I))
; verum