let P be Instruction-Sequence of SCM+FSA; for I, J being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st s . a <> 0 & J is_closed_on Initialized s,P & J is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (J,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
for s being State of SCM+FSA st s . a <> 0 & J is_closed_on Initialized s,P & J is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let a be read-write Int-Location ; for s being State of SCM+FSA st s . a <> 0 & J is_closed_on Initialized s,P & J is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let s be State of SCM+FSA; ( s . a <> 0 & J is_closed_on Initialized s,P & J is_halting_on Initialized s,P implies IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
set I1 = I ';' (Stop SCM+FSA);
set JI2 = ((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA);
set s2 = Initialized s;
set P2 = P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA));
A1:
((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) c= P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))
by FUNCT_4:25;
set P3 = P +* (if=0 (a,I,J));
set s4 = Comput ((P +* (if=0 (a,I,J))),(Initialized s),1);
set s5 = Comput ((P +* (if=0 (a,I,J))),(Initialized s),2);
set i = a =0_goto ((card J) + 3);
0 in dom (if=0 (a,I,J))
by Lm2;
then A3: (P +* (if=0 (a,I,J))) . 0 =
(if=0 (a,I,J)) . 0
by FUNCT_4:13
.=
a =0_goto ((card J) + 3)
by Lm3
;
A5:
1 in dom (if=0 (a,I,J))
by Lm2;
A6: (P +* (if=0 (a,I,J))) . 1 =
(if=0 (a,I,J)) . 1
by A5, FUNCT_4:13
.=
goto 2
by Lm3
;
L1:
dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )}
by SCMFSA6A:42;
( a <> intloc 0 & a <> IC )
by SCMFSA_2:56;
then B9:
not a in dom (Initialize ((intloc 0) .--> 1))
by L1, TARSKI:def 2;
IC in dom (Initialize ((intloc 0) .--> 1))
by MEMSTR_0:48;
then A7: IC (Initialized s) =
IC (Initialize ((intloc 0) .--> 1))
by FUNCT_4:13
.=
0
by MEMSTR_0:def 8
;
if=0 (a,I,J) =
(((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA))
by SCMFSA6A:25
.=
((a =0_goto ((card J) + 3)) ';' J) ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))
by SCMFSA6A:25
.=
(a =0_goto ((card J) + 3)) ';' (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA))))
by SCMFSA6A:29
.=
(a =0_goto ((card J) + 3)) ';' ((J ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA)))
by SCMFSA6A:25
.=
(Macro (a =0_goto ((card J) + 3))) ';' (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))
by SCMFSA6A:25
;
then
Reloc ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),(card (Macro (a =0_goto ((card J) + 3))))) c= if=0 (a,I,J)
by Lm1;
then A8:
Reloc ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),2) c= if=0 (a,I,J)
by COMPOS_1:56;
if=0 (a,I,J) c= P +* (if=0 (a,I,J))
by FUNCT_4:25;
then A12:
Reloc ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),2) c= P +* (if=0 (a,I,J))
by A8, XBOOLE_1:1;
A13: Comput ((P +* (if=0 (a,I,J))),(Initialized s),(0 + 1)) =
Following ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),0)))
by EXTPRO_1:3
.=
Following ((P +* (if=0 (a,I,J))),(Initialized s))
by EXTPRO_1:2
.=
Exec ((a =0_goto ((card J) + 3)),(Initialized s))
by A7, A3, PBOOLE:143
;
assume
s . a <> 0
; ( not J is_closed_on Initialized s,P or not J is_halting_on Initialized s,P or IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
then
(Initialized s) . a <> 0
by B9, FUNCT_4:11;
then A14: IC (Comput ((P +* (if=0 (a,I,J))),(Initialized s),1)) =
succ 0
by A7, A13, SCMFSA_2:70
.=
0 + 1
;
assume A15:
J is_closed_on Initialized s,P
; ( not J is_halting_on Initialized s,P or IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
A16: Comput ((P +* (if=0 (a,I,J))),(Initialized s),(1 + 1)) =
Following ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),1)))
by EXTPRO_1:3
.=
Exec ((goto 2),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),1)))
by A14, A6, PBOOLE:143
;
then A17:
IC (Comput ((P +* (if=0 (a,I,J))),(Initialized s),2)) = 2
by SCMFSA_2:69;
A19:
now let f be
FinSeq-Location ;
(Initialized s) . f = (Comput ((P +* (if=0 (a,I,J))),(Initialized s),2)) . fthus (Initialized s) . f =
(Comput ((P +* (if=0 (a,I,J))),(Initialized s),1)) . f
by A13, SCMFSA_2:70
.=
(Comput ((P +* (if=0 (a,I,J))),(Initialized s),2)) . f
by A16, SCMFSA_2:69
;
verum end;
now let a be
Int-Location ;
(Initialized s) . a = (Comput ((P +* (if=0 (a,I,J))),(Initialized s),2)) . athus (Initialized s) . a =
(Comput ((P +* (if=0 (a,I,J))),(Initialized s),1)) . a
by A13, SCMFSA_2:70
.=
(Comput ((P +* (if=0 (a,I,J))),(Initialized s),2)) . a
by A16, SCMFSA_2:69
;
verum end;
then A20:
DataPart (Initialized s) = DataPart (Comput ((P +* (if=0 (a,I,J))),(Initialized s),2))
by A19, SCMFSA6A:7;
assume A21:
J is_halting_on Initialized s,P
; IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
then A22:
P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) halts_on Initialized s
by A15, SCMFSA8A:39;
((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) is_closed_on Initialized s,P
by A15, A21, SCMFSA8A:37;
then A23:
((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) is_closed_on Initialized s,P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))
by Th9;
A24: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),((LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))) + 2)))) =
CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),2)),(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))))))
by EXTPRO_1:4
.=
IncAddr ((CurInstr ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s),(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))))))),2)
by A23, A12, A17, A20, Th11, A1
.=
IncAddr ((halt SCM+FSA),2)
by A22, EXTPRO_1:def 15
.=
halt SCM+FSA
by COMPOS_1:11
;
then A25:
P +* (if=0 (a,I,J)) halts_on Initialized s
by EXTPRO_1:29;
now let l be
Element of
NAT ;
( l < (LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))) + 2 implies CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),b1))) <> halt SCM+FSA )assume A26:
l < (LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))) + 2
;
CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),b1))) <> halt SCM+FSAA27:
Comput (
(P +* (if=0 (a,I,J))),
(Initialized s),
0)
= Initialized s
by EXTPRO_1:2;
per cases
( l = 0 or l = 1 or ( l <> 0 & l <> 1 ) )
;
suppose
l = 0
;
CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),b1))) <> halt SCM+FSAhence
CurInstr (
(P +* (if=0 (a,I,J))),
(Comput ((P +* (if=0 (a,I,J))),(Initialized s),l)))
<> halt SCM+FSA
by A7, A3, A27, PBOOLE:143;
verum end; suppose A28:
(
l <> 0 &
l <> 1 )
;
not CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),b1))) = halt SCM+FSAassume A29:
CurInstr (
(P +* (if=0 (a,I,J))),
(Comput ((P +* (if=0 (a,I,J))),(Initialized s),l)))
= halt SCM+FSA
;
contradictionconsider n being
Nat such that A30:
l = n + 1
by A28, NAT_1:6;
n <> 0
by A28, A30;
then consider l2 being
Nat such that A31:
n = l2 + 1
by NAT_1:6;
reconsider l2 =
l2 as
Element of
NAT by ORDINAL1:def 12;
A32:
Comput (
(P +* (if=0 (a,I,J))),
(Initialized s),
(l2 + (1 + 1)))
= Comput (
(P +* (if=0 (a,I,J))),
(Comput ((P +* (if=0 (a,I,J))),(Initialized s),(1 + 1))),
l2)
by EXTPRO_1:4;
InsCode (CurInstr ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s),l2)))) =
InsCode (IncAddr ((CurInstr ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s),l2)))),2))
by COMPOS_1:def 17
.=
0
by A30, A31, A29, A32, A23, A17, A20, Th11, A12, A1, SCMFSA_2:97
;
then A33:
CurInstr (
(P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),
(Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s),l2)))
= halt SCM+FSA
by SCMFSA_2:95;
n + 1
< ((LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))) + 1) + 1
by A26, A30;
then
n < (LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))) + 1
by XREAL_1:6;
then
l2 < LifeSpan (
(P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),
(Initialized s))
by A31, XREAL_1:6;
hence
contradiction
by A22, A33, EXTPRO_1:def 15;
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))),(Initialized s),l))) = halt SCM+FSA holds
(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))) + 2 <= l
;
then A34:
LifeSpan ((P +* (if=0 (a,I,J))),(Initialized s)) = (LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))) + 2
by A24, A25, EXTPRO_1:def 15;
A35: DataPart (Result ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))) =
DataPart (Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s),(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s)))))
by A21, A15, EXTPRO_1:23, SCMFSA8A:39
.=
DataPart (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),2)),(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s)))))
by A23, A17, A20, Th11, A12, A1
.=
DataPart (Comput ((P +* (if=0 (a,I,J))),(Initialized s),((LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))) + 2)))
by EXTPRO_1:4
.=
DataPart (Result ((P +* (if=0 (a,I,J))),(Initialized s)))
by A25, A34, EXTPRO_1:23
;
A36:
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 ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1 )A37:
dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) = {(IC )}
by FUNCOP_1:13;
A38:
IExec (
(if=0 (a,I,J)),
P,
s)
= Result (
(P +* (if=0 (a,I,J))),
(Initialized s))
by SCMFSA6B:def 1;
A39:
IExec (
(((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),
P,
s)
= Result (
(P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),
(Initialized s))
by SCMFSA6B:def 1;
assume A40:
x in dom (IExec ((if=0 (a,I,J)),P,s))
;
(IExec ((if=0 (a,I,J)),P,s)) . b1 = ((IExec ((((J ';' (Goto ((card I) + 1))) ';' 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 )
by A40, SCMFSA6A:5;
suppose A41:
x is
Int-Location
;
(IExec ((if=0 (a,I,J)),P,s)) . b1 = ((IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1then
x <> IC
by SCMFSA_2:56;
then A42:
not
x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A37, TARSKI:def 1;
thus (IExec ((if=0 (a,I,J)),P,s)) . x =
(Result ((P +* (if=0 (a,I,J))),(Initialized s))) . x
by A38
.=
(Result ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))) . x
by A35, A41, SCMFSA6A:7
.=
(IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) . x
by A39
.=
((IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A42, FUNCT_4:11
;
verum end; suppose A43:
x is
FinSeq-Location
;
(IExec ((if=0 (a,I,J)),P,s)) . b1 = ((IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1then
x <> IC
by SCMFSA_2:57;
then A44:
not
x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A37, TARSKI:def 1;
thus (IExec ((if=0 (a,I,J)),P,s)) . x =
(Result ((P +* (if=0 (a,I,J))),(Initialized s))) . x
by A38
.=
(Result ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))) . x
by A35, A43, SCMFSA6A:7
.=
(IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) . x
by A39
.=
((IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A44, FUNCT_4:11
;
verum end; suppose A45:
x = IC
;
(IExec ((if=0 (a,I,J)),P,s)) . b1 = ((IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1then A46:
x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A37, TARSKI:def 1;
A48:
IC (Result ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))) =
IC (IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s))
by A39
.=
((card I) + (card J)) + 1
by A15, A21, SCMFSA8A:40
;
thus (IExec ((if=0 (a,I,J)),P,s)) . x =
(Result ((P +* (if=0 (a,I,J))),(Initialized s))) . x
by A38
.=
(Comput ((P +* (if=0 (a,I,J))),(Initialized s),((LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s))) + 2))) . x
by A25, A34, EXTPRO_1:23
.=
IC (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),2)),(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s)))))
by A45, EXTPRO_1:4
.=
(IC (Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s),(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s)))))) + 2
by A23, A17, A20, Th11, A12, A1
.=
(IC (Result ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialized s)))) + 2
by A21, A15, EXTPRO_1:23, SCMFSA8A:39
.=
(Start-At (((((card I) + (card J)) + 1) + 2),SCM+FSA)) . (IC )
by A48, FUNCOP_1:72
.=
((IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A45, A46, FUNCT_4:13
;
verum end; end;
dom (IExec ((if=0 (a,I,J)),P,s)) =
the carrier of SCM+FSA
by PARTFUN1:def 2
.=
dom ((IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)))
by PARTFUN1:def 2
;
hence IExec ((if=0 (a,I,J)),P,s) =
(IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A36, FUNCT_1:2
.=
((IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A15, A21, SCMFSA8A:41
.=
(IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by FUNCT_4:114
;
verum