let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . a > 0 holds
( (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)))) )
let s be State of SCM+FSA; :: thesis: for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . a > 0 holds
( (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)))) )
let I be good InitHalting Program of SCM+FSA; :: thesis: for a being read-write Int-Location st not I destroys a & s . a > 0 holds
( (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)))) )
let a be read-write Int-Location ; :: thesis: ( not I destroys a & s . a > 0 implies ( (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)))) ) )
assume A1: not I destroys a ; :: thesis: ( not s . a > 0 or ( (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)))) ) )
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 Th35;
then A2: I ';' (SubFrom (a,(intloc 0))) is_closed_on Initialized s,p by Th40;
I ';' (SubFrom (a,(intloc 0))) is_halting_onInit s,p by Th36;
then A3: ( I ';' (SubFrom (a,(intloc 0))) = I ';' J3 & I ';' (SubFrom (a,(intloc 0))) is_halting_on Initialized s,p ) by Th41;
then A4: (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . (intloc 0) = 1 by A2, SCMFSA8C:96;
set P = if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))));
set s0 = Initialized s;
set p0 = p;
A5: ProgramPart (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) = loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by RELAT_1:209;
assume A6: s . a > 0 ; :: thesis: ( (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)))) )
then A7: (Initialized s) . a > 0 by SCMFSA6C:3;
then consider s2 being State of SCM+FSA, p2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT , k being Element of NAT such that
A8: s2 = (Initialized s) +* (Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) and
A9: 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) +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1 and
A10: (Comput (p2,s2,k)) . a = ((Initialized s) . a) - 1 and
A11: (Comput (p2,s2,k)) . (intloc 0) = 1 and
A12: for b being read-write Int-Location st b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,(Initialized s))) . b and
A13: for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,(Initialized s))) . f and
A14: IC (Comput (p2,s2,k)) = 0 and
A15: 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, Th77;
A16: loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) c= p2 by A9, FUNCT_4:26;
A17: s2 = (Initialized (Initialized s)) +* (Initialize (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by A8, SCMFSA8A:13
.= (Initialized s) +* (Initialize (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by SCMFSA8C:15 ;
A18: now
let f be FinSeq-Location ; :: thesis: (Comput (p2,s2,k)) . f = (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . f
thus (Comput (p2,s2,k)) . f = (IExec (I,p,(Initialized s))) . f by A13
.= (Exec ((SubFrom (a,(intloc 0))),(IExec (I,p,(Initialized s))))) . f by SCMFSA_2:91
.= (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,(Initialized s))) . f by Th34
.= (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . f by SCMFSA8C:17 ; :: thesis: verum
end;
thus A19: (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a = (Exec ((SubFrom (a,(intloc 0))),(IExec (I,p,s)))) . a by Th33
.= ((IExec (I,p,s)) . a) - ((IExec (I,p,s)) . (intloc 0)) by SCMFSA_2:91
.= ((IExec (I,p,s)) . a) - 1 by Th17
.= ((Initialized s) . a) - 1 by A1, Th63
.= (s . a) - 1 by SCMFSA6C:3 ; :: thesis: DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))))
now
let b be Int-Location ; :: thesis: (Comput (p2,s2,k)) . b1 = (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . b1
per cases ( b = intloc 0 or b = a or ( b <> a & b <> intloc 0 ) ) ;
suppose b = intloc 0 ; :: thesis: (Comput (p2,s2,k)) . b1 = (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . b1
hence (Comput (p2,s2,k)) . b = (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . b by A11, A3, A2, SCMFSA8C:96; :: thesis: verum
end;
suppose b = a ; :: thesis: (Comput (p2,s2,k)) . b1 = (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . b1
hence (Comput (p2,s2,k)) . b = (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . b by A10, A19, SCMFSA6C:3; :: thesis: verum
end;
suppose A20: ( b <> a & b <> intloc 0 ) ; :: thesis: (Comput (p2,s2,k)) . b1 = (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . b1
then reconsider bb = b as read-write Int-Location by SF_MASTR:def 5;
thus (Comput (p2,s2,k)) . b = (IExec (I,p,(Initialized s))) . bb by A12, A20
.= (Exec ((SubFrom (a,(intloc 0))),(IExec (I,p,(Initialized s))))) . b by A20, SCMFSA_2:91
.= (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,(Initialized s))) . b by Th33
.= (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . b by SCMFSA8C:17 ; :: thesis: verum
end;
end;
end;
then A21: DataPart (Comput (p2,s2,k)) = DataPart (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) by A18, SCMFSA6A:38;
set s21 = (Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)));
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 = (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)));
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:54;
then A22: 0 in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:105;
A23: (Initialized s) . (intloc 0) = 1 by SCMFSA6C:3;
then A24: loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on Initialized s,p by A1, A7, Th73;
A25: 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:63;
then A26: Directed (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) is_pseudo-closed_on Initialized s,p by A1, A23, A7, Th73;
A27: 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, A23, A7, A25, Th73, SCMFSA8C:69;
per cases ( (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a = 0 or (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a <> 0 ) ;
suppose A28: (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a = 0 ; :: thesis: DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))))
A29: (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:65;
A30: (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:29
.= card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by SCMFSA8B:14
.= card (dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by CARD_1:104
.= card (dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by FUNCT_4:105
.= card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by CARD_1:104 ;
then ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) + 0 < card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by XREAL_1:8;
then A31: (card (I ';' (SubFrom (a,(intloc 0))))) + 3 in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by AFINSQ_1:70;
p2 . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) = 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 A31, GRFUNC_1:8, A16 ;
then A32: p2 . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) = goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 5) by A29, FUNCT_4:111;
A33: p2 . 0 = p2 . 0
.= (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) . 0 by A22, GRFUNC_1:8, A16 ;
A34: Comput (p2,s2,(k + 1)) = Following (p2,(Comput (p2,s2,k))) by EXTPRO_1:4
.= Exec ((p2 . 0),(Comput (p2,s2,k))) by A14, PBOOLE:158 ;
A35: (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . 0 = a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) by SCMFSA8C:55;
A36: p2 . 0 = a =0_goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) by A33, A35, FUNCT_4:111;
then InsCode (p2 . 0) = 7 by SCMFSA_2:48;
then InsCode (p2 . 0) in {0,6,7,8} by ENUMSET1:def 2;
then A37: DataPart (Comput (p2,s2,k)) = DataPart (Comput (p2,s2,(k + 1))) by A34, SCMFSA8C:32;
A38: (Comput (p2,s2,k)) . a = 0 by A10, A19, A28, SCMFSA6C:3;
then A39: IC (Comput (p2,s2,(k + 1))) = (card (I ';' (SubFrom (a,(intloc 0))))) + 3 by A34, A36, SCMFSA_2:96;
A40: now
let n be Element of NAT ; :: thesis: ( not IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) implies k + (1 + 1) <= n )
assume A41: not IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ; :: thesis: k + (1 + 1) <= n
then k < n by A15;
then k + 1 <= n by INT_1:20;
then k + 1 < n by A39, A31, A41, XXREAL_0:1;
then (k + 1) + 1 <= n by INT_1:20;
hence k + (1 + 1) <= n ; :: thesis: verum
end;
A42: p2 /. (IC (Comput (p2,s2,(k + 1)))) = p2 . (IC (Comput (p2,s2,(k + 1)))) by PBOOLE:158;
A43: Comput (p2,s2,(k + (1 + 1))) = Comput (p2,s2,((k + 1) + 1))
.= Following (p2,(Comput (p2,s2,(k + 1)))) by EXTPRO_1:4
.= Exec ((p2 . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)),(Comput (p2,s2,(k + 1)))) by A38, A34, A36, A42, SCMFSA_2:96 ;
then IC (Comput (p2,s2,(k + 2))) = (card (I ';' (SubFrom (a,(intloc 0))))) + 5 by A32, SCMFSA_2:95
.= card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A30 ;
then A44: k + 2 = pseudo-LifeSpan ((Initialized s),p,(loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by A17, A24, A40, SCMFSA8A:def 5, A9, A5;
InsCode (p2 . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3)) = 6 by A32, SCMFSA_2:47;
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 A37, A43, SCMFSA8C:32;
A46: (Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))) = s +* (Initialized ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))) by SCMFSA8A:13;
thus DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(Initialized s))) by SCMFSA8C:17
.= DataPart (IExec (((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)),p,s)) by A27, SCMFSA8C:17
.= DataPart ((Result ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))))) +* (s | NAT)) by A46, SCMFSA6B:def 1
.= DataPart (Result ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))))) by COMPOS_1:82
.= DataPart (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) by A1, A23, A7, A17, A25, A21, A44, A45, Th73, SCMFSA8C:59, A9
.= DataPart (IExec ((Times (a,I)),p,(IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)))) by A4, A28, Th78 ; :: thesis: verum
end;
suppose A47: (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a <> 0 ; :: thesis: DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))))
s . a >= 0 + 1 by A6, INT_1:20;
then A48: (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a > 0 by A19, A47, XREAL_1:21;
A49: ( Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) c= (Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))) & Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) c= (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))) ) by FUNCT_4:26;
loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on Initialized s,p by A1, A23, A7, Th73;
then A50: k < pseudo-LifeSpan ((Initialized s),p,(loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by A15, A17, SCMFSA8C:2, A9, A5;
then A51: DataPart (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))),k)) = DataPart (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) by A17, A25, A26, A21, SCMFSA8C:58, A9;
A52: now
A53: DataPart (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) = DataPart ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))) by SCMFSA8A:11;
hereby :: thesis: for f being FinSeq-Location holds (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))),k)) . f = ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))) . f
let a be Int-Location ; :: thesis: (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))),k)) . b1 = ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))) . b1
per cases ( a = intloc 0 or a <> intloc 0 ) ;
suppose A54: a = intloc 0 ; :: thesis: (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))),k)) . b1 = ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))) . b1
thus (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))),k)) . a = (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a by A51, SCMFSA6A:38
.= 1 by A54, Th17
.= (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) . a by A54, SCMFSA6C:3
.= ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))) . a by A53, SCMFSA6A:38 ; :: thesis: verum
end;
suppose a <> intloc 0 ; :: thesis: (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))),k)) . b1 = ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))) . b1
then A55: a is read-write Int-Location by SF_MASTR:def 5;
thus (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))),k)) . a = (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a by A51, SCMFSA6A:38
.= (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) . a by A55, SCMFSA6C:3
.= ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))) . a by A53, SCMFSA6A:38 ; :: thesis: verum
end;
end;
end;
let f be FinSeq-Location ; :: thesis: (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))),k)) . f = ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))) . f
thus (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))),k)) . f = (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . f by A51, SCMFSA6A:38
.= (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) . f by SCMFSA6C:3
.= ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))) . f by A53, SCMFSA6A:38 ; :: thesis: verum
end;
IC (Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))),k)) = IC (Comput (p2,s2,k)) by A17, A25, A26, A50, SCMFSA8C:58, A9
.= IC (Initialize ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))) by A14, FUNCT_4:121
.= IC ((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))) by FUNCT_4:15 ;
then A56: Comput ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))),k),(Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))) equal_outside NAT by A52, SCMFSA10:91;
A57: (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . (intloc 0) = 1 by A3, A2, SCMFSA8C:96;
( Directed (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) = loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) & DataPart (Initialized s) = DataPart ((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))) ) by SCMFSA6A:63, SCMFSA8A:11;
then Directed (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) is_pseudo-closed_on (Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) by A1, A23, A7, Th73, SCMFSA8C:52;
then A58: ( (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA) is_closed_on (Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),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 (Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)) ) by SCMFSA8C:58;
A59: (Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))) = s +* (Initialized ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))) by SCMFSA8A:13;
A60: (Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))) = (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) +* (Initialized ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))) by SCMFSA8A:13;
A61: ( (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:26;
A62: Result ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))))), Result ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))))) equal_outside NAT by A49, A58, A56, SCMFSA8C:103, A61;
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:17
.= DataPart ((Result ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))))) +* (s | NAT)) by A59, SCMFSA6B:def 1
.= DataPart (Result ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized s) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))))) by COMPOS_1:82
.= DataPart (Result ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))))) by COMPOS_1:138, A62
.= DataPart ((Result ((p +* ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA))),((Initialized (IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s))) +* (Initialize ((loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ';' (Stop SCM+FSA)))))) +* ((IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) | NAT)) by COMPOS_1:82
.= 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 A60, SCMFSA6B:def 1
.= DataPart (IExec ((Times (a,I)),p,(IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)))) by A1, A25, A57, A48, Th73, SCMFSA8C:69 ;
hence DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)))) by A27, SCMFSA8C:17; :: thesis: verum
end;
end;