:: SCMFSA_3 semantic presentation

begin

theorem :: SCMFSA_3:1
canceled;

theorem :: SCMFSA_3:2
canceled;


theorem :: SCMFSA_3:3
for s being State of SCM+FSA
for iloc being Element of NAT
for a being Int-Location holds s . a = (s +* (Start-At (iloc,SCM+FSA))) . a
proof
let s be State of SCM+FSA; ::_thesis: for iloc being Element of NAT
for a being Int-Location holds s . a = (s +* (Start-At (iloc,SCM+FSA))) . a
let iloc be Element of NAT ; ::_thesis: for a being Int-Location holds s . a = (s +* (Start-At (iloc,SCM+FSA))) . a
let a be Int-Location; ::_thesis: s . a = (s +* (Start-At (iloc,SCM+FSA))) . a
 a in the carrier of SCM+FSA ;
then  a in dom s by PARTFUN1:def_2;
then A1: ( dom (Start-At (iloc,SCM+FSA)) = {(IC )} & a in (dom s) \/ (dom (Start-At (iloc,SCM+FSA))) ) by FUNCOP_1:13, XBOOLE_0:def_3;
 a <> IC by SCMFSA_2:56;
then  not a in {(IC )} by TARSKI:def_1;
hence  s . a = (s +* (Start-At (iloc,SCM+FSA))) . a by A1, FUNCT_4:def_1; ::_thesis: verum
end;

theorem :: SCMFSA_3:4
for s being State of SCM+FSA
for iloc being Element of NAT
for a being FinSeq-Location holds s . a = (s +* (Start-At (iloc,SCM+FSA))) . a
proof
let s be State of SCM+FSA; ::_thesis: for iloc being Element of NAT
for a being FinSeq-Location holds s . a = (s +* (Start-At (iloc,SCM+FSA))) . a
let iloc be Element of NAT ; ::_thesis: for a being FinSeq-Location holds s . a = (s +* (Start-At (iloc,SCM+FSA))) . a
let a be FinSeq-Location ; ::_thesis: s . a = (s +* (Start-At (iloc,SCM+FSA))) . a
 a in the carrier of SCM+FSA ;
then  a in dom s by PARTFUN1:def_2;
then A1: ( dom (Start-At (iloc,SCM+FSA)) = {(IC )} & a in (dom s) \/ (dom (Start-At (iloc,SCM+FSA))) ) by FUNCOP_1:13, XBOOLE_0:def_3;
 a <> IC by SCMFSA_2:57;
then  not a in {(IC )} by TARSKI:def_1;
hence  s . a = (s +* (Start-At (iloc,SCM+FSA))) . a by A1, FUNCT_4:def_1; ::_thesis: verum
end;

begin

definition
let la be Int-Location;
let a be Integer;
:: original: .-->
redefine funcla .--> a ->  FinPartState of SCM+FSA;
coherence
 la .--> a is FinPartState of SCM+FSA
proof
 ( a is Element of INT & Values la = INT ) by INT_1:def_2, SCMFSA_2:11;
hence  la .--> a is FinPartState of SCM+FSA ; ::_thesis: verum
end;
end;

registration
cluster SCM+FSA  ->  IC-recognized ;
coherence
 SCM+FSA is IC-recognized
proof
 for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being b1 -autonomic FinPartState of SCM+FSA st DataPart p <> {} holds
IC in dom p
proof
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for p being q -autonomic FinPartState of SCM+FSA st DataPart p <> {} holds
IC in dom p
let p be q -autonomic FinPartState of SCM+FSA; ::_thesis: ( DataPart p <> {} implies IC in dom p )
assume  DataPart p <> {} ; ::_thesis: IC in dom p
then A1: dom (DataPart p) <> {} ;
assume  not IC in dom p ; ::_thesis: contradiction
then A2: dom p misses {(IC )} by ZFMISC_1:50;
 not p is q -autonomic
proof
set il = the Element of NAT \ (dom q);
set d2 = the Element of Int-Locations \ (dom p);
set d1 = the Element of dom (DataPart p);
A3: dom (DataPart p) c= Data-Locations by RELAT_1:58;
 not NAT c= dom q ;
then A4: NAT \ (dom q) <> {} by XBOOLE_1:37;
then reconsider il = the Element of NAT \ (dom q) as Element of NAT by XBOOLE_0:def_5;
 not Int-Locations c= dom p ;
then A5: Int-Locations \ (dom p) <> {} by XBOOLE_1:37;
then  the Element of Int-Locations \ (dom p) in Int-Locations by XBOOLE_0:def_5;
then reconsider d2 = the Element of Int-Locations \ (dom p) as Int-Location by AMI_2:def_16;
A6: the Element of dom (DataPart p) in dom (DataPart p) by A1;
 DataPart p c= p by MEMSTR_0:12;
then A7: dom (DataPart p) c= dom p by RELAT_1:11;
 dom (DataPart p) c= the carrier of SCM+FSA by RELAT_1:def_18;
then reconsider d1 = the Element of dom (DataPart p) as Element of SCM+FSA by A6;
percases ( d1 in Int-Locations or d1 in FinSeq-Locations ) by A6, A3, SCMFSA_2:100, XBOOLE_0:def_3;
suppose d1 in Int-Locations ; ::_thesis: not p is q -autonomic
then reconsider d1 = d1 as Int-Location by AMI_2:def_16;
set p1 = p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)));
set p2 = p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)));
set q1 = q +* (il .--> (d1 := d2));
set q2 = q +* (il .--> (d1 := d2));
consider s1 being State of SCM+FSA such that
A8: p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) c= s1 by PBOOLE:141;
consider S1 being Instruction-Sequence of SCM+FSA such that
A9: q +* (il .--> (d1 := d2)) c= S1 by PBOOLE:145;
 not d2 in dom p by A5, XBOOLE_0:def_5;
then A10: dom p misses {d2} by ZFMISC_1:50;
consider s2 being State of SCM+FSA such that
A11: p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) c= s2 by PBOOLE:141;
consider S2 being Instruction-Sequence of SCM+FSA such that
A12: q +* (il .--> (d1 := d2)) c= S2 by PBOOLE:145;
take P = S1; :: according to EXTPRO_1:def_10 ::_thesis: ex b1 being set st
( q c= P & q c= b1 & ex b2, b3 being set st
( p c= b2 & p c= b3 & not for b4 being Element of NAT holds (Comput (P,b2,b4)) | (dom p) = (Comput (b1,b3,b4)) | (dom p) ) )
take Q = S2; ::_thesis: ( q c= P & q c= Q & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (dom p) = (Comput (Q,b2,b3)) | (dom p) ) )
A13: dom (il .--> (d1 := d2)) = {il} by FUNCOP_1:13;
A14: not il in dom q by A4, XBOOLE_0:def_5;
dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 0)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def_1
.= (dom (d2 .--> 0)) \/ {(IC )} by FUNCOP_1:13
.= {d2} \/ {(IC )} by FUNCOP_1:13 ;
then (dom p) /\ (dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) = ((dom p) /\ {d2}) \/ ((dom p) /\ {(IC )}) by XBOOLE_1:23
.= ((dom p) /\ {d2}) \/ {} by A2, XBOOLE_0:def_7
.= {} by A10, XBOOLE_0:def_7 ;
then  dom p misses dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by XBOOLE_0:def_7;
then  p c= p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by FUNCT_4:32;
then A15: p c= s1 by A8, XBOOLE_1:1;
 dom q misses dom (il .--> (d1 := d2)) by A13, A14, ZFMISC_1:50;
