let T be InsType of SCM+FSA ; AMISTD_2:def 11 AddressParts T is product-like
per cases
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 or T = 9 or T = 10 or T = 11 or T = 12 )
by Lm4;
suppose A2:
T = 1
;
AddressParts T is product-like take
product" (AddressParts T)
;
CARD_3:def 14 AddressParts T = product (product" (AddressParts T))thus
AddressParts T c= product (product" (AddressParts T))
by CARD_3:94;
XBOOLE_0:def 10 product (product" (AddressParts T)) c= AddressParts Tlet x be
set ;
TARSKI:def 3 ( not x in product (product" (AddressParts T)) or x in AddressParts T )assume
x in product (product" (AddressParts T))
;
x in AddressParts Tthen consider f being
Function such that A3:
x = f
and A4:
dom f = dom (product" (AddressParts T))
and A5:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A6:
dom (product" (AddressParts T)) = {1,2}
by A2, Th31;
then A7:
1
in dom (product" (AddressParts T))
by TARSKI:def 2;
then
f . 1
in (product" (AddressParts T)) . 1
by A5;
then
f . 1
in pi (AddressParts T),1
by A7, CARD_3:def 13;
then consider g being
Function such that A8:
g in AddressParts T
and A9:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
SCM+FSA such that A10:
g = AddressPart I
and A11:
InsCode I = T
by A8;
consider d1,
b being
Int-Location such that A12:
I = d1 := b
by A2, A11, SCMFSA_2:54;
A13:
2
in dom (product" (AddressParts T))
by A6, TARSKI:def 2;
then
f . 2
in (product" (AddressParts T)) . 2
by A5;
then
f . 2
in pi (AddressParts T),2
by A13, CARD_3:def 13;
then consider h being
Function such that A14:
h in AddressParts T
and A15:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
SCM+FSA such that A16:
h = AddressPart J
and A17:
InsCode J = T
by A14;
consider a,
d2 being
Int-Location such that A18:
J = a := d2
by A2, A17, SCMFSA_2:54;
A19:
h = <*a,d2*>
by A16, A18, Th18;
A20:
g = <*d1,b*>
by A10, A12, Th18;
A21:
for
k being
set st
k in {1,2} holds
<*d1,d2*> . k = f . k
dom <*d1,d2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then A25:
<*d1,d2*> = f
by A4, A6, A21, FUNCT_1:9;
A26:
InsCode (d1 := d2) = 1
by SCMFSA_2:42;
AddressPart (d1 := d2) = <*d1,d2*>
by Th18;
hence
x in AddressParts T
by A2, A3, A25, A26;
verum end; suppose A27:
T = 2
;
AddressParts T is product-like take
product" (AddressParts T)
;
CARD_3:def 14 AddressParts T = product (product" (AddressParts T))thus
AddressParts T c= product (product" (AddressParts T))
by CARD_3:94;
XBOOLE_0:def 10 product (product" (AddressParts T)) c= AddressParts Tlet x be
set ;
TARSKI:def 3 ( not x in product (product" (AddressParts T)) or x in AddressParts T )assume
x in product (product" (AddressParts T))
;
x in AddressParts Tthen consider f being
Function such that A28:
x = f
and A29:
dom f = dom (product" (AddressParts T))
and A30:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A31:
dom (product" (AddressParts T)) = {1,2}
by A27, Th32;
then A32:
1
in dom (product" (AddressParts T))
by TARSKI:def 2;
then
f . 1
in (product" (AddressParts T)) . 1
by A30;
then
f . 1
in pi (AddressParts T),1
by A32, CARD_3:def 13;
then consider g being
Function such that A33:
g in AddressParts T
and A34:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
SCM+FSA such that A35:
g = AddressPart I
and A36:
InsCode I = T
by A33;
consider d1,
b being
Int-Location such that A37:
I = AddTo d1,
b
by A27, A36, SCMFSA_2:55;
A38:
2
in dom (product" (AddressParts T))
by A31, TARSKI:def 2;
then
f . 2
in (product" (AddressParts T)) . 2
by A30;
then
f . 2
in pi (AddressParts T),2
by A38, CARD_3:def 13;
then consider h being
Function such that A39:
h in AddressParts T
and A40:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
SCM+FSA such that A41:
h = AddressPart J
and A42:
InsCode J = T
by A39;
consider a,
d2 being
Int-Location such that A43:
J = AddTo a,
d2
by A27, A42, SCMFSA_2:55;
A44:
h = <*a,d2*>
by A41, A43, Th19;
A45:
g = <*d1,b*>
by A35, A37, Th19;
A46:
for
k being
set st
k in {1,2} holds
<*d1,d2*> . k = f . k
dom <*d1,d2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then A50:
<*d1,d2*> = f
by A29, A31, A46, FUNCT_1:9;
A51:
InsCode (AddTo d1,d2) = 2
by SCMFSA_2:43;
AddressPart (AddTo d1,d2) = <*d1,d2*>
by Th19;
hence
x in AddressParts T
by A27, A28, A50, A51;
verum end; suppose A52:
T = 3
;
AddressParts T is product-like take
product" (AddressParts T)
;
CARD_3:def 14 AddressParts T = product (product" (AddressParts T))thus
AddressParts T c= product (product" (AddressParts T))
by CARD_3:94;
XBOOLE_0:def 10 product (product" (AddressParts T)) c= AddressParts Tlet x be
set ;
TARSKI:def 3 ( not x in product (product" (AddressParts T)) or x in AddressParts T )assume
x in product (product" (AddressParts T))
;
x in AddressParts Tthen consider f being
Function such that A53:
x = f
and A54:
dom f = dom (product" (AddressParts T))
and A55:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A56:
dom (product" (AddressParts T)) = {1,2}
by A52, Th33;
then A57:
1
in dom (product" (AddressParts T))
by TARSKI:def 2;
then
f . 1
in (product" (AddressParts T)) . 1
by A55;
then
f . 1
in pi (AddressParts T),1
by A57, CARD_3:def 13;
then consider g being
Function such that A58:
g in AddressParts T
and A59:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
SCM+FSA such that A60:
g = AddressPart I
and A61:
InsCode I = T
by A58;
consider d1,
b being
Int-Location such that A62:
I = SubFrom d1,
b
by A52, A61, SCMFSA_2:56;
A63:
2
in dom (product" (AddressParts T))
by A56, TARSKI:def 2;
then
f . 2
in (product" (AddressParts T)) . 2
by A55;
then
f . 2
in pi (AddressParts T),2
by A63, CARD_3:def 13;
then consider h being
Function such that A64:
h in AddressParts T
and A65:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
SCM+FSA such that A66:
h = AddressPart J
and A67:
InsCode J = T
by A64;
consider a,
d2 being
Int-Location such that A68:
J = SubFrom a,
d2
by A52, A67, SCMFSA_2:56;
A69:
h = <*a,d2*>
by A66, A68, Th20;
A70:
g = <*d1,b*>
by A60, A62, Th20;
A71:
for
k being
set st
k in {1,2} holds
<*d1,d2*> . k = f . k
dom <*d1,d2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then A75:
<*d1,d2*> = f
by A54, A56, A71, FUNCT_1:9;
A76:
InsCode (SubFrom d1,d2) = 3
by SCMFSA_2:44;
AddressPart (SubFrom d1,d2) = <*d1,d2*>
by Th20;
hence
x in AddressParts T
by A52, A53, A75, A76;
verum end; suppose A77:
T = 4
;
AddressParts T is product-like take
product" (AddressParts T)
;
CARD_3:def 14 AddressParts T = product (product" (AddressParts T))thus
AddressParts T c= product (product" (AddressParts T))
by CARD_3:94;
XBOOLE_0:def 10 product (product" (AddressParts T)) c= AddressParts Tlet x be
set ;
TARSKI:def 3 ( not x in product (product" (AddressParts T)) or x in AddressParts T )assume
x in product (product" (AddressParts T))
;
x in AddressParts Tthen consider f being
Function such that A78:
x = f
and A79:
dom f = dom (product" (AddressParts T))
and A80:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A81:
dom (product" (AddressParts T)) = {1,2}
by A77, Th34;
then A82:
1
in dom (product" (AddressParts T))
by TARSKI:def 2;
then
f . 1
in (product" (AddressParts T)) . 1
by A80;
then
f . 1
in pi (AddressParts T),1
by A82, CARD_3:def 13;
then consider g being
Function such that A83:
g in AddressParts T
and A84:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
SCM+FSA such that A85:
g = AddressPart I
and A86:
InsCode I = T
by A83;
consider d1,
b being
Int-Location such that A87:
I = MultBy d1,
b
by A77, A86, SCMFSA_2:57;
A88:
2
in dom (product" (AddressParts T))
by A81, TARSKI:def 2;
then
f . 2
in (product" (AddressParts T)) . 2
by A80;
then
f . 2
in pi (AddressParts T),2
by A88, CARD_3:def 13;
then consider h being
Function such that A89:
h in AddressParts T
and A90:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
SCM+FSA such that A91:
h = AddressPart J
and A92:
InsCode J = T
by A89;
consider a,
d2 being
Int-Location such that A93:
J = MultBy a,
d2
by A77, A92, SCMFSA_2:57;
A94:
h = <*a,d2*>
by A91, A93, Th21;
A95:
g = <*d1,b*>
by A85, A87, Th21;
A96:
for
k being
set st
k in {1,2} holds
<*d1,d2*> . k = f . k
dom <*d1,d2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then A100:
<*d1,d2*> = f
by A79, A81, A96, FUNCT_1:9;
A101:
InsCode (MultBy d1,d2) = 4
by SCMFSA_2:45;
AddressPart (MultBy d1,d2) = <*d1,d2*>
by Th21;
hence
x in AddressParts T
by A77, A78, A100, A101;
verum end; suppose A102:
T = 5
;
AddressParts T is product-like take
product" (AddressParts T)
;
CARD_3:def 14 AddressParts T = product (product" (AddressParts T))thus
AddressParts T c= product (product" (AddressParts T))
by CARD_3:94;
XBOOLE_0:def 10 product (product" (AddressParts T)) c= AddressParts Tlet x be
set ;
TARSKI:def 3 ( not x in product (product" (AddressParts T)) or x in AddressParts T )assume
x in product (product" (AddressParts T))
;
x in AddressParts Tthen consider f being
Function such that A103:
x = f
and A104:
dom f = dom (product" (AddressParts T))
and A105:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A106:
dom (product" (AddressParts T)) = {1,2}
by A102, Th35;
then A107:
1
in dom (product" (AddressParts T))
by TARSKI:def 2;
then
f . 1
in (product" (AddressParts T)) . 1
by A105;
then
f . 1
in pi (AddressParts T),1
by A107, CARD_3:def 13;
then consider g being
Function such that A108:
g in AddressParts T
and A109:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
SCM+FSA such that A110:
g = AddressPart I
and A111:
InsCode I = T
by A108;
consider d1,
b being
Int-Location such that A112:
I = Divide d1,
b
by A102, A111, SCMFSA_2:58;
A113:
2
in dom (product" (AddressParts T))
by A106, TARSKI:def 2;
then
f . 2
in (product" (AddressParts T)) . 2
by A105;
then
f . 2
in pi (AddressParts T),2
by A113, CARD_3:def 13;
then consider h being
Function such that A114:
h in AddressParts T
and A115:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
SCM+FSA such that A116:
h = AddressPart J
and A117:
InsCode J = T
by A114;
consider a,
d2 being
Int-Location such that A118:
J = Divide a,
d2
by A102, A117, SCMFSA_2:58;
A119:
h = <*a,d2*>
by A116, A118, Th22;
A120:
g = <*d1,b*>
by A110, A112, Th22;
A121:
for
k being
set st
k in {1,2} holds
<*d1,d2*> . k = f . k
dom <*d1,d2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then A125:
<*d1,d2*> = f
by A104, A106, A121, FUNCT_1:9;
A126:
InsCode (Divide d1,d2) = 5
by SCMFSA_2:46;
AddressPart (Divide d1,d2) = <*d1,d2*>
by Th22;
hence
x in AddressParts T
by A102, A103, A125, A126;
verum end; suppose A127:
T = 6
;
AddressParts T is product-like take
product" (AddressParts T)
;
CARD_3:def 14 AddressParts T = product (product" (AddressParts T))thus
AddressParts T c= product (product" (AddressParts T))
by CARD_3:94;
XBOOLE_0:def 10 product (product" (AddressParts T)) c= AddressParts Tlet x be
set ;
TARSKI:def 3 ( not x in product (product" (AddressParts T)) or x in AddressParts T )assume
x in product (product" (AddressParts T))
;
x in AddressParts Tthen consider f being
Function such that A128:
x = f
and A129:
dom f = dom (product" (AddressParts T))
and A130:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A131:
dom (product" (AddressParts T)) = {1}
by A127, Th36;
then A132:
1
in dom (product" (AddressParts T))
by TARSKI:def 1;
then
f . 1
in (product" (AddressParts T)) . 1
by A130;
then
f . 1
in pi (AddressParts T),1
by A132, CARD_3:def 13;
then consider g being
Function such that A133:
g in AddressParts T
and A134:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
SCM+FSA such that A135:
g = AddressPart I
and A136:
InsCode I = T
by A133;
consider i1 being
Element of
NAT such that A137:
I = goto i1
by A127, A136, SCMFSA_2:59;
A138:
for
k being
set st
k in {1} holds
<*i1*> . k = f . k
dom <*i1*> = {1}
by FINSEQ_1:4, FINSEQ_1:def 8;
then A139:
<*i1*> = f
by A129, A131, A138, FUNCT_1:9;
A140:
InsCode (goto i1) = 6
by SCMFSA_2:47;
AddressPart (goto i1) = <*i1*>
by Th23;
hence
x in AddressParts T
by A127, A128, A139, A140;
verum end; suppose A141:
T = 7
;
AddressParts T is product-like take
product" (AddressParts T)
;
CARD_3:def 14 AddressParts T = product (product" (AddressParts T))thus
AddressParts T c= product (product" (AddressParts T))
by CARD_3:94;
XBOOLE_0:def 10 product (product" (AddressParts T)) c= AddressParts Tlet x be
set ;
TARSKI:def 3 ( not x in product (product" (AddressParts T)) or x in AddressParts T )assume
x in product (product" (AddressParts T))
;
x in AddressParts Tthen consider f being
Function such that A142:
x = f
and A143:
dom f = dom (product" (AddressParts T))
and A144:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A145:
dom (product" (AddressParts T)) = {1,2}
by A141, Th37;
then A146:
1
in dom (product" (AddressParts T))
by TARSKI:def 2;
then
f . 1
in (product" (AddressParts T)) . 1
by A144;
then
f . 1
in pi (AddressParts T),1
by A146, CARD_3:def 13;
then consider g being
Function such that A147:
g in AddressParts T
and A148:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
SCM+FSA such that A149:
g = AddressPart I
and A150:
InsCode I = T
by A147;
consider i1 being
Element of
NAT ,
d1 being
Int-Location such that A151:
I = d1 =0_goto i1
by A141, A150, SCMFSA_2:60;
A152:
2
in dom (product" (AddressParts T))
by A145, TARSKI:def 2;
then
f . 2
in (product" (AddressParts T)) . 2
by A144;
then
f . 2
in pi (AddressParts T),2
by A152, CARD_3:def 13;
then consider h being
Function such that A153:
h in AddressParts T
and A154:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
SCM+FSA such that A155:
h = AddressPart J
and A156:
InsCode J = T
by A153;
consider i2 being
Element of
NAT ,
d2 being
Int-Location such that A157:
J = d2 =0_goto i2
by A141, A156, SCMFSA_2:60;
A158:
h = <*i2,d2*>
by A155, A157, Th24;
A159:
g = <*i1,d1*>
by A149, A151, Th24;
A160:
for
k being
set st
k in {1,2} holds
<*i1,d2*> . k = f . k
dom <*i1,d2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then A164:
<*i1,d2*> = f
by A143, A145, A160, FUNCT_1:9;
A165:
InsCode (d2 =0_goto i1) = 7
by SCMFSA_2:48;
AddressPart (d2 =0_goto i1) = <*i1,d2*>
by Th24;
hence
x in AddressParts T
by A141, A142, A164, A165;
verum end; suppose A166:
T = 8
;
AddressParts T is product-like take
product" (AddressParts T)
;
CARD_3:def 14 AddressParts T = product (product" (AddressParts T))thus
AddressParts T c= product (product" (AddressParts T))
by CARD_3:94;
XBOOLE_0:def 10 product (product" (AddressParts T)) c= AddressParts Tlet x be
set ;
TARSKI:def 3 ( not x in product (product" (AddressParts T)) or x in AddressParts T )assume
x in product (product" (AddressParts T))
;
x in AddressParts Tthen consider f being
Function such that A167:
x = f
and A168:
dom f = dom (product" (AddressParts T))
and A169:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A170:
dom (product" (AddressParts T)) = {1,2}
by A166, Th38;
then A171:
1
in dom (product" (AddressParts T))
by TARSKI:def 2;
then
f . 1
in (product" (AddressParts T)) . 1
by A169;
then
f . 1
in pi (AddressParts T),1
by A171, CARD_3:def 13;
then consider g being
Function such that A172:
g in AddressParts T
and A173:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
SCM+FSA such that A174:
g = AddressPart I
and A175:
InsCode I = T
by A172;
consider i1 being
Element of
NAT ,
d1 being
Int-Location such that A176:
I = d1 >0_goto i1
by A166, A175, SCMFSA_2:61;
A177:
2
in dom (product" (AddressParts T))
by A170, TARSKI:def 2;
then
f . 2
in (product" (AddressParts T)) . 2
by A169;
then
f . 2
in pi (AddressParts T),2
by A177, CARD_3:def 13;
then consider h being
Function such that A178:
h in AddressParts T
and A179:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
SCM+FSA such that A180:
h = AddressPart J
and A181:
InsCode J = T
by A178;
consider i2 being
Element of
NAT ,
d2 being
Int-Location such that A182:
J = d2 >0_goto i2
by A166, A181, SCMFSA_2:61;
A183:
h = <*i2,d2*>
by A180, A182, Th25;
A184:
g = <*i1,d1*>
by A174, A176, Th25;
A185:
for
k being
set st
k in {1,2} holds
<*i1,d2*> . k = f . k
dom <*i1,d2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then A189:
<*i1,d2*> = f
by A168, A170, A185, FUNCT_1:9;
A190:
InsCode (d2 >0_goto i1) = 8
by SCMFSA_2:49;
AddressPart (d2 >0_goto i1) = <*i1,d2*>
by Th25;
hence
x in AddressParts T
by A166, A167, A189, A190;
verum end; suppose A191:
T = 9
;
AddressParts T is product-like take
product" (AddressParts T)
;
CARD_3:def 14 AddressParts T = product (product" (AddressParts T))thus
AddressParts T c= product (product" (AddressParts T))
by CARD_3:94;
XBOOLE_0:def 10 product (product" (AddressParts T)) c= AddressParts Tlet x be
set ;
TARSKI:def 3 ( not x in product (product" (AddressParts T)) or x in AddressParts T )assume
x in product (product" (AddressParts T))
;
x in AddressParts Tthen consider f being
Function such that A192:
x = f
and A193:
dom f = dom (product" (AddressParts T))
and A194:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A195:
dom (product" (AddressParts T)) = {1,2,3}
by A191, Th39;
then A196:
1
in dom (product" (AddressParts T))
by ENUMSET1:def 1;
then
f . 1
in (product" (AddressParts T)) . 1
by A194;
then
f . 1
in pi (AddressParts T),1
by A196, CARD_3:def 13;
then consider g being
Function such that A197:
g in AddressParts T
and A198:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
SCM+FSA such that A199:
g = AddressPart I
and A200:
InsCode I = T
by A197;
consider a,
b being
Int-Location ,
f1 being
FinSeq-Location such that A201:
I = b := f1,
a
by A191, A200, SCMFSA_2:62;
A202:
3
in dom (product" (AddressParts T))
by A195, ENUMSET1:def 1;
then
f . 3
in (product" (AddressParts T)) . 3
by A194;
then
f . 3
in pi (AddressParts T),3
by A202, CARD_3:def 13;
then consider z being
Function such that A203:
z in AddressParts T
and A204:
z . 3
= f . 3
by CARD_3:def 6;
consider K being
Instruction of
SCM+FSA such that A205:
z = AddressPart K
and A206:
InsCode K = T
by A203;
consider d3,
d4 being
Int-Location ,
f3 being
FinSeq-Location such that A207:
K = d4 := f3,
d3
by A191, A206, SCMFSA_2:62;
A208:
2
in dom (product" (AddressParts T))
by A195, ENUMSET1:def 1;
then
f . 2
in (product" (AddressParts T)) . 2
by A194;
then
f . 2
in pi (AddressParts T),2
by A208, CARD_3:def 13;
then consider h being
Function such that A209:
h in AddressParts T
and A210:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
SCM+FSA such that A211:
h = AddressPart J
and A212:
InsCode J = T
by A209;
consider d1,
d2 being
Int-Location ,
f2 being
FinSeq-Location such that A213:
J = d2 := f2,
d1
by A191, A212, SCMFSA_2:62;
A214:
z = <*d4,f3,d3*>
by A205, A207, MCART_1:def 2;
A215:
h = <*d2,f2,d1*>
by A211, A213, MCART_1:def 2;
A216:
g = <*b,f1,a*>
by A199, A201, MCART_1:def 2;
A217:
for
k being
set st
k in {1,2,3} holds
<*b,f2,d3*> . k = f . k
dom <*b,f2,d3*> = {1,2,3}
by FINSEQ_3:1, FINSEQ_3:30;
then A222:
<*b,f2,d3*> = f
by A193, A195, A217, FUNCT_1:9;
A223:
AddressPart (b := f2,d3) = <*b,f2,d3*>
by MCART_1:def 2;
InsCode (b := f2,d3) = 9
by SCMFSA_2:50;
hence
x in AddressParts T
by A191, A192, A222, A223;
verum end; suppose A224:
T = 10
;
AddressParts T is product-like take
product" (AddressParts T)
;
CARD_3:def 14 AddressParts T = product (product" (AddressParts T))thus
AddressParts T c= product (product" (AddressParts T))
by CARD_3:94;
XBOOLE_0:def 10 product (product" (AddressParts T)) c= AddressParts Tlet x be
set ;
TARSKI:def 3 ( not x in product (product" (AddressParts T)) or x in AddressParts T )assume
x in product (product" (AddressParts T))
;
x in AddressParts Tthen consider f being
Function such that A225:
x = f
and A226:
dom f = dom (product" (AddressParts T))
and A227:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A228:
dom (product" (AddressParts T)) = {1,2,3}
by A224, Th40;
then A229:
1
in dom (product" (AddressParts T))
by ENUMSET1:def 1;
then
f . 1
in (product" (AddressParts T)) . 1
by A227;
then
f . 1
in pi (AddressParts T),1
by A229, CARD_3:def 13;
then consider g being
Function such that A230:
g in AddressParts T
and A231:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
SCM+FSA such that A232:
g = AddressPart I
and A233:
InsCode I = T
by A230;
consider a,
b being
Int-Location ,
f1 being
FinSeq-Location such that A234:
I = f1,
a := b
by A224, A233, SCMFSA_2:63;
A235:
3
in dom (product" (AddressParts T))
by A228, ENUMSET1:def 1;
then
f . 3
in (product" (AddressParts T)) . 3
by A227;
then
f . 3
in pi (AddressParts T),3
by A235, CARD_3:def 13;
then consider z being
Function such that A236:
z in AddressParts T
and A237:
z . 3
= f . 3
by CARD_3:def 6;
consider K being
Instruction of
SCM+FSA such that A238:
z = AddressPart K
and A239:
InsCode K = T
by A236;
consider d3,
d4 being
Int-Location ,
f3 being
FinSeq-Location such that A240:
K = f3,
d3 := d4
by A224, A239, SCMFSA_2:63;
A241:
2
in dom (product" (AddressParts T))
by A228, ENUMSET1:def 1;
then
f . 2
in (product" (AddressParts T)) . 2
by A227;
then
f . 2
in pi (AddressParts T),2
by A241, CARD_3:def 13;
then consider h being
Function such that A242:
h in AddressParts T
and A243:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
SCM+FSA such that A244:
h = AddressPart J
and A245:
InsCode J = T
by A242;
consider d1,
d2 being
Int-Location ,
f2 being
FinSeq-Location such that A246:
J = f2,
d1 := d2
by A224, A245, SCMFSA_2:63;
A247:
z = <*d4,f3,d3*>
by A238, A240, MCART_1:def 2;
A248:
h = <*d2,f2,d1*>
by A244, A246, MCART_1:def 2;
A249:
g = <*b,f1,a*>
by A232, A234, MCART_1:def 2;
A250:
for
k being
set st
k in {1,2,3} holds
<*b,f2,d3*> . k = f . k
dom <*b,f2,d3*> = {1,2,3}
by FINSEQ_3:1, FINSEQ_3:30;
then A255:
<*b,f2,d3*> = f
by A226, A228, A250, FUNCT_1:9;
A256:
AddressPart (f2,d3 := b) = <*b,f2,d3*>
by MCART_1:def 2;
InsCode (f2,d3 := b) = 10
by SCMFSA_2:51;
hence
x in AddressParts T
by A224, A225, A255, A256;
verum end; suppose A257:
T = 11
;
AddressParts T is product-like take
product" (AddressParts T)
;
CARD_3:def 14 AddressParts T = product (product" (AddressParts T))thus
AddressParts T c= product (product" (AddressParts T))
by CARD_3:94;
XBOOLE_0:def 10 product (product" (AddressParts T)) c= AddressParts Tlet x be
set ;
TARSKI:def 3 ( not x in product (product" (AddressParts T)) or x in AddressParts T )assume
x in product (product" (AddressParts T))
;
x in AddressParts Tthen consider f being
Function such that A258:
x = f
and A259:
dom f = dom (product" (AddressParts T))
and A260:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A261:
dom (product" (AddressParts T)) = {1,2}
by A257, Th41;
then A262:
1
in dom (product" (AddressParts T))
by TARSKI:def 2;
then
f . 1
in (product" (AddressParts T)) . 1
by A260;
then
f . 1
in pi (AddressParts T),1
by A262, CARD_3:def 13;
then consider g being
Function such that A263:
g in AddressParts T
and A264:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
SCM+FSA such that A265:
g = AddressPart I
and A266:
InsCode I = T
by A263;
consider a being
Int-Location ,
f1 being
FinSeq-Location such that A267:
I = a :=len f1
by A257, A266, SCMFSA_2:64;
A268:
2
in dom (product" (AddressParts T))
by A261, TARSKI:def 2;
then
f . 2
in (product" (AddressParts T)) . 2
by A260;
then
f . 2
in pi (AddressParts T),2
by A268, CARD_3:def 13;
then consider h being
Function such that A269:
h in AddressParts T
and A270:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
SCM+FSA such that A271:
h = AddressPart J
and A272:
InsCode J = T
by A269;
consider b being
Int-Location ,
f2 being
FinSeq-Location such that A273:
J = b :=len f2
by A257, A272, SCMFSA_2:64;
A274:
h = <*b,f2*>
by A271, A273, MCART_1:def 2;
A275:
g = <*a,f1*>
by A265, A267, MCART_1:def 2;
A276:
for
k being
set st
k in {1,2} holds
<*a,f2*> . k = f . k
dom <*a,f2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then A280:
<*a,f2*> = f
by A259, A261, A276, FUNCT_1:9;
A281:
AddressPart (a :=len f2) = <*a,f2*>
by MCART_1:def 2;
InsCode (a :=len f2) = 11
by SCMFSA_2:52;
hence
x in AddressParts T
by A257, A258, A280, A281;
verum end; suppose A282:
T = 12
;
AddressParts T is product-like take
product" (AddressParts T)
;
CARD_3:def 14 AddressParts T = product (product" (AddressParts T))thus
AddressParts T c= product (product" (AddressParts T))
by CARD_3:94;
XBOOLE_0:def 10 product (product" (AddressParts T)) c= AddressParts Tlet x be
set ;
TARSKI:def 3 ( not x in product (product" (AddressParts T)) or x in AddressParts T )assume
x in product (product" (AddressParts T))
;
x in AddressParts Tthen consider f being
Function such that A283:
x = f
and A284:
dom f = dom (product" (AddressParts T))
and A285:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A286:
dom (product" (AddressParts T)) = {1,2}
by A282, Th42;
then A287:
1
in dom (product" (AddressParts T))
by TARSKI:def 2;
then
f . 1
in (product" (AddressParts T)) . 1
by A285;
then
f . 1
in pi (AddressParts T),1
by A287, CARD_3:def 13;
then consider g being
Function such that A288:
g in AddressParts T
and A289:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
SCM+FSA such that A290:
g = AddressPart I
and A291:
InsCode I = T
by A288;
consider a being
Int-Location ,
f1 being
FinSeq-Location such that A292:
I = f1 :=<0,...,0> a
by A282, A291, SCMFSA_2:65;
A293:
2
in dom (product" (AddressParts T))
by A286, TARSKI:def 2;
then
f . 2
in (product" (AddressParts T)) . 2
by A285;
then
f . 2
in pi (AddressParts T),2
by A293, CARD_3:def 13;
then consider h being
Function such that A294:
h in AddressParts T
and A295:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
SCM+FSA such that A296:
h = AddressPart J
and A297:
InsCode J = T
by A294;
consider b being
Int-Location ,
f2 being
FinSeq-Location such that A298:
J = f2 :=<0,...,0> b
by A282, A297, SCMFSA_2:65;
A299:
h = <*b,f2*>
by A296, A298, MCART_1:def 2;
A300:
g = <*a,f1*>
by A290, A292, MCART_1:def 2;
A301:
for
k being
set st
k in {1,2} holds
<*a,f2*> . k = f . k
dom <*a,f2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then A305:
<*a,f2*> = f
by A284, A286, A301, FUNCT_1:9;
A306:
AddressPart (f2 :=<0,...,0> a) = <*a,f2*>
by MCART_1:def 2;
InsCode (f2 :=<0,...,0> a) = 12
by SCMFSA_2:53;
hence
x in AddressParts T
by A282, A283, A305, A306;
verum end;