let p be Instruction-Sequence of SCM+FSA; for a being read-write Int-Location
for I being Program of SCM+FSA
for s being 0 -started State of SCM+FSA st while=0 (a,I) c= p & s . a <> 0 holds
( LifeSpan (p,s) = 4 & ( for k being Element of NAT holds DataPart (Comput (p,s,k)) = DataPart s ) )
let a be read-write Int-Location ; for I being Program of SCM+FSA
for s being 0 -started State of SCM+FSA st while=0 (a,I) c= p & s . a <> 0 holds
( LifeSpan (p,s) = 4 & ( for k being Element of NAT holds DataPart (Comput (p,s,k)) = DataPart s ) )
let I be Program of SCM+FSA; for s being 0 -started State of SCM+FSA st while=0 (a,I) c= p & s . a <> 0 holds
( LifeSpan (p,s) = 4 & ( for k being Element of NAT holds DataPart (Comput (p,s,k)) = DataPart s ) )
let s be 0 -started State of SCM+FSA; ( while=0 (a,I) c= p & s . a <> 0 implies ( LifeSpan (p,s) = 4 & ( for k being Element of NAT holds DataPart (Comput (p,s,k)) = DataPart s ) ) )
A1:
Start-At (0,SCM+FSA) c= s
by MEMSTR_0:29;
assume that
A2:
while=0 (a,I) c= p
and
A3:
s . a <> 0
; ( LifeSpan (p,s) = 4 & ( for k being Element of NAT holds DataPart (Comput (p,s,k)) = DataPart s ) )
A4:
p +* (while=0 (a,I)) = p
by A2, FUNCT_4:98;
set i = a =0_goto 4;
set s1 = Initialize s;
set p1 = p +* (while=0 (a,I));
A5:
while=0 (a,I) c= p +* (while=0 (a,I))
by FUNCT_4:25;
B6:
IC in dom (Start-At (0,SCM+FSA))
by MEMSTR_0:15;
not a in dom (Start-At (0,SCM+FSA))
by SCMFSA_2:102;
then A7:
(Initialize s) . a = s . a
by FUNCT_4:11;
A8:
1 in dom (while=0 (a,I))
by SCMFSA_9:10;
A9: (p +* (while=0 (a,I))) . 1 =
(while=0 (a,I)) . 1
by A8, FUNCT_4:13
.=
goto 2
by SCMFSA_9:11
;
A10: IC (Initialize s) =
IC (Start-At (0,SCM+FSA))
by B6, FUNCT_4:13
.=
0
by FUNCOP_1:72
;
A11:
(p +* (while=0 (a,I))) /. (IC (Initialize s)) = (p +* (while=0 (a,I))) . (IC (Initialize s))
by PBOOLE:143;
0 in dom (while=0 (a,I))
by SCMFSA_9:10;
then (p +* (while=0 (a,I))) . 0 =
(while=0 (a,I)) . 0
by FUNCT_4:13
.=
a =0_goto 4
by SCMFSA_9:11
;
then A12:
CurInstr ((p +* (while=0 (a,I))),(Initialize s)) = a =0_goto 4
by A10, A11;
A13: 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
.=
Following ((p +* (while=0 (a,I))),(Initialize s))
by EXTPRO_1:2
.=
Exec ((a =0_goto 4),(Initialize s))
by A12
;
set loc5 = (card I) + 5;
set s5 = Comput ((p +* (while=0 (a,I))),(Initialize s),4);
set p5 = p +* (while=0 (a,I));
set s4 = Comput ((p +* (while=0 (a,I))),(Initialize s),3);
set p4 = p +* (while=0 (a,I));
set s3 = Comput ((p +* (while=0 (a,I))),(Initialize s),2);
set p3 = p +* (while=0 (a,I));
set s2 = Comput ((p +* (while=0 (a,I))),(Initialize s),1);
A14:
2 in dom (while=0 (a,I))
by SCMFSA_9:12;
A15: (p +* (while=0 (a,I))) . 2 =
(while=0 (a,I)) . 2
by A14, FUNCT_4:13
.=
goto 3
by SCMFSA_9:16
;
A16:
3 in dom (while=0 (a,I))
by SCMFSA_9:12;
A17: (p +* (while=0 (a,I))) . 3 =
(while=0 (a,I)) . 3
by A16, FUNCT_4:13
.=
goto ((card I) + 5)
by SCMFSA_9:15
;
A18:
(card I) + 5 in dom (while=0 (a,I))
by SCMFSA_9:13;
A19: (p +* (while=0 (a,I))) . ((card I) + 5) =
(while=0 (a,I)) . ((card I) + 5)
by A18, A5, GRFUNC_1:2
.=
halt SCM+FSA
by SCMFSA_9:14
;
A20:
( ( for c being Int-Location holds (Exec ((goto ((card I) + 5)),(Comput ((p +* (while=0 (a,I))),(Initialize s),3)))) . c = (Comput ((p +* (while=0 (a,I))),(Initialize s),3)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto ((card I) + 5)),(Comput ((p +* (while=0 (a,I))),(Initialize s),3)))) . f = (Comput ((p +* (while=0 (a,I))),(Initialize s),3)) . f ) )
by SCMFSA_2:69;
A21:
( ( for c being Int-Location holds (Exec ((goto 2),(Comput ((p +* (while=0 (a,I))),(Initialize s),1)))) . c = (Comput ((p +* (while=0 (a,I))),(Initialize s),1)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto 2),(Comput ((p +* (while=0 (a,I))),(Initialize s),1)))) . f = (Comput ((p +* (while=0 (a,I))),(Initialize s),1)) . f ) )
by SCMFSA_2:69;
A22:
(p +* (while=0 (a,I))) /. (IC (Comput ((p +* (while=0 (a,I))),(Initialize s),1))) = (p +* (while=0 (a,I))) . (IC (Comput ((p +* (while=0 (a,I))),(Initialize s),1)))
by PBOOLE:143;
IC (Comput ((p +* (while=0 (a,I))),(Initialize s),1)) =
succ 0
by A3, A10, A13, A7, SCMFSA_2:70
.=
0 + 1
;
then A23:
CurInstr ((p +* (while=0 (a,I))),(Comput ((p +* (while=0 (a,I))),(Initialize s),1))) = goto 2
by A9, A22;
A24: Comput ((p +* (while=0 (a,I))),(Initialize s),(1 + 1)) =
Following ((p +* (while=0 (a,I))),(Comput ((p +* (while=0 (a,I))),(Initialize s),1)))
by EXTPRO_1:3
.=
Exec ((goto 2),(Comput ((p +* (while=0 (a,I))),(Initialize s),1)))
by A23
;
A25:
(p +* (while=0 (a,I))) /. (IC (Comput ((p +* (while=0 (a,I))),(Initialize s),2))) = (p +* (while=0 (a,I))) . (IC (Comput ((p +* (while=0 (a,I))),(Initialize s),2)))
by PBOOLE:143;
IC (Comput ((p +* (while=0 (a,I))),(Initialize s),2)) = 2
by A24, SCMFSA_2:69;
then A26:
CurInstr ((p +* (while=0 (a,I))),(Comput ((p +* (while=0 (a,I))),(Initialize s),2))) = goto 3
by A15, A25;
A27: Comput ((p +* (while=0 (a,I))),(Initialize s),(2 + 1)) =
Following ((p +* (while=0 (a,I))),(Comput ((p +* (while=0 (a,I))),(Initialize s),2)))
by EXTPRO_1:3
.=
Exec ((goto 3),(Comput ((p +* (while=0 (a,I))),(Initialize s),2)))
by A26
;
A28:
(p +* (while=0 (a,I))) /. (IC (Comput ((p +* (while=0 (a,I))),(Initialize s),3))) = (p +* (while=0 (a,I))) . (IC (Comput ((p +* (while=0 (a,I))),(Initialize s),3)))
by PBOOLE:143;
IC (Comput ((p +* (while=0 (a,I))),(Initialize s),3)) = 3
by A27, SCMFSA_2:69;
then A29:
CurInstr ((p +* (while=0 (a,I))),(Comput ((p +* (while=0 (a,I))),(Initialize s),3))) = goto ((card I) + 5)
by A17, A28;
A30: Comput ((p +* (while=0 (a,I))),(Initialize s),(3 + 1)) =
Following ((p +* (while=0 (a,I))),(Comput ((p +* (while=0 (a,I))),(Initialize s),3)))
by EXTPRO_1:3
.=
Exec ((goto ((card I) + 5)),(Comput ((p +* (while=0 (a,I))),(Initialize s),3)))
by A29
;
A31:
(p +* (while=0 (a,I))) /. (IC (Comput ((p +* (while=0 (a,I))),(Initialize s),4))) = (p +* (while=0 (a,I))) . (IC (Comput ((p +* (while=0 (a,I))),(Initialize s),4)))
by PBOOLE:143;
IC (Comput ((p +* (while=0 (a,I))),(Initialize s),4)) = (card I) + 5
by A30, SCMFSA_2:69;
then A32:
CurInstr ((p +* (while=0 (a,I))),(Comput ((p +* (while=0 (a,I))),(Initialize s),4))) = halt SCM+FSA
by A19, A31;
then A33:
p +* (while=0 (a,I)) halts_on Initialize s
by EXTPRO_1:29;
A34:
s = Initialize s
by A1, FUNCT_4:98;
hence A37:
LifeSpan (p,s) = 4
by A34, A32, A33, A4, EXTPRO_1:def 15; for k being Element of NAT holds DataPart (Comput (p,s,k)) = DataPart s
A38:
( ( for c being Int-Location holds (Exec ((a =0_goto 4),(Initialize s))) . c = (Initialize s) . c ) & ( for f being FinSeq-Location holds (Exec ((a =0_goto 4),(Initialize s))) . f = (Initialize s) . f ) )
by SCMFSA_2:70;
then A39:
DataPart (Comput (p,s,1)) = DataPart s
by A34, A13, A4, SCMFSA6A:7;
then A40:
DataPart (Comput (p,s,2)) = DataPart s
by A34, A24, A21, A4, SCMFSA6A:7;
A41:
( ( for c being Int-Location holds (Exec ((goto 3),(Comput ((p +* (while=0 (a,I))),(Initialize s),2)))) . c = (Comput ((p +* (while=0 (a,I))),(Initialize s),2)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto 3),(Comput ((p +* (while=0 (a,I))),(Initialize s),2)))) . f = (Comput ((p +* (while=0 (a,I))),(Initialize s),2)) . f ) )
by SCMFSA_2:69;
then
DataPart (Comput (p,s,3)) = DataPart s
by A34, A27, A40, A4, SCMFSA6A:7;
then A42:
DataPart (Comput (p,s,4)) = DataPart s
by A34, A30, A20, A4, SCMFSA6A:7;
let k be Element of NAT ; DataPart (Comput (p,s,k)) = DataPart s
( k <= 3 or 3 < k )
;
then A43:
( k = 0 or k = 1 or k = 2 or k = 3 or 3 + 1 <= k )
by NAT_1:13, NAT_1:27;
per cases
( k = 0 or k = 1 or k = 2 or k = 3 or 4 <= k )
by A43;
suppose
4
<= k
;
DataPart (Comput (p,s,k)) = DataPart sthen
CurInstr (
p,
(Comput (p,s,k)))
= halt SCM+FSA
by A34, A33, A37, A4, EXTPRO_1:36;
hence
DataPart (Comput (p,s,k)) = DataPart s
by A37, A42, EXTPRO_1:24;
verum end;