then  q c= q +* (il .--> (d1 := d2)) by FUNCT_4:32;
hence  q c= P by A9, XBOOLE_1:1; ::_thesis: ( q c= Q & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (dom p) = (Comput (Q,b2,b3)) | (dom p) ) )
dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 1)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def_1
.= (dom (d2 .--> 1)) \/ {(IC )} by FUNCOP_1:13
.= {d2} \/ {(IC )} by FUNCOP_1:13 ;
then (dom p) /\ (dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) = ((dom p) /\ {d2}) \/ ((dom p) /\ {(IC )}) by XBOOLE_1:23
.= ((dom p) /\ {d2}) \/ {} by A2, XBOOLE_0:def_7
.= {} by A10, XBOOLE_0:def_7 ;
then  dom p misses dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by XBOOLE_0:def_7;
then  p c= p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by FUNCT_4:32;
then A16: p c= s2 by A11, XBOOLE_1:1;
 dom q misses dom (il .--> (d1 := d2)) by A13, A14, ZFMISC_1:50;
then  q c= q +* (il .--> (d1 := d2)) by FUNCT_4:32;
hence  q c= Q by A12, XBOOLE_1:1; ::_thesis: ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (dom p) = (Comput (Q,b2,b3)) | (dom p) )
take  s1 ; ::_thesis: ex b1 being set st
( p c= s1 & p c= b1 & not for b2 being Element of NAT holds (Comput (P,s1,b2)) | (dom p) = (Comput (Q,b1,b2)) | (dom p) )
take  s2 ; ::_thesis: ( p c= s1 & p c= s2 & not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (dom p) = (Comput (Q,s2,b1)) | (dom p) )
thus  p c= s1 by A15; ::_thesis: ( p c= s2 & not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (dom p) = (Comput (Q,s2,b1)) | (dom p) )
thus  p c= s2 by A16; ::_thesis: not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (dom p) = (Comput (Q,s2,b1)) | (dom p)
take  1 ; ::_thesis: not (Comput (P,s1,1)) | (dom p) = (Comput (Q,s2,1)) | (dom p)
A17: dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 1)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def_1;
A18: dom p c= the carrier of SCM+FSA by RELAT_1:def_18;
A19: dom (Comput (S2,s2,1)) = the carrier of SCM+FSA by PARTFUN1:def_2;
A20: dom ((Comput (S2,s2,1)) | (dom p)) = dom p by A18, A19, RELAT_1:62;
A21: dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 0)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def_1;
A22: dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) = (dom p) \/ (dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) by FUNCT_4:def_1;
A23: dom (Start-At (il,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A24: IC in dom (Start-At (il,SCM+FSA)) by TARSKI:def_1;
then A25: IC in dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by A21, XBOOLE_0:def_3;
then  IC in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) by A22, XBOOLE_0:def_3;
then A26: IC s1 = (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) . (IC ) by A8, GRFUNC_1:2
.= ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) . (IC ) by A25, FUNCT_4:13
.= (Start-At (il,SCM+FSA)) . (IC ) by A24, FUNCT_4:13
.= il by FUNCOP_1:72 ;
 d2 <> IC by SCMFSA_2:56;
then A27: not d2 in dom (Start-At (il,SCM+FSA)) by A23, TARSKI:def_1;
 dom (d2 .--> 0) = {d2} by FUNCOP_1:13;
then  d2 in dom (d2 .--> 0) by TARSKI:def_1;
then A28: d2 in dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by A21, XBOOLE_0:def_3;
then  d2 in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) by A22, XBOOLE_0:def_3;
then A29: s1 . d2 = (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) . d2 by A8, GRFUNC_1:2
.= ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) . d2 by A28, FUNCT_4:13
.= (d2 .--> 0) . d2 by A27, FUNCT_4:11
.= 0 by FUNCOP_1:72 ;
 dom (il .--> (d1 := d2)) = {il} by FUNCOP_1:13;
then A30: il in dom (il .--> (d1 := d2)) by TARSKI:def_1;
 dom (q +* (il .--> (d1 := d2))) = (dom q) \/ (dom (il .--> (d1 := d2))) by FUNCT_4:def_1;
then  il in dom (q +* (il .--> (d1 := d2))) by A30, XBOOLE_0:def_3;
then A31: S1 . il = (q +* (il .--> (d1 := d2))) . il by A9, GRFUNC_1:2
.= (il .--> (d1 := d2)) . il by A30, FUNCT_4:13
.= d1 := d2 by FUNCOP_1:72 ;
A32: dom p c= the carrier of SCM+FSA by RELAT_1:def_18;
A33: dom (Comput (S1,s1,1)) = the carrier of SCM+FSA by PARTFUN1:def_2;
A34: dom ((Comput (S1,s1,1)) | (dom p)) = dom p by A32, A33, RELAT_1:62;
A35: dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) = (dom p) \/ (dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) by FUNCT_4:def_1;
A36: dom (q +* (il .--> (d1 := d2))) = (dom q) \/ (dom (il .--> (d1 := d2))) by FUNCT_4:def_1;
A37: dom (Start-At (il,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A38: IC in dom (Start-At (il,SCM+FSA)) by TARSKI:def_1;
then A39: IC in dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by A17, XBOOLE_0:def_3;
then  IC in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) by A35, XBOOLE_0:def_3;
then A40: IC s2 = (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) . (IC ) by A11, GRFUNC_1:2
.= ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) . (IC ) by A39, FUNCT_4:13
.= (Start-At (il,SCM+FSA)) . (IC ) by A38, FUNCT_4:13
.= il by FUNCOP_1:72 ;
 d2 <> IC by SCMFSA_2:56;
then A41: not d2 in dom (Start-At (il,SCM+FSA)) by A37, TARSKI:def_1;
 dom (d2 .--> 1) = {d2} by FUNCOP_1:13;
then  d2 in dom (d2 .--> 1) by TARSKI:def_1;
then A42: d2 in dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by A17, XBOOLE_0:def_3;
then  d2 in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) by A35, XBOOLE_0:def_3;
then A43: s2 . d2 = (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) . d2 by A11, GRFUNC_1:2
.= ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) . d2 by A42, FUNCT_4:13
.= (d2 .--> 1) . d2 by A41, FUNCT_4:11
.= 1 by FUNCOP_1:72 ;
 dom (il .--> (d1 := d2)) = {il} by FUNCOP_1:13;
then A44: il in dom (il .--> (d1 := d2)) by TARSKI:def_1;
 il in dom (q +* (il .--> (d1 := d2))) by A36, A44, XBOOLE_0:def_3;
