let p be Instruction-Sequence of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
let I be good InitHalting Program of SCM+FSA; :: thesis:
let a be read-write Int-Location; :: thesis:
assume A1: not I destroys a ; :: thesis:
reconsider J3 = Macro (SubFrom (a,(intloc 0))) as good Program of SCM+FSA ;
set I1 = I ";" (SubFrom (a,(intloc 0)));
set ss = IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s);
set pp = p;
I ";" (SubFrom (a,(intloc 0))) is_closed_onInit s,p by Th25;
then A2: I ";" (SubFrom (a,(intloc 0))) is_closed_on Initialized s,p by Th30;
I ";" (SubFrom (a,(intloc 0))) is_halting_onInit s,p by Th26;
then A3: ( I ";" (SubFrom (a,(intloc 0))) = I ";" J3 & I ";" (SubFrom (a,(intloc 0))) is_halting_on Initialized s,p ) by Th31;
then A4: (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . (intloc 0) = 1 by A2, SCMFSA8C:67;
set P = if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))));
set s0 = Initialized s;
set p0 = p;
assume A5: s . a > 0 ; :: thesis:
then A6: (Initialized s) . a > 0 by SCMFSA_M:37;
then consider s2 being State of SCM+FSA, p2 being Instruction-Sequence of SCM+FSA, k being Element of NAT such that
A7: s2 = Initialized (Initialized s) and
A8: p2 = p +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) and
k = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),((Initialized s) +* (Initialize ((intloc 0) .--> 1))))) + 1 and
A9: (Comput (p2,s2,k)) . a = ((Initialized s) . a) - 1 and
A10: (Comput (p2,s2,k)) . (intloc 0) = 1 and
A11: for b being read-write Int-Location st b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,(Initialized s))) . b and
A12: for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,(Initialized s))) . f and
A13: IC (Comput (p2,s2,k)) = 0 and
A14: for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A1, Th64;
A15: loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) c= p2 by A8, FUNCT_4:25;

A16: now :: thesis:

let f be FinSeq-Location ; :: thesis:
thus (Comput (p2,s2,k)) . f = (IExec (I,p,(Initialized s))) . f by A12
.= (Exec ((SubFrom (a,(intloc 0))),(IExec (I,p,(Initialized s))))) . f by SCMFSA_2:65
.= (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . f by Th24
.= (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . f by SCMFSA8C:3 ; :: thesis:

end;

A17: Initialize (Initialized s) = ((Initialized s) +* (Initialize ((intloc 0) .--> 1))) +* (Start-At (0,SCM+FSA)) by FUNCT_4:93
.= (Initialized s) +* ((Initialize ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:14
.= s2 by A7, FUNCT_4:93 ;
thus A18: (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a = (Exec ((SubFrom (a,(intloc 0))),(IExec (I,p,s)))) . a by Th23
.= ((IExec (I,p,s)) . a) - ((IExec (I,p,s)) . (intloc 0)) by SCMFSA_2:65
.= ((IExec (I,p,s)) . a) - 1 by Th9
.= ((Initialized s) . a) - 1 by A1, Th53
.= (s . a) - 1 by SCMFSA_M:37 ; :: thesis:

let b be Int-Location; :: thesis:

suppose b = intloc 0 ; :: thesis:

hence (Comput (p2,s2,k)) . b = (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . b by A10, A3, A2, SCMFSA8C:67; :: thesis:

end;

suppose b = a ; :: thesis:

hence (Comput (p2,s2,k)) . b = (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . b by A9, A18, SCMFSA_M:37; :: thesis:

end;

suppose A19: ( b <> a & b <> intloc 0 ) ; :: thesis:

then reconsider bb = b as read-write Int-Location by SCMFSA_M:def 2;
thus (Comput (p2,s2,k)) . b = (IExec (I,p,(Initialized s))) . bb by A11, A19
.= (Exec ((SubFrom (a,(intloc 0))),(IExec (I,p,(Initialized s))))) . b by A19, SCMFSA_2:65
.= (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . b by Th23
.= (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . b by SCMFSA8C:3 ; :: thesis:

end;

end;

end;

then A20: DataPart (Comput (p2,s2,k)) = DataPart (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) by A16, SCMFSA_M:2;
set s21 = Initialize (Initialized s);
set p21 = p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA));
set ss0 = Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s));
set s31 = Initialize (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)));
set p31 = p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA));
0 in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) by SCMFSA8C:25;
then A21: 0 in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by FUNCT_4:99;
A22: (Initialized s) . (intloc 0) = 1 by SCMFSA_M:9;
then A23: loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on Initialized s,p by A1, A6, Th60;
A24: Directed (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) = loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) by SCMFSA6A:22;
then A25: Directed (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) is_pseudo-closed_on Initialized s,p by A1, A22, A6, Th60;
A26: DataPart (IExec ((Times (a,I)),p,(Initialized s))) = DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA)),p,(Initialized s))) by A1, A22, A6, A24, Th60, SCMFSA8C:40;

