let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a = 0 & I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let s be State of SCM+FSA; for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a = 0 & I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let I, J be Program of SCM+FSA; for a being read-write Int-Location st s . a = 0 & I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let a be read-write Int-Location ; ( s . a = 0 & I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
set I1 = I ';' (Stop SCM+FSA);
set s1 = s +* (Initialize ((intloc 0) .--> 1));
set P1 = P +* (I ';' (Stop SCM+FSA));
A1:
I ';' (Stop SCM+FSA) c= P +* (I ';' (Stop SCM+FSA))
by FUNCT_4:26;
set s3 = s +* (Initialize ((intloc 0) .--> 1));
set P3 = P +* (if=0 (a,I,J));
set s4 = Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1);
set i = a =0_goto ((card J) + 3);
B2:
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1)
by FUNCT_4:26;
then A2:
Start-At (0,SCM+FSA) c= s +* (Initialize ((intloc 0) .--> 1))
by B2, XBOOLE_1:1;
A3:
if=0 (a,I,J) = (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA))
by SCMFSA6A:67;
A4:
0 in dom (if=0 (a,I,J))
by Lm2;
A5: (P +* (if=0 (a,I,J))) . 0 =
(if=0 (a,I,J)) . 0
by A4, FUNCT_4:14
.=
a =0_goto ((card J) + 3)
by Lm3
;
V:
Initialize ((intloc 0) .--> 1) c= Initialized (if=0 (a,I,J))
by FUNCT_4:26;
then
dom (Initialize ((intloc 0) .--> 1)) c= dom (Initialized (if=0 (a,I,J)))
by RELAT_1:25;
then C11:
not a in dom (Initialize ((intloc 0) .--> 1))
by SCMFSA6A:48;
X2:
IC in dom (Initialize ((intloc 0) .--> 1))
by COMPOS_1:225;
then A6: IC (s +* (Initialize ((intloc 0) .--> 1))) =
IC (Initialize ((intloc 0) .--> 1))
by FUNCT_4:14
.=
IC (Initialized (if=0 (a,I,J)))
by V, X2, GRFUNC_1:8
.=
0
by SCMFSA6A:46
;
A7: Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),(0 + 1)) =
Following ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),0)))
by EXTPRO_1:4
.=
Following ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))))
by EXTPRO_1:3
.=
Exec ((a =0_goto ((card J) + 3)),(s +* (Initialize ((intloc 0) .--> 1))))
by A6, A5, PBOOLE:158
;
A10:
if=0 (a,I,J) c= P +* (if=0 (a,I,J))
by FUNCT_4:26;
A12:
dom (ProgramPart s) = NAT
by COMPOS_1:34;
assume
s . a = 0
; ( not I is_closed_on Initialized s,P or not I is_halting_on Initialized s,P or IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
then
(s +* (Initialize ((intloc 0) .--> 1))) . a = 0
by C11, FUNCT_4:12;
then A13:
IC (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1)) = (card J) + 3
by A7, SCMFSA_2:96;
A15:
for f being FinSeq-Location holds (s +* (Initialize ((intloc 0) .--> 1))) . f = (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1)) . f
by A7, SCMFSA_2:96;
for a being Int-Location holds (s +* (Initialize ((intloc 0) .--> 1))) . a = (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1)) . a
by A7, SCMFSA_2:96;
then A16:
DataPart (s +* (Initialize ((intloc 0) .--> 1))) = DataPart (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1))
by A15, SCMFSA6A:38;
card (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) =
(card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + (card (Goto ((card I) + 1)))
by SCMFSA6A:61
.=
(card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + 1
by SCMFSA8A:29
.=
((card (Macro (a =0_goto ((card J) + 3)))) + (card J)) + 1
by SCMFSA6A:61
.=
((card J) + 2) + 1
by COMPOS_1:150
.=
(card J) + (2 + 1)
;
then A17:
Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= if=0 (a,I,J)
by A3, Lm1;
A19:
Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= P +* (if=0 (a,I,J))
by A17, A10, XBOOLE_1:1;
assume A20:
I is_closed_on Initialized s,P
; ( not I is_halting_on Initialized s,P or IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
assume A21:
I is_halting_on Initialized s,P
; IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
then A22:
P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1))
by A20, SCMFSA8A:55;
I ';' (Stop SCM+FSA) is_closed_on Initialized s,P
by A20, A21, SCMFSA8A:46;
then A23:
I ';' (Stop SCM+FSA) is_closed_on s +* (Initialize ((intloc 0) .--> 1)),P +* (I ';' (Stop SCM+FSA))
by Th9;
A24: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)))) =
CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1)),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))))))
by EXTPRO_1:5
.=
IncAddr ((CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))))))),((card J) + 3))
by A2, A23, A13, A16, Th11, A19, A1
.=
IncAddr ((halt SCM+FSA),((card J) + 3))
by A22, EXTPRO_1:def 14
.=
halt SCM+FSA
by COMPOS_1:93
;
then A25:
P +* (if=0 (a,I,J)) halts_on s +* (Initialize ((intloc 0) .--> 1))
by EXTPRO_1:30;
now let l be
Element of
NAT ;
( l < (LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 implies CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),b1))) <> halt SCM+FSA )assume A26:
l < (LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 1
;
CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),b1))) <> halt SCM+FSAA27:
Comput (
(P +* (if=0 (a,I,J))),
(s +* (Initialize ((intloc 0) .--> 1))),
0)
= s +* (Initialize ((intloc 0) .--> 1))
by EXTPRO_1:3;
per cases
( l = 0 or l <> 0 )
;
suppose
l = 0
;
CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),b1))) <> halt SCM+FSAhence
CurInstr (
(P +* (if=0 (a,I,J))),
(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),l)))
<> halt SCM+FSA
by A6, A5, A27, PBOOLE:158;
verum end; suppose
l <> 0
;
not CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),b1))) = halt SCM+FSAthen consider n being
Nat such that A28:
l = n + 1
by NAT_1:6;
assume A29:
CurInstr (
(P +* (if=0 (a,I,J))),
(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),l)))
= halt SCM+FSA
;
contradictionreconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
InsCode (CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),n)))) =
InsCode (IncAddr ((CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),n)))),((card J) + 3)))
by COMPOS_1:def 38
.=
InsCode (CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1)),n))))
by A2, A23, A13, A16, Th11, A19, A1
.=
0
by A28, A29, EXTPRO_1:5, SCMFSA_2:124
;
then A30:
CurInstr (
(P +* (I ';' (Stop SCM+FSA))),
(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),n)))
= halt SCM+FSA
by SCMFSA_2:122;
n < LifeSpan (
(P +* (I ';' (Stop SCM+FSA))),
(s +* (Initialize ((intloc 0) .--> 1))))
by A26, A28, XREAL_1:8;
hence
contradiction
by A22, A30, EXTPRO_1:def 14;
verum end; end;
then
for l being Element of NAT st CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),l))) = halt SCM+FSA holds
(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 <= l
;
then A31:
LifeSpan ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 1
by A24, A25, EXTPRO_1:def 14;
A32: DataPart (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) =
DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))))))
by A20, A21, EXTPRO_1:23, SCMFSA8A:55
.=
DataPart (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1)),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))))))
by A2, A23, A13, A16, Th11, A1, A19
.=
DataPart (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)))
by EXTPRO_1:5
.=
DataPart (Result ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1)))))
by A25, A31, EXTPRO_1:23
;
A33:
now let x be
set ;
( x in dom (IExec ((if=0 (a,I,J)),P,s)) implies (IExec ((if=0 (a,I,J)),P,s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1 )A34:
IExec (
(I ';' (Stop SCM+FSA)),
P,
s)
= (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT)
by SCMFSA6B:def 1;
A35:
dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) = {(IC )}
by FUNCOP_1:19;
A36:
IExec (
(if=0 (a,I,J)),
P,
s)
= (Result ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT)
by SCMFSA6B:def 1;
A37:
dom (ProgramPart s) = NAT
by COMPOS_1:34;
assume A38:
x in dom (IExec ((if=0 (a,I,J)),P,s))
;
(IExec ((if=0 (a,I,J)),P,s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1per cases
( x is Int-Location or x is FinSeq-Location or x = IC or x is Element of NAT )
by A38, SCMFSA6A:35;
suppose A39:
x is
Int-Location
;
(IExec ((if=0 (a,I,J)),P,s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1then
x <> IC
by SCMFSA_2:81;
then A40:
not
x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A35, TARSKI:def 1;
thus (IExec ((if=0 (a,I,J)),P,s)) . x =
(Result ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))))) . x
by A36, A39, A37, FUNCT_4:12, SCMFSA10:3
.=
(Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) . x
by A32, A39, SCMFSA6A:38
.=
(IExec ((I ';' (Stop SCM+FSA)),P,s)) . x
by A34, A39, A37, FUNCT_4:12, SCMFSA10:3
.=
((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A40, FUNCT_4:12
;
verum end; suppose A41:
x is
FinSeq-Location
;
(IExec ((if=0 (a,I,J)),P,s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1then
x <> IC
by SCMFSA_2:82;
then A42:
not
x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A35, TARSKI:def 1;
thus (IExec ((if=0 (a,I,J)),P,s)) . x =
(Result ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))))) . x
by A36, A41, A37, FUNCT_4:12, SCMFSA10:4
.=
(Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) . x
by A32, A41, SCMFSA6A:38
.=
(IExec ((I ';' (Stop SCM+FSA)),P,s)) . x
by A34, A41, A37, FUNCT_4:12, SCMFSA10:4
.=
((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A42, FUNCT_4:12
;
verum end; suppose A43:
x = IC
;
(IExec ((if=0 (a,I,J)),P,s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1then A44:
x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A35, TARSKI:def 1;
A45:
not
x in dom (s | NAT)
by A43, A37, COMPOS_1:def 12;
A46:
IC (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) =
(IExec ((I ';' (Stop SCM+FSA)),P,s)) . (IC )
by A34, A43, A45, FUNCT_4:12
.=
IC ((IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA)))
by A20, A21, SCMFSA8A:57
.=
card I
by FUNCT_4:121
;
thus (IExec ((if=0 (a,I,J)),P,s)) . x =
(Result ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))))) . x
by A36, A45, FUNCT_4:12
.=
(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) . x
by A25, A31, EXTPRO_1:23
.=
IC (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1)),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))))))
by A43, EXTPRO_1:5
.=
(IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))))))) + ((card J) + 3)
by A2, A23, A13, A16, Th11, A19, A1
.=
(IC (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))))) + ((card J) + 3)
by A20, A21, EXTPRO_1:23, SCMFSA8A:55
.=
(Start-At (((card I) + ((card J) + 3)),SCM+FSA)) . (IC )
by A46, FUNCOP_1:87
.=
((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A43, A44, FUNCT_4:14
;
verum end; suppose A47:
x is
Element of
NAT
;
(IExec ((if=0 (a,I,J)),P,s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1then
x <> IC
by COMPOS_1:3;
then A48:
not
x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A35, TARSKI:def 1;
thus (IExec ((if=0 (a,I,J)),P,s)) . x =
(s | NAT) . x
by A36, A47, A12, FUNCT_4:14
.=
(IExec ((I ';' (Stop SCM+FSA)),P,s)) . x
by A34, A47, A12, FUNCT_4:14
.=
((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A48, FUNCT_4:12
;
verum end; end;
dom (IExec ((if=0 (a,I,J)),P,s)) =
the carrier of SCM+FSA
by PARTFUN1:def 4
.=
dom ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)))
by PARTFUN1:def 4
;
hence IExec ((if=0 (a,I,J)),P,s) =
(IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A33, FUNCT_1:9
.=
((IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A20, A21, SCMFSA8A:57
.=
(IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by FUNCT_4:122
;
verum