then A45: S2 . il = (q +* (il .--> (d1 := d2))) . il by A12, GRFUNC_1:2
.= (il .--> (d1 := d2)) . il by A44, FUNCT_4:13
.= d1 := d2 by FUNCOP_1:72 ;
A46: S2 /. (IC s2) = S2 . (IC s2) by PBOOLE:143;
A47: (Comput (S2,s2,(0 + 1))) . d1 = (Following (S2,(Comput (S2,s2,0)))) . d1 by EXTPRO_1:3
.= (Following (S2,s2)) . d1
.= 1 by A40, A45, A43, A46, SCMFSA_2:63 ;
A48: S1 /. (IC s1) = S1 . (IC s1) by PBOOLE:143;
(Comput (S1,s1,(0 + 1))) . d1 = (Following (S1,(Comput (S1,s1,0)))) . d1 by EXTPRO_1:3
.= (Following (S1,s1)) . d1
.= 0 by A26, A31, A29, A48, SCMFSA_2:63 ;
then  ((Comput (S1,s1,1)) | (dom p)) . d1 = 0 by A7, A34, A6, FUNCT_1:47;
hence  (Comput (P,s1,1)) | (dom p) <> (Comput (Q,s2,1)) | (dom p) by A47, A6, A7, A20, FUNCT_1:47; ::_thesis: verum
end;
suppose d1 in FinSeq-Locations ; ::_thesis: not p is q -autonomic
then reconsider d1 = d1 as FinSeq-Location by SCMFSA_2:def_5;
set p1 = p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)));
set p2 = p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)));
set q1 = q +* (il .--> (d1 :=<0,...,0> d2));
set q2 = q +* (il .--> (d1 :=<0,...,0> d2));
consider s1 being State of SCM+FSA such that
A49: p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) c= s1 by PBOOLE:141;
consider S1 being Instruction-Sequence of SCM+FSA such that
A50: q +* (il .--> (d1 :=<0,...,0> d2)) c= S1 by PBOOLE:145;
A51: dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 0)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def_1;
consider k being Element of NAT  such that
A52: k = abs (s1 . d2) and
A53: (Exec ((d1 :=<0,...,0> d2),s1)) . d1 = k |-> 0 by SCMFSA_2:75;
A54: dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) = (dom p) \/ (dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) by FUNCT_4:def_1;
A55: dom (q +* (il .--> (d1 :=<0,...,0> d2))) = (dom q) \/ (dom (il .--> (d1 :=<0,...,0> d2))) by FUNCT_4:def_1;
A56: dom (Start-At (il,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A57: IC in dom (Start-At (il,SCM+FSA)) by TARSKI:def_1;
then A58: IC in dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by A51, XBOOLE_0:def_3;
then  IC in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) by A54, XBOOLE_0:def_3;
then A59: IC s1 = (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) . (IC ) by A49, GRFUNC_1:2
.= ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) . (IC ) by A58, FUNCT_4:13
.= (Start-At (il,SCM+FSA)) . (IC ) by A57, FUNCT_4:13
.= il by FUNCOP_1:72 ;
consider s2 being State of SCM+FSA such that
A60: p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) c= s2 by PBOOLE:141;
consider S2 being Instruction-Sequence of SCM+FSA such that
A61: q +* (il .--> (d1 :=<0,...,0> d2)) c= S2 by PBOOLE:145;
 d2 <> IC by SCMFSA_2:56;
then A62: not d2 in dom (Start-At (il,SCM+FSA)) by A56, TARSKI:def_1;
 dom (d2 .--> 0) = {d2} by FUNCOP_1:13;
then  d2 in dom (d2 .--> 0) by TARSKI:def_1;
then A63: d2 in dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by A51, XBOOLE_0:def_3;
then  d2 in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) by A54, XBOOLE_0:def_3;
then s1 . d2 = (p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) . d2 by A49, GRFUNC_1:2
.= ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) . d2 by A63, FUNCT_4:13
.= (d2 .--> 0) . d2 by A62, FUNCT_4:11
.= 0 by FUNCOP_1:72 ;
then A64: k |-> 0 = 0 |-> 0 by A52, ABSVALUE:2
.= {} by FINSEQ_2:58 ;
 not d2 in dom p by A5, XBOOLE_0:def_5;
then A65: dom p misses {d2} by ZFMISC_1:50;
A66: dom (il .--> (d1 :=<0,...,0> d2)) = {il} by FUNCOP_1:13;
A67: il in dom (il .--> (d1 :=<0,...,0> d2)) by A66, ZFMISC_1:31;
then  il in dom (q +* (il .--> (d1 :=<0,...,0> d2))) by A55, XBOOLE_0:def_3;
then A68: S1 . il = (q +* (il .--> (d1 :=<0,...,0> d2))) . il by A50, GRFUNC_1:2
.= (il .--> (d1 :=<0,...,0> d2)) . il by A67, FUNCT_4:13
.= d1 :=<0,...,0> d2 by FUNCOP_1:72 ;
A69: dom p c= the carrier of SCM+FSA by RELAT_1:def_18;
A70: dom (Comput (S1,s1,1)) = the carrier of SCM+FSA by PARTFUN1:def_2;
A71: dom ((Comput (S1,s1,1)) | (dom p)) = dom p by A69, A70, RELAT_1:62;
consider k being Element of NAT  such that
A72: k = abs (s2 . d2) and
A73: (Exec ((d1 :=<0,...,0> d2),s2)) . d1 = k |-> 0 by SCMFSA_2:75;
A74: dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) = (dom p) \/ (dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) by FUNCT_4:def_1;
take P = S1; :: according to EXTPRO_1:def_10 ::_thesis: ex b1 being set st
( q c= P & q c= b1 & ex b2, b3 being set st
( p c= b2 & p c= b3 & not for b4 being Element of NAT holds (Comput (P,b2,b4)) | (dom p) = (Comput (b1,b3,b4)) | (dom p) ) )
take Q = S2; ::_thesis: ( q c= P & q c= Q & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (dom p) = (Comput (Q,b2,b3)) | (dom p) ) )
A75: dom (il .--> (d1 :=<0,...,0> d2)) = {il} by FUNCOP_1:13;
A76: not il in dom q by A4, XBOOLE_0:def_5;
A77: dom (q +* (il .--> (d1 :=<0,...,0> d2))) = (dom q) \/ (dom (il .--> (d1 :=<0,...,0> d2))) by FUNCT_4:def_1;
dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 0)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def_1
.= (dom (d2 .--> 0)) \/ {(IC )} by FUNCOP_1:13
.= {d2} \/ {(IC )} by FUNCOP_1:13 ;
then (dom p) /\ (dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA)))) = ((dom p) /\ {d2}) \/ ((dom p) /\ {(IC )}) by XBOOLE_1:23
.= ((dom p) /\ {d2}) \/ {} by A2, XBOOLE_0:def_7
.= {} by A65, XBOOLE_0:def_7 ;
then  dom p misses dom ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by XBOOLE_0:def_7;
then  p c= p +* ((d2 .--> 0) +* (Start-At (il,SCM+FSA))) by FUNCT_4:32;
then A78: p c= s1 by A49, XBOOLE_1:1;
 dom q misses dom (il .--> (d1 :=<0,...,0> d2)) by A75, A76, ZFMISC_1:50;