per cases ) . a = 0 or (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a <> 0 ) ;

suppose A27: (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a = 0 ; :: thesis:

A28: (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . ((card (I ";" (SubFrom (a,(intloc 0))))) + 3) = goto ((card (I ";" (SubFrom (a,(intloc 0))))) + 5) by SCMFSA8C:36;
A29: (card (I ";" (SubFrom (a,(intloc 0))))) + (3 + 2) = ((card (I ";" (SubFrom (a,(intloc 0))))) + 1) + 4
.= ((card (Goto 2)) + (card (I ";" (SubFrom (a,(intloc 0)))))) + 4 by SCMFSA8A:15
.= card (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) by SCMFSA8B:11
.= card (dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by CARD_1:62
.= card (dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) by FUNCT_4:99
.= card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by CARD_1:62 ;
then ((card (I ";" (SubFrom (a,(intloc 0))))) + 3) + 0 < card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by XREAL_1:6;
then A30: (card (I ";" (SubFrom (a,(intloc 0))))) + 3 in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by AFINSQ_1:66;
p2 . ((card (I ";" (SubFrom (a,(intloc 0))))) + 3) = (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) . ((card (I ";" (SubFrom (a,(intloc 0))))) + 3) by A30, A15, GRFUNC_1:2;
then A31: p2 . ((card (I ";" (SubFrom (a,(intloc 0))))) + 3) = goto ((card (I ";" (SubFrom (a,(intloc 0))))) + 5) by A28, FUNCT_4:105;
A32: p2 . 0 = (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) . 0 by A21, A15, GRFUNC_1:2;
A33: Comput (p2,s2,(k + 1)) = Following (p2,(Comput (p2,s2,k))) by EXTPRO_1:3
.= Exec ((p2 . 0),(Comput (p2,s2,k))) by A13, PBOOLE:143 ;
A34: (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . 0 = a =0_goto ((card (I ";" (SubFrom (a,(intloc 0))))) + 3) by SCMFSA8C:26;
A35: p2 . 0 = a =0_goto ((card (I ";" (SubFrom (a,(intloc 0))))) + 3) by A32, A34, FUNCT_4:105;
then InsCode (p2 . 0) = 7 by SCMFSA_2:24;
then InsCode (p2 . 0) in {0,6,7,8} by ENUMSET1:def 2;
then A36: DataPart (Comput (p2,s2,k)) = DataPart (Comput (p2,s2,(k + 1))) by A33, SCMFSA8C:12;
A37: (Comput (p2,s2,k)) . a = 0 by A9, A18, A27, SCMFSA_M:37;
then A38: IC (Comput (p2,s2,(k + 1))) = (card (I ";" (SubFrom (a,(intloc 0))))) + 3 by A33, A35, SCMFSA_2:70;

A39: now :: thesis:

let n be Element of NAT ; :: thesis:
assume A40: not IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ; :: thesis:
then k < n by A14;
then k + 1 <= n by INT_1:7;
then k + 1 < n by A38, A30, A40, XXREAL_0:1;
then (k + 1) + 1 <= n by INT_1:7;
hence k + (1 + 1) <= n ; :: thesis:

end;

A41: p2 /. (IC (Comput (p2,s2,(k + 1)))) = p2 . (IC (Comput (p2,s2,(k + 1)))) by PBOOLE:143;
A42: Comput (p2,s2,(k + (1 + 1))) = Comput (p2,s2,((k + 1) + 1))
.= Following (p2,(Comput (p2,s2,(k + 1)))) by EXTPRO_1:3
.= Exec ((p2 . ((card (I ";" (SubFrom (a,(intloc 0))))) + 3)),(Comput (p2,s2,(k + 1)))) by A37, A33, A35, A41, SCMFSA_2:70 ;
then A43: IC (Comput ((p +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize (Initialized s)),(k + 2))) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A8, A17, A29, A31, SCMFSA_2:69;
A44: k + 2 = pseudo-LifeSpan ((Initialized s),p,(loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) by A43, A8, A17, A23, A39, SCMFSA8A:def 4;
InsCode (p2 . ((card (I ";" (SubFrom (a,(intloc 0))))) + 3)) = 6 by A31, SCMFSA_2:23;
then InsCode (p2 . ((card (I ";" (SubFrom (a,(intloc 0))))) + 3)) in {0,6,7,8} by ENUMSET1:def 2;
then A45: DataPart (Comput (p2,s2,k)) = DataPart (Comput (p2,s2,(k + 2))) by A36, A42, SCMFSA8C:12;
A46: Initialize (Initialized s) = s +* ((Initialize ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:14
.= Initialized s by FUNCT_4:93 ;
A47: s2 = (Initialized s) +* ((Initialize ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) by A7, FUNCT_4:93
.= ((Initialized s) +* (Initialize ((intloc 0) .--> 1))) +* (Start-At (0,SCM+FSA)) by FUNCT_4:14
.= (Initialized s) +* (Start-At (0,SCM+FSA)) by FUNCT_4:93 ;
thus DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(Initialized s))) by SCMFSA8C:3
.= DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA)),p,s)) by A26, SCMFSA8C:3
.= DataPart (Result ((p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)))) by A46, SCMFSA6B:def 1
.= DataPart (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) by A20, A45, A47, A24, A1, A22, A6, Th60, A8, A44, SCMFSA8C:30
.= DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) by A4, A27, Th65 ; :: thesis:

