let T be InsType of (SCM R); 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 )
by Lm3;
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, Th33;
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 R) such that A10:
g = AddressPart I
and A11:
InsCode I = T
by A8;
consider d1,
b being
Data-Location of
R such that A12:
I = d1 := b
by A2, A11, Th17;
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 R) such that A16:
h = AddressPart J
and A17:
InsCode J = T
by A14;
consider a,
d2 being
Data-Location of
R such that A18:
J = a := d2
by A2, A17, Th17;
A19:
h = <*a,d2*>
by A16, A18, MCART_1:def 2;
A20:
g = <*d1,b*>
by A10, A12, MCART_1:def 2;
A21:
for
k being
set st
k in {1,2} holds
<*d1,d2*> . k = f . k
A25:
(
InsCode (d1 := d2) = 1 &
AddressPart (d1 := d2) = <*d1,d2*> )
by MCART_1:def 1, MCART_1:def 2;
dom <*d1,d2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then
<*d1,d2*> = f
by A4, A6, A21, FUNCT_1:9;
hence
x in AddressParts T
by A2, A3, A25;
verum end; suppose A26:
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 A27:
x = f
and A28:
dom f = dom (product" (AddressParts T))
and A29:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A30:
dom (product" (AddressParts T)) = {1,2}
by A26, Th34;
then A31:
1
in dom (product" (AddressParts T))
by TARSKI:def 2;
then
f . 1
in (product" (AddressParts T)) . 1
by A29;
then
f . 1
in pi (AddressParts T),1
by A31, CARD_3:def 13;
then consider g being
Function such that A32:
g in AddressParts T
and A33:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
(SCM R) such that A34:
g = AddressPart I
and A35:
InsCode I = T
by A32;
consider d1,
b being
Data-Location of
R such that A36:
I = AddTo d1,
b
by A26, A35, Th18;
A37:
2
in dom (product" (AddressParts T))
by A30, TARSKI:def 2;
then
f . 2
in (product" (AddressParts T)) . 2
by A29;
then
f . 2
in pi (AddressParts T),2
by A37, CARD_3:def 13;
then consider h being
Function such that A38:
h in AddressParts T
and A39:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
(SCM R) such that A40:
h = AddressPart J
and A41:
InsCode J = T
by A38;
consider a,
d2 being
Data-Location of
R such that A42:
J = AddTo a,
d2
by A26, A41, Th18;
A43:
h = <*a,d2*>
by A40, A42, MCART_1:def 2;
A44:
g = <*d1,b*>
by A34, A36, MCART_1:def 2;
A45:
for
k being
set st
k in {1,2} holds
<*d1,d2*> . k = f . k
A49:
(
InsCode (AddTo d1,d2) = 2 &
AddressPart (AddTo d1,d2) = <*d1,d2*> )
by MCART_1:def 1, MCART_1:def 2;
dom <*d1,d2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then
<*d1,d2*> = f
by A28, A30, A45, FUNCT_1:9;
hence
x in AddressParts T
by A26, A27, A49;
verum end; suppose A50:
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 A51:
x = f
and A52:
dom f = dom (product" (AddressParts T))
and A53:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A54:
dom (product" (AddressParts T)) = {1,2}
by A50, Th35;
then A55:
1
in dom (product" (AddressParts T))
by TARSKI:def 2;
then
f . 1
in (product" (AddressParts T)) . 1
by A53;
then
f . 1
in pi (AddressParts T),1
by A55, CARD_3:def 13;
then consider g being
Function such that A56:
g in AddressParts T
and A57:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
(SCM R) such that A58:
g = AddressPart I
and A59:
InsCode I = T
by A56;
consider d1,
b being
Data-Location of
R such that A60:
I = SubFrom d1,
b
by A50, A59, Th19;
A61:
2
in dom (product" (AddressParts T))
by A54, TARSKI:def 2;
then
f . 2
in (product" (AddressParts T)) . 2
by A53;
then
f . 2
in pi (AddressParts T),2
by A61, CARD_3:def 13;
then consider h being
Function such that A62:
h in AddressParts T
and A63:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
(SCM R) such that A64:
h = AddressPart J
and A65:
InsCode J = T
by A62;
consider a,
d2 being
Data-Location of
R such that A66:
J = SubFrom a,
d2
by A50, A65, Th19;
A67:
h = <*a,d2*>
by A64, A66, MCART_1:def 2;
A68:
g = <*d1,b*>
by A58, A60, MCART_1:def 2;
A69:
for
k being
set st
k in {1,2} holds
<*d1,d2*> . k = f . k
A73:
(
InsCode (SubFrom d1,d2) = 3 &
AddressPart (SubFrom d1,d2) = <*d1,d2*> )
by MCART_1:def 1, MCART_1:def 2;
dom <*d1,d2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then
<*d1,d2*> = f
by A52, A54, A69, FUNCT_1:9;
hence
x in AddressParts T
by A50, A51, A73;
verum end; suppose A74:
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 A75:
x = f
and A76:
dom f = dom (product" (AddressParts T))
and A77:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A78:
dom (product" (AddressParts T)) = {1,2}
by A74, Th36;
then A79:
1
in dom (product" (AddressParts T))
by TARSKI:def 2;
then
f . 1
in (product" (AddressParts T)) . 1
by A77;
then
f . 1
in pi (AddressParts T),1
by A79, CARD_3:def 13;
then consider g being
Function such that A80:
g in AddressParts T
and A81:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
(SCM R) such that A82:
g = AddressPart I
and A83:
InsCode I = T
by A80;
consider d1,
b being
Data-Location of
R such that A84:
I = MultBy d1,
b
by A74, A83, Th20;
A85:
2
in dom (product" (AddressParts T))
by A78, TARSKI:def 2;
then
f . 2
in (product" (AddressParts T)) . 2
by A77;
then
f . 2
in pi (AddressParts T),2
by A85, CARD_3:def 13;
then consider h being
Function such that A86:
h in AddressParts T
and A87:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
(SCM R) such that A88:
h = AddressPart J
and A89:
InsCode J = T
by A86;
consider a,
d2 being
Data-Location of
R such that A90:
J = MultBy a,
d2
by A74, A89, Th20;
A91:
h = <*a,d2*>
by A88, A90, MCART_1:def 2;
A92:
g = <*d1,b*>
by A82, A84, MCART_1:def 2;
A93:
for
k being
set st
k in {1,2} holds
<*d1,d2*> . k = f . k
A97:
(
InsCode (MultBy d1,d2) = 4 &
AddressPart (MultBy d1,d2) = <*d1,d2*> )
by MCART_1:def 1, MCART_1:def 2;
dom <*d1,d2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then
<*d1,d2*> = f
by A76, A78, A93, FUNCT_1:9;
hence
x in AddressParts T
by A74, A75, A97;
verum end; suppose A98:
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 A99:
x = f
and A100:
dom f = dom (product" (AddressParts T))
and A101:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A102:
dom (product" (AddressParts T)) = {1,2}
by A98, Th37;
then A103:
1
in dom (product" (AddressParts T))
by TARSKI:def 2;
then
f . 1
in (product" (AddressParts T)) . 1
by A101;
then
f . 1
in pi (AddressParts T),1
by A103, CARD_3:def 13;
then consider g being
Function such that A104:
g in AddressParts T
and A105:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
(SCM R) such that A106:
g = AddressPart I
and A107:
InsCode I = T
by A104;
consider d1 being
Data-Location of
R,
r being
Element of
R such that A108:
I = d1 := r
by A98, A107, Th21;
A109:
2
in dom (product" (AddressParts T))
by A102, TARSKI:def 2;
then
f . 2
in (product" (AddressParts T)) . 2
by A101;
then
f . 2
in pi (AddressParts T),2
by A109, CARD_3:def 13;
then consider h being
Function such that A110:
h in AddressParts T
and A111:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
(SCM R) such that A112:
h = AddressPart J
and A113:
InsCode J = T
by A110;
consider a being
Data-Location of
R,
r2 being
Element of
R such that A114:
J = a := r2
by A98, A113, Th21;
A115:
h = <*a,r2*>
by A112, A114, MCART_1:def 2;
A116:
g = <*d1,r*>
by A106, A108, MCART_1:def 2;
A117:
for
k being
set st
k in {1,2} holds
<*d1,r2*> . k = f . k
A121:
(
InsCode (d1 := r2) = 5 &
AddressPart (d1 := r2) = <*d1,r2*> )
by MCART_1:def 1, MCART_1:def 2;
dom <*d1,r2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then
<*d1,r2*> = f
by A100, A102, A117, FUNCT_1:9;
hence
x in AddressParts T
by A98, A99, A121;
verum end; suppose A122:
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 A123:
x = f
and A124:
dom f = dom (product" (AddressParts T))
and A125:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A126:
dom (product" (AddressParts T)) = {1}
by A122, Th38;
then A127:
1
in dom (product" (AddressParts T))
by TARSKI:def 1;
then
f . 1
in (product" (AddressParts T)) . 1
by A125;
then
f . 1
in pi (AddressParts T),1
by A127, CARD_3:def 13;
then consider g being
Function such that A128:
g in AddressParts T
and A129:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
(SCM R) such that A130:
g = AddressPart I
and A131:
InsCode I = T
by A128;
consider i1 being
Element of
NAT such that A132:
I = goto i1,
R
by A122, A131, Th22;
A133:
for
k being
set st
k in {1} holds
<*i1*> . k = f . k
A134:
(
InsCode (goto i1,R) = 6 &
AddressPart (goto i1,R) = <*i1*> )
by MCART_1:def 1, MCART_1:def 2;
dom <*i1*> = {1}
by FINSEQ_1:4, FINSEQ_1:def 8;
then
<*i1*> = f
by A124, A126, A133, FUNCT_1:9;
hence
x in AddressParts T
by A122, A123, A134;
verum end; suppose A135:
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 A136:
x = f
and A137:
dom f = dom (product" (AddressParts T))
and A138:
for
k being
set st
k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k
by CARD_3:def 5;
A139:
dom (product" (AddressParts T)) = {1,2}
by A135, Th39;
then A140:
1
in dom (product" (AddressParts T))
by TARSKI:def 2;
then
f . 1
in (product" (AddressParts T)) . 1
by A138;
then
f . 1
in pi (AddressParts T),1
by A140, CARD_3:def 13;
then consider g being
Function such that A141:
g in AddressParts T
and A142:
g . 1
= f . 1
by CARD_3:def 6;
consider I being
Instruction of
(SCM R) such that A143:
g = AddressPart I
and A144:
InsCode I = T
by A141;
consider d1 being
Data-Location of
R,
i1 being
Element of
NAT such that A145:
I = d1 =0_goto i1
by A135, A144, Th23;
A146:
2
in dom (product" (AddressParts T))
by A139, TARSKI:def 2;
then
f . 2
in (product" (AddressParts T)) . 2
by A138;
then
f . 2
in pi (AddressParts T),2
by A146, CARD_3:def 13;
then consider h being
Function such that A147:
h in AddressParts T
and A148:
h . 2
= f . 2
by CARD_3:def 6;
consider J being
Instruction of
(SCM R) such that A149:
h = AddressPart J
and A150:
InsCode J = T
by A147;
consider d2 being
Data-Location of
R,
i2 being
Element of
NAT such that A151:
J = d2 =0_goto i2
by A135, A150, Th23;
A152:
h = <*i2,d2*>
by A149, A151, MCART_1:def 2;
A153:
g = <*i1,d1*>
by A143, A145, MCART_1:def 2;
A154:
for
k being
set st
k in {1,2} holds
<*i1,d2*> . k = f . k
A158:
(
InsCode (d2 =0_goto i1) = 7 &
AddressPart (d2 =0_goto i1) = <*i1,d2*> )
by MCART_1:def 1, MCART_1:def 2;
dom <*i1,d2*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then
<*i1,d2*> = f
by A137, A139, A154, FUNCT_1:9;
hence
x in AddressParts T
by A135, A136, A158;
verum end;