then  q c= q +* (il .--> (d1 :=<0,...,0> d2)) by FUNCT_4:32;
hence  q c= P by A50, XBOOLE_1:1; ::_thesis: ( q c= Q & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (dom p) = (Comput (Q,b2,b3)) | (dom p) ) )
dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 1)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def_1
.= (dom (d2 .--> 1)) \/ {(IC )} by FUNCOP_1:13
.= {d2} \/ {(IC )} by FUNCOP_1:13 ;
then (dom p) /\ (dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) = ((dom p) /\ {d2}) \/ ((dom p) /\ {(IC )}) by XBOOLE_1:23
.= ((dom p) /\ {d2}) \/ {} by A2, XBOOLE_0:def_7
.= {} by A65, XBOOLE_0:def_7 ;
then  dom p misses dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by XBOOLE_0:def_7;
then  p c= p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by FUNCT_4:32;
then A79: p c= s2 by A60, XBOOLE_1:1;
 dom q misses dom (il .--> (d1 :=<0,...,0> d2)) by A75, A76, ZFMISC_1:50;
then  q c= q +* (il .--> (d1 :=<0,...,0> d2)) by FUNCT_4:32;
hence  q c= Q by A61, XBOOLE_1:1; ::_thesis: ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (dom p) = (Comput (Q,b2,b3)) | (dom p) )
take  s1 ; ::_thesis: ex b1 being set st
( p c= s1 & p c= b1 & not for b2 being Element of NAT holds (Comput (P,s1,b2)) | (dom p) = (Comput (Q,b1,b2)) | (dom p) )
take  s2 ; ::_thesis: ( p c= s1 & p c= s2 & not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (dom p) = (Comput (Q,s2,b1)) | (dom p) )
thus  p c= s1 by A78; ::_thesis: ( p c= s2 & not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (dom p) = (Comput (Q,s2,b1)) | (dom p) )
thus  p c= s2 by A79; ::_thesis: not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (dom p) = (Comput (Q,s2,b1)) | (dom p)
take  1 ; ::_thesis: not (Comput (P,s1,1)) | (dom p) = (Comput (Q,s2,1)) | (dom p)
A80: dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) = (dom (d2 .--> 1)) \/ (dom (Start-At (il,SCM+FSA))) by FUNCT_4:def_1;
A81: dom (Start-At (il,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A82: IC in dom (Start-At (il,SCM+FSA)) by TARSKI:def_1;
then A83: IC in dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by A80, XBOOLE_0:def_3;
then  IC in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) by A74, XBOOLE_0:def_3;
then A84: IC s2 = (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) . (IC ) by A60, GRFUNC_1:2
.= ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) . (IC ) by A83, FUNCT_4:13
.= (Start-At (il,SCM+FSA)) . (IC ) by A82, FUNCT_4:13
.= il by FUNCOP_1:72 ;
 d2 <> IC by SCMFSA_2:56;
then A85: not d2 in dom (Start-At (il,SCM+FSA)) by A81, TARSKI:def_1;
 dom (d2 .--> 1) = {d2} by FUNCOP_1:13;
then  d2 in dom (d2 .--> 1) by TARSKI:def_1;
then A86: d2 in dom ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) by A80, XBOOLE_0:def_3;
then  d2 in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) by A74, XBOOLE_0:def_3;
then s2 . d2 = (p +* ((d2 .--> 1) +* (Start-At (il,SCM+FSA)))) . d2 by A60, GRFUNC_1:2
.= ((d2 .--> 1) +* (Start-At (il,SCM+FSA))) . d2 by A86, FUNCT_4:13
.= (d2 .--> 1) . d2 by A85, FUNCT_4:11
.= 1 by FUNCOP_1:72 ;
then A87: k |-> 0 = 1 |-> 0 by A72, ABSVALUE:def_1
.= <*0*> by FINSEQ_2:59 ;
 dom (il .--> (d1 :=<0,...,0> d2)) = {il} by FUNCOP_1:13;
then A88: il in dom (il .--> (d1 :=<0,...,0> d2)) by TARSKI:def_1;
then  il in dom (q +* (il .--> (d1 :=<0,...,0> d2))) by A77, XBOOLE_0:def_3;
then A89: S2 . il = (q +* (il .--> (d1 :=<0,...,0> d2))) . il by A61, GRFUNC_1:2
.= (il .--> (d1 :=<0,...,0> d2)) . il by A88, FUNCT_4:13
.= d1 :=<0,...,0> d2 by FUNCOP_1:72 ;
A90: (Comput (S2,s2,(0 + 1))) . d1 = (Following (S2,(Comput (S2,s2,0)))) . d1 by EXTPRO_1:3
.= (Following (S2,s2)) . d1
.= <*0*> by A84, A89, A73, A87, PBOOLE:143 ;
A91: dom p c= the carrier of SCM+FSA by RELAT_1:def_18;
A92: dom (Comput (S2,s2,1)) = the carrier of SCM+FSA by PARTFUN1:def_2;
A93: dom ((Comput (S2,s2,1)) | (dom p)) = dom p by A91, A92, RELAT_1:62;
(Comput (S1,s1,(0 + 1))) . d1 = (Following (S1,(Comput (S1,s1,0)))) . d1 by EXTPRO_1:3
.= (Following (S1,s1)) . d1
.= {} by A59, A68, A53, A64, PBOOLE:143 ;
then  ((Comput (S1,s1,1)) | (dom p)) . d1 = {} by A6, A7, A71, FUNCT_1:47;
hence  (Comput (P,s1,1)) | (dom p) <> (Comput (Q,s2,1)) | (dom p) by A90, A6, A7, A93, FUNCT_1:47; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
hence  SCM+FSA is IC-recognized by AMISTD_5:3; ::_thesis: verum
end;
end;

registration
cluster SCM+FSA  ->  CurIns-recognized ;
coherence
 SCM+FSA is CurIns-recognized
proof
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; :: according to AMISTD_5:def_4 ::_thesis: for b1 being set
for b2 being set holds
( not b1 c= b2 or for b3 being set holds
( not q c= b3 or for b4 being Element of NAT holds IC (Comput (b3,b2,b4)) in dom q ) )
let p be non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for b1 being set holds
( not p c= b1 or for b2 being set holds
( not q c= b2 or for b3 being Element of NAT holds IC (Comput (b2,b1,b3)) in dom q ) )
let s be State of SCM+FSA; ::_thesis: ( not p c= s or for b1 being set holds
( not q c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in dom q ) )
assume A1: p c= s ; ::_thesis: for b1 being set holds
( not q c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in dom q )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not q c= P or for b1 being Element of NAT holds IC (Comput (P,s,b1)) in dom q )
assume A2: q c= P ; ::_thesis: for b1 being Element of NAT holds IC (Comput (P,s,b1)) in dom q
let i be Element of NAT ; ::_thesis: IC (Comput (P,s,i)) in dom q
set Csi = Comput (P,s,i);
set loc = IC (Comput (P,s,i));
set loc1 = (IC (Comput (P,s,i))) + 1;
assume A3: not IC (Comput (P,s,i)) in dom q ; ::_thesis: contradiction
set I = (intloc 0) := (intloc 0);
set q1 = q +* ((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0)));
set q2 = q +* ((IC (Comput (P,s,i))) .--> (halt SCM+FSA));
reconsider P1 = P +* ((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0))) as Instruction-Sequence of SCM+FSA ;
reconsider P2 = P +* ((IC (Comput (P,s,i))) .--> (halt SCM+FSA)) as Instruction-Sequence of SCM+FSA ;
A4: dom ((IC (Comput (P,s,i))) .--> (halt SCM+FSA)) = {(IC (Comput (P,s,i)))} by FUNCOP_1:13;
then A5: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> (halt SCM+FSA)) by TARSKI:def_1;
A6: dom ((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0))) = {(IC (Comput (P,s,i)))} by FUNCOP_1:13;
then A7: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0))) by TARSKI:def_1;
A8: dom q misses dom ((IC (Comput (P,s,i))) .--> (halt SCM+FSA)) by A3, A4, ZFMISC_1:50;
A9: dom q misses dom ((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0))) by A3, A6, ZFMISC_1:50;
A10: q +* ((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0))) c= P1 by A2, FUNCT_4:123;
A11: q +* ((IC (Comput (P,s,i))) .--> (halt SCM+FSA)) c= P2 by A2, FUNCT_4:123;
set Cs2i = Comput (P2,s,i);
set Cs1i = Comput (P1,s,i);
 not p is q -autonomic
proof
 ((IC (Comput (P,s,i))) .--> (halt SCM+FSA)) . (IC (Comput (P,s,i))) = halt SCM+FSA by FUNCOP_1:72;
then A12: P2 . (IC (Comput (P,s,i))) = halt SCM+FSA by A5, FUNCT_4:13;
A13: ((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0))) . (IC (Comput (P,s,i))) = (intloc 0) := (intloc 0) by FUNCOP_1:72;
take  P1 ; :: according to EXTPRO_1:def_10 ::_thesis: ex b1 being set st
( q c= P1 & q c= b1 & ex b2, b3 being set st
( p c= b2 & p c= b3 & not for b4 being Element of NAT holds (Comput (P1,b2,b4)) | (dom p) = (Comput (b1,b3,b4)) | (dom p) ) )
take  P2 ; ::_thesis: ( q c= P1 & q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) ) )
 q c= q +* ((IC (Comput (P,s,i))) .--> ((intloc 0) := (intloc 0))) by A9, FUNCT_4:32;
hence A14: q c= P1 by A10, XBOOLE_1:1; ::_thesis: ( q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) ) )
 q c= q +* ((IC (Comput (P,s,i))) .--> (halt SCM+FSA)) by A8, FUNCT_4:32;
hence A15: q c= P2 by A11, XBOOLE_1:1; ::_thesis: ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) )
take  s ; ::_thesis: ex b1 being set st
( p c= s & p c= b1 & not for b2 being Element of NAT holds (Comput (P1,s,b2)) | (dom p) = (Comput (P2,b1,b2)) | (dom p) )
take  s ; ::_thesis: ( p c= s & p c= s & not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom p) )
thus  p c= s by A1; ::_thesis: ( p c= s & not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom p) )
A16: (Comput (P1,s,i)) | (dom p) = (Comput (P,s,i)) | (dom p) by A14, A2, A1, EXTPRO_1:def_10;
thus  p c= s by A1; ::_thesis: not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom p)
A17: (Comput (P1,s,i)) | (dom p) = (Comput (P2,s,i)) | (dom p) by A14, A15, A1, EXTPRO_1:def_10;
take k = i + 1; ::_thesis: not (Comput (P1,s,k)) | (dom p) = (Comput (P2,s,k)) | (dom p)
set Cs1k = Comput (P1,s,k);
A18: IC in dom p by AMISTD_5:6;
 IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by A18, FUNCT_1:49;
then  IC (Comput (P1,s,i)) = IC (Comput (P,s,i)) by A16, A18, FUNCT_1:49;
then A19: CurInstr (P1,(Comput (P1,s,i))) = P1 . (IC (Comput (P,s,i))) by PBOOLE:143
.= (intloc 0) := (intloc 0) by A13, A7, FUNCT_4:13 ;
A20: Comput (P1,s,k) = Following (P1,(Comput (P1,s,i))) by EXTPRO_1:3
.= Exec (((intloc 0) := (intloc 0)),(Comput (P1,s,i))) by A19 ;
A21: IC (Exec (((intloc 0) := (intloc 0)),(Comput (P1,s,i)))) = succ (IC (Comput (P1,s,i))) by SCMFSA_2:63;
A22: IC in dom p by AMISTD_5:6;
A23: IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by A22, FUNCT_1:49;
then A24: IC (Comput (P1,s,k)) = succ (IC (Comput (P,s,i))) by A20, A21, A16, A22, FUNCT_1:49
.= (IC (Comput (P,s,i))) + 1 by NAT_1:38 ;
set Cs2k = Comput (P2,s,k);
A25: Comput (P2,s,k) = Following (P2,(Comput (P2,s,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s,i)))),(Comput (P2,s,i))) ;
A26: P2 /. (IC (Comput (P2,s,i))) = P2 . (IC (Comput (P2,s,i))) by PBOOLE:143;
 IC (Comput (P2,s,i)) = IC (Comput (P,s,i)) by A16, A23, A17, A22, FUNCT_1:49;
then A27: IC (Comput (P2,s,k)) = IC (Comput (P,s,i)) by A25, A12, A26, EXTPRO_1:def_3;
 ( IC ((Comput (P1,s,k)) | (dom p)) = IC (Comput (P1,s,k)) & IC ((Comput (P2,s,k)) | (dom p)) = IC (Comput (P2,s,k)) ) by A22, FUNCT_1:49;
hence  not (Comput (P1,s,k)) | (dom p) = (Comput (P2,s,k)) | (dom p) by A24, A27; ::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;
end;

theorem :: SCMFSA_3:5
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
proof
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
let p be non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
let s1, s2 be State of SCM+FSA; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
let i be Element of NAT ; ::_thesis: for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
let da, db be Int-Location; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = da := db & da in dom p implies (Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db )
set I = CurInstr (P1,(Comput (P1,s1,i)));
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
A4: ( da in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . da = (Comput (P1,s1,(i + 1))) . da & ((Comput (P2,s2,(i + 1))) | (dom p)) . da = (Comput (P2,s2,(i + 1))) . da ) ) by FUNCT_1:49;
assume that
A5: CurInstr (P1,(Comput (P1,s1,i))) = da := db and
A6: ( da in dom p & (Comput (P1,s1,i)) . db <> (Comput (P2,s2,i)) . db ) ; ::_thesis: contradiction
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then A7: (Comput (P1,s1,(i + 1))) . da = (Comput (P1,s1,i)) . db by A5, SCMFSA_2:63;
 CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