end;

suppose A48: (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a <> 0 ; :: thesis:

s . a >= 0 + 1 by A5, INT_1:7;
then A49: (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a > 0 by A18, A48, XREAL_1:19;
A50: k < pseudo-LifeSpan ((Initialized s),p,(loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) by A14, A8, A22, A17, A1, A6, Th60, SCMFSA8C:1;
then A51: DataPart (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)),k)) = DataPart (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) by A24, A25, A20, A17, A8, SCMFSA8C:29;

A52: now :: thesis:

A53: DataPart (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s))) = (DataPart (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) +* {}
.= (DataPart (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) +* (DataPart (Start-At (0,SCM+FSA))) by MEMSTR_0:20
.= DataPart (Initialize (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) by FUNCT_4:71 ;

hereby :: thesis:

let a be Int-Location; :: thesis:

suppose A54: a = intloc 0 ; :: thesis:

thus (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)),k)) . a = (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a by A51, SCMFSA_M:2
.= 1 by A54, Th9
.= (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s))) . a by A54, SCMFSA_M:9
.= (Initialize (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) . a by A53, SCMFSA_M:2 ; :: thesis:

end;

suppose a <> intloc 0 ; :: thesis:

then A55: a is read-write Int-Location by SCMFSA_M:def 2;
thus (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)),k)) . a = (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a by A51, SCMFSA_M:2
.= (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s))) . a by A55, SCMFSA_M:37
.= (Initialize (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) . a by A53, SCMFSA_M:2 ; :: thesis:

end;

end;

end;

let f be FinSeq-Location ; :: thesis:
thus (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)),k)) . f = (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . f by A51, SCMFSA_M:2
.= (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s))) . f by SCMFSA_M:37
.= (Initialize (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) . f by A53, SCMFSA_M:2 ; :: thesis:

end;

A56: IC (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)),k)) = IC (Comput (p2,s2,k)) by A24, A25, A50, A8, A17, SCMFSA8C:29
.= IC (Initialize (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) by A13, FUNCT_4:113 ;
A57: (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . (intloc 0) = 1 by A3, A2, SCMFSA8C:67;
A58: DataPart (Initialized s) = (DataPart (Initialized s)) +* {}
.= (DataPart (Initialized s)) +* (DataPart (Start-At (0,SCM+FSA))) by MEMSTR_0:20
.= DataPart (Initialize (Initialized s)) by FUNCT_4:71 ;
Directed (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) = loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) by SCMFSA6A:22;
then Directed (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) is_pseudo-closed_on Initialize (Initialized s),p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA)) by A1, A22, A6, Th60, A58, SCMFSA8C:23;
then A59: ( (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA) is_closed_on Initialize (Initialized s),p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA)) & (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA) is_halting_on Initialize (Initialized s),p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA)) ) by SCMFSA8C:29;
A60: Initialize (Initialized s) = s +* ((Initialize ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:14
.= Initialized s by FUNCT_4:93 ;
A61: Initialize (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s))) = (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) +* ((Initialize ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:14
.= Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) by FUNCT_4:93 ;
A62: ( (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA) c= p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA)) & (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA) c= p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA)) ) by FUNCT_4:25;
A63: Result ((p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s))) = Result ((p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s))))) by A59, A56, A62, A52, SCMFSA8C:73, SCMFSA_2:61;
DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA)),p,(Initialized s))) = DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA)),p,s)) by SCMFSA8C:3
.= DataPart (Result ((p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized s)))) by A60, SCMFSA6B:def 1
.= DataPart (Result ((p +* ((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA))),(Initialize (Initialized (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))))) by A63
.= DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ";" (Stop SCM+FSA)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) by A61, SCMFSA6B:def 1
.= DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) by A1, A24, A57, A49, Th60, SCMFSA8C:40 ;
hence DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) by A26, SCMFSA8C:3; :: thesis:

end;

end;