then  (Comput (P2,s2,(i + 1))) . da = (Comput (P2,s2,i)) . db by A3, A5, SCMFSA_2:63;
hence  contradiction by A4, A6, A7, A2, A1, EXTPRO_1:def_10; ::_thesis: verum
end;

theorem :: SCMFSA_3:6
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
proof
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
let p be non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
let s1, s2 be State of SCM+FSA; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
let i be Element of NAT ; ::_thesis: for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
let da, db be Int-Location; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) & da in dom p implies ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) )
set I = CurInstr (P1,(Comput (P1,s1,i)));
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
A4: ( da in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . da = (Comput (P1,s1,(i + 1))) . da & ((Comput (P2,s2,(i + 1))) | (dom p)) . da = (Comput (P2,s2,(i + 1))) . da ) ) by FUNCT_1:49;
assume that
A5: CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) and
A6: ( da in dom p & ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) <> ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) ) ; ::_thesis: contradiction
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then A7: (Comput (P1,s1,(i + 1))) . da = ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) by A5, SCMFSA_2:64;
 CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
then  (Comput (P2,s2,(i + 1))) . da = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) by A3, A5, SCMFSA_2:64;
hence  contradiction by A1, A4, A6, A7, A2, EXTPRO_1:def_10; ::_thesis: verum
end;

theorem :: SCMFSA_3:7
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
proof
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
let p be non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
let s1, s2 be State of SCM+FSA; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
let i be Element of NAT ; ::_thesis: for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
let da, db be Int-Location; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) & da in dom p implies ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) )
set I = CurInstr (P1,(Comput (P1,s1,i)));
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
A4: ( da in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . da = (Comput (P1,s1,(i + 1))) . da & ((Comput (P2,s2,(i + 1))) | (dom p)) . da = (Comput (P2,s2,(i + 1))) . da ) ) by FUNCT_1:49;
assume that
A5: CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) and
A6: ( da in dom p & ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) <> ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) ) ; ::_thesis: contradiction
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then A7: (Comput (P1,s1,(i + 1))) . da = ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) by A5, SCMFSA_2:65;
 CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
then  (Comput (P2,s2,(i + 1))) . da = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) by A3, A5, SCMFSA_2:65;
hence  contradiction by A1, A4, A6, A7, A2, EXTPRO_1:def_10; ::_thesis: verum
end;

theorem :: SCMFSA_3:8
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
proof
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
let p be non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
let s1, s2 be State of SCM+FSA; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
let i be Element of NAT ; ::_thesis: for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
let da, db be Int-Location; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) & da in dom p implies ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) )
set I = CurInstr (P1,(Comput (P1,s1,i)));
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
A4: ( da in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . da = (Comput (P1,s1,(i + 1))) . da & ((Comput (P2,s2,(i + 1))) | (dom p)) . da = (Comput (P2,s2,(i + 1))) . da ) ) by FUNCT_1:49;
assume that
A5: CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) and
A6: ( da in dom p & ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) <> ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) ) ; ::_thesis: contradiction
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then A7: (Comput (P1,s1,(i + 1))) . da = ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) by A5, SCMFSA_2:66;
 CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
then  (Comput (P2,s2,(i + 1))) . da = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) by A3, A5, SCMFSA_2:66;
hence  contradiction by A1, A4, A6, A7, A2, EXTPRO_1:def_10; ::_thesis: verum
end;

theorem :: SCMFSA_3:9
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
proof
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
let p be non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
let s1, s2 be State of SCM+FSA; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
let i be Element of NAT ; ::_thesis: for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
let da, db be Int-Location; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & da in dom p & da <> db implies ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) )
set I = CurInstr (P1,(Comput (P1,s1,i)));
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
A4: ( da in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . da = (Comput (P1,s1,(i + 1))) . da & ((Comput (P2,s2,(i + 1))) | (dom p)) . da = (Comput (P2,s2,(i + 1))) . da ) ) by FUNCT_1:49;
assume that
A5: CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) and
A6: da in dom p and
A7: da <> db and
A8: ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) <> ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) ; ::_thesis: contradiction
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then A9: (Comput (P1,s1,(i + 1))) . da = ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) by A5, A7, SCMFSA_2:67;
 CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
then  (Comput (P2,s2,(i + 1))) . da = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) by A3, A5, A7, SCMFSA_2:67;
hence  contradiction by A1, A4, A8, A9, A2, A6, EXTPRO_1:def_10; ::_thesis: verum
end;

theorem :: SCMFSA_3:10
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
proof
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
let p be non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
let s1, s2 be State of SCM+FSA; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
let i be Element of NAT ; ::_thesis: for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
let da, db be Int-Location; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & db in dom p implies ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) )
set I = CurInstr (P1,(Comput (P1,s1,i)));
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A4: CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) and
A5: db in dom p and
A6: ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) <> ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) ; ::_thesis: contradiction
A7: ( ((Comput (P1,s1,(i + 1))) | (dom p)) . db = (Comput (P1,s1,(i + 1))) . db & ((Comput (P2,s2,(i + 1))) | (dom p)) . db = (Comput (P2,s2,(i + 1))) . db ) by A5, FUNCT_1:49;
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then A8: (Comput (P1,s1,(i + 1))) . db = ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) by A4, SCMFSA_2:67;
 CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
then  (Comput (P2,s2,(i + 1))) . db = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A3, A4, SCMFSA_2:67;
hence  contradiction by A1, A6, A7, A8, A2, EXTPRO_1:def_10; ::_thesis: verum
end;

theorem :: SCMFSA_3:11
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
proof
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
let p be non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
let s1, s2 be State of SCM+FSA; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 ) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 ) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
let i be Element of NAT ; ::_thesis: for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
let da be Int-Location; ::_thesis: for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
let loc be Element of NAT ; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) implies ( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 ) )
set I = CurInstr (P1,(Comput (P1,s1,i)));
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A4: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
 IC in dom p by AMISTD_5:6;
then A5: ( ((Comput (P1,s1,(i + 1))) | (dom p)) . (IC ) = (Comput (P1,s1,(i + 1))) . (IC ) & ((Comput (P2,s2,(i + 1))) | (dom p)) . (IC ) = (Comput (P2,s2,(i + 1))) . (IC ) ) by FUNCT_1:49;
assume that
A6: CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc and
A7: loc <> succ (IC (Comput (P1,s1,i))) ; ::_thesis: ( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
A8: CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
A9: now__::_thesis:_(_(Comput_(P2,s2,i))_._da_=_0_implies_not_(Comput_(P1,s1,i))_._da_<>_0_)
assume  ( (Comput (P2,s2,i)) . da = 0 & (Comput (P1,s1,i)) . da <> 0 ) ; ::_thesis: contradiction
then  ( (Comput (P2,s2,(i + 1))) . (IC ) = loc & (Comput (P1,s1,(i + 1))) . (IC ) = succ (IC (Comput (P1,s1,i))) ) by A8, A3, A4, A6, SCMFSA_2:70;
hence  contradiction by A1, A5, A7, A2, EXTPRO_1:def_10; ::_thesis: verum
end;
A10: (Comput (P1,s1,(i + 1))) | (dom p) = (Comput (P2,s2,(i + 1))) | (dom p) by A1, A2, EXTPRO_1:def_10;
now__::_thesis:_(_(Comput_(P1,s1,i))_._da_=_0_implies_not_(Comput_(P2,s2,i))_._da_<>_0_)
assume  ( (Comput (P1,s1,i)) . da = 0 & (Comput (P2,s2,i)) . da <> 0 ) ; ::_thesis: contradiction
then  ( (Comput (P1,s1,(i + 1))) . (IC ) = loc & (Comput (P2,s2,(i + 1))) . (IC ) = succ (IC (Comput (P2,s2,i))) ) by A8, A3, A4, A6, SCMFSA_2:70;
hence  contradiction by A1, A5, A10, A7, A2, AMISTD_5:7; ::_thesis: verum
end;
hence  ( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 ) by A9; ::_thesis: verum
end;

theorem :: SCMFSA_3:12
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
proof
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
let p be non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
let s1, s2 be State of SCM+FSA; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 ) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 ) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
let i be Element of NAT ; ::_thesis: for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
let da be Int-Location; ::_thesis: for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
let loc be Element of NAT ; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) implies ( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 ) )
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: (Comput (P1,s1,(i + 1))) | (dom p) = (Comput (P2,s2,(i + 1))) | (dom p) by A1, A2, EXTPRO_1:def_10;
set Cs2i = Comput (P2,s2,i);
set Cs1i = Comput (P1,s1,i);
set I = CurInstr (P1,(Comput (P1,s1,i)));
A4: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
 IC in dom p by AMISTD_5:6;
then A5: ( ((Comput (P1,s1,(i + 1))) | (dom p)) . (IC ) = (Comput (P1,s1,(i + 1))) . (IC ) & ((Comput (P2,s2,(i + 1))) | (dom p)) . (IC ) = (Comput (P2,s2,(i + 1))) . (IC ) ) by FUNCT_1:49;
A6: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A7: CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc and
A8: loc <> succ (IC (Comput (P1,s1,i))) ; ::_thesis: ( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
A9: CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
A10: now__::_thesis:_(_(Comput_(P2,s2,i))_._da_>_0_implies_not_(Comput_(P1,s1,i))_._da_<=_0_)
assume that
A11: (Comput (P2,s2,i)) . da > 0 and
A12: (Comput (P1,s1,i)) . da <= 0 ; ::_thesis: contradiction
 (Comput (P2,s2,(i + 1))) . (IC ) = loc by A9, A6, A7, A11, SCMFSA_2:71;
hence  contradiction by A4, A5, A3, A7, A8, A12, SCMFSA_2:71; ::_thesis: verum
end;
A13: IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) by A1, A2, AMISTD_5:7;
now__::_thesis:_(_(Comput_(P1,s1,i))_._da_>_0_implies_not_(Comput_(P2,s2,i))_._da_<=_0_)
assume that
A14: (Comput (P1,s1,i)) . da > 0 and
A15: (Comput (P2,s2,i)) . da <= 0 ; ::_thesis: contradiction
 (Comput (P1,s1,(i + 1))) . (IC ) = loc by A4, A7, A14, SCMFSA_2:71;
hence  contradiction by A13, A9, A6, A5, A3, A7, A8, A15, SCMFSA_2:71; ::_thesis: verum
end;
hence  ( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 ) by A10; ::_thesis: verum
end;

theorem :: SCMFSA_3:13
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) & da in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2
proof
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) & da in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2
let p be non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) & da in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2
let s1, s2 be State of SCM+FSA; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) & da in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2 )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) & da in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2
let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) & da in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2 )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) & da in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2
let i be Element of NAT ; ::_thesis: for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) & da in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2
let da, db be Int-Location; ::_thesis: for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) & da in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2
let f be FinSeq-Location ; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) & da in dom p implies for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2 )
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: (Comput (P1,s1,(i + 1))) | (dom p) = (Comput (P2,s2,(i + 1))) | (dom p) by A1, A2, EXTPRO_1:def_10;
set Cs2i = Comput (P2,s2,i);
set Cs1i = Comput (P1,s1,i);
set I = CurInstr (P1,(Comput (P1,s1,i)));
A4: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A5: ( da in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . da = (Comput (P1,s1,(i + 1))) . da & ((Comput (P2,s2,(i + 1))) | (dom p)) . da = (Comput (P2,s2,(i + 1))) . da ) ) by FUNCT_1:49;
A6: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A7: CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) and
A8: da in dom p ; ::_thesis: for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2
A9: ( ex k1 being Element of NAT st
( k1 = abs ((Comput (P1,s1,i)) . db) & (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . da = ((Comput (P1,s1,i)) . f) /. k1 ) & ex k2 being Element of NAT st
( k2 = abs ((Comput (P2,s2,i)) . db) & (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i)))) . da = ((Comput (P2,s2,i)) . f) /. k2 ) ) by A7, SCMFSA_2:72;
let i1, i2 be Element of NAT ; ::_thesis: ( i1 = abs ((Comput (P1,s1,i)) . db) & i2 = abs ((Comput (P2,s2,i)) . db) implies ((Comput (P1,s1,i)) . f) /. i1 = ((Comput (P2,s2,i)) . f) /. i2 )
assume  ( i1 = abs ((Comput (P1,s1,i)) . db) & i2 = abs ((Comput (P2,s2,i)) . db) & ((Comput (P1,s1,i)) . f) /. i1 <> ((Comput (P2,s2,i)) . f) /. i2 ) ; ::_thesis: contradiction
hence  contradiction by A1, A4, A6, A5, A3, A9, A8, A2, AMISTD_5:7; ::_thesis: verum
end;

theorem :: SCMFSA_3:14
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da))
proof
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da))
let p be non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da))
let s1, s2 be State of SCM+FSA; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da)) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da))
let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da)) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da))
let i be Element of NAT ; ::_thesis: for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da))
let da, db be Int-Location; ::_thesis: for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da))
let f be FinSeq-Location ; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da & f in dom p implies for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da)) )
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: (Comput (P1,s1,(i + 1))) | (dom p) = (Comput (P2,s2,(i + 1))) | (dom p) by A1, A2, EXTPRO_1:def_10;
set Cs2i = Comput (P2,s2,i);
set Cs1i = Comput (P1,s1,i);
set I = CurInstr (P1,(Comput (P1,s1,i)));
A4: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A5: ( f in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . f = (Comput (P1,s1,(i + 1))) . f & ((Comput (P2,s2,(i + 1))) | (dom p)) . f = (Comput (P2,s2,(i + 1))) . f ) ) by FUNCT_1:49;
A6: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A7: CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da and
A8: f in dom p ; ::_thesis: for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) & k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da))
A9: ( ex k1 being Element of NAT st
( k1 = abs ((Comput (P1,s1,i)) . db) & (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . f = ((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) ) & ex k2 being Element of NAT st
( k2 = abs ((Comput (P2,s2,i)) . db) & (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i)))) . f = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da)) ) ) by A7, SCMFSA_2:73;
let i1, i2 be Element of NAT ; ::_thesis: ( i1 = abs ((Comput (P1,s1,i)) . db) & i2 = abs ((Comput (P2,s2,i)) . db) implies ((Comput (P1,s1,i)) . f) +* (i1,((Comput (P1,s1,i)) . da)) = ((Comput (P2,s2,i)) . f) +* (i2,((Comput (P2,s2,i)) . da)) )
assume  ( i1 = abs ((Comput (P1,s1,i)) . db) & i2 = abs ((Comput (P2,s2,i)) . db) & ((Comput (P1,s1,i)) . f) +* (i1,((Comput (P1,s1,i)) . da)) <> ((Comput (P2,s2,i)) . f) +* (i2,((Comput (P2,s2,i)) . da)) ) ; ::_thesis: contradiction
hence  contradiction by A1, A4, A6, A5, A3, A9, A8, A2, AMISTD_5:7; ::_thesis: verum
end;

theorem :: SCMFSA_3:15
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da :=len f & da in dom p holds
len ((Comput (P1,s1,i)) . f) = len ((Comput (P2,s2,i)) . f)
proof
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da :=len f & da in dom p holds
len ((Comput (P1,s1,i)) . f) = len ((Comput (P2,s2,i)) . f)
let p be non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da :=len f & da in dom p holds
len ((Comput (P1,s1,i)) . f) = len ((Comput (P2,s2,i)) . f)
let s1, s2 be State of SCM+FSA; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da :=len f & da in dom p holds
len ((Comput (P1,s1,i)) . f) = len ((Comput (P2,s2,i)) . f) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da :=len f & da in dom p holds
len ((Comput (P1,s1,i)) . f) = len ((Comput (P2,s2,i)) . f)
let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da :=len f & da in dom p holds
len ((Comput (P1,s1,i)) . f) = len ((Comput (P2,s2,i)) . f) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da :=len f & da in dom p holds
len ((Comput (P1,s1,i)) . f) = len ((Comput (P2,s2,i)) . f)
let i be Element of NAT ; ::_thesis: for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da :=len f & da in dom p holds
len ((Comput (P1,s1,i)) . f) = len ((Comput (P2,s2,i)) . f)
let da be Int-Location; ::_thesis: for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da :=len f & da in dom p holds
len ((Comput (P1,s1,i)) . f) = len ((Comput (P2,s2,i)) . f)
let f be FinSeq-Location ; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = da :=len f & da in dom p implies len ((Comput (P1,s1,i)) . f) = len ((Comput (P2,s2,i)) . f) )
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: (Comput (P1,s1,(i + 1))) | (dom p) = (Comput (P2,s2,(i + 1))) | (dom p) by A1, A2, EXTPRO_1:def_10;
set Cs2i = Comput (P2,s2,i);
set Cs1i = Comput (P1,s1,i);
set I = CurInstr (P1,(Comput (P1,s1,i)));
A4: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A5: ( da in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . da = (Comput (P1,s1,(i + 1))) . da & ((Comput (P2,s2,(i + 1))) | (dom p)) . da = (Comput (P2,s2,(i + 1))) . da ) ) by FUNCT_1:49;
A6: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A7: CurInstr (P1,(Comput (P1,s1,i))) = da :=len f and
A8: ( da in dom p & len ((Comput (P1,s1,i)) . f) <> len ((Comput (P2,s2,i)) . f) ) ; ::_thesis: contradiction
 ( (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . da = len ((Comput (P1,s1,i)) . f) & (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i)))) . da = len ((Comput (P2,s2,i)) . f) ) by A7, SCMFSA_2:74;
hence  contradiction by A1, A4, A6, A5, A3, A8, A2, AMISTD_5:7; ::_thesis: verum
end;

theorem :: SCMFSA_3:16
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . da) & k2 = abs ((Comput (P2,s2,i)) . da) holds
k1 |-> 0 = k2 |-> 0
proof
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . da) & k2 = abs ((Comput (P2,s2,i)) . da) holds
k1 |-> 0 = k2 |-> 0
let p be non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . da) & k2 = abs ((Comput (P2,s2,i)) . da) holds
k1 |-> 0 = k2 |-> 0
let s1, s2 be State of SCM+FSA; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . da) & k2 = abs ((Comput (P2,s2,i)) . da) holds
k1 |-> 0 = k2 |-> 0 )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . da) & k2 = abs ((Comput (P2,s2,i)) . da) holds
k1 |-> 0 = k2 |-> 0
let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . da) & k2 = abs ((Comput (P2,s2,i)) . da) holds
k1 |-> 0 = k2 |-> 0 )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . da) & k2 = abs ((Comput (P2,s2,i)) . da) holds
k1 |-> 0 = k2 |-> 0
let i be Element of NAT ; ::_thesis: for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . da) & k2 = abs ((Comput (P2,s2,i)) . da) holds
k1 |-> 0 = k2 |-> 0
let da be Int-Location; ::_thesis: for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da & f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . da) & k2 = abs ((Comput (P2,s2,i)) . da) holds
k1 |-> 0 = k2 |-> 0
let f be FinSeq-Location ; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da & f in dom p implies for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . da) & k2 = abs ((Comput (P2,s2,i)) . da) holds
k1 |-> 0 = k2 |-> 0 )
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: (Comput (P1,s1,(i + 1))) | (dom p) = (Comput (P2,s2,(i + 1))) | (dom p) by A1, A2, EXTPRO_1:def_10;
set Cs2i = Comput (P2,s2,i);
set Cs1i = Comput (P1,s1,i);
set I = CurInstr (P1,(Comput (P1,s1,i)));
A4: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A5: ( f in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . f = (Comput (P1,s1,(i + 1))) . f & ((Comput (P2,s2,(i + 1))) | (dom p)) . f = (Comput (P2,s2,(i + 1))) . f ) ) by FUNCT_1:49;
A6: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A7: CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da and
A8: f in dom p ; ::_thesis: for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . da) & k2 = abs ((Comput (P2,s2,i)) . da) holds
k1 |-> 0 = k2 |-> 0
A9: ( ex k1 being Element of NAT st
( k1 = abs ((Comput (P1,s1,i)) . da) & (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . f = k1 |-> 0 ) & ex k2 being Element of NAT st
( k2 = abs ((Comput (P2,s2,i)) . da) & (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i)))) . f = k2 |-> 0 ) ) by A7, SCMFSA_2:75;
let i1, i2 be Element of NAT ; ::_thesis: ( i1 = abs ((Comput (P1,s1,i)) . da) & i2 = abs ((Comput (P2,s2,i)) . da) implies i1 |-> 0 = i2 |-> 0 )
assume  ( i1 = abs ((Comput (P1,s1,i)) . da) & i2 = abs ((Comput (P2,s2,i)) . da) & i1 |-> 0 <> i2 |-> 0 ) ; ::_thesis: contradiction
hence  contradiction by A1, A4, A6, A5, A3, A9, A8, A2, AMISTD_5:7; ::_thesis: verum
end;