let T be InsType of SCM ; :: according to AMISTD_2:def 11 :: thesis: 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 ) by Lm3;
suppose A1: T = 0 ; :: thesis: AddressParts T is product-like
reconsider f = {} as Function ;
take f ; :: according to CARD_3:def 14 :: thesis: AddressParts T = product f
thus AddressParts T = product f by A1, Th16, CARD_3:19; :: thesis: verum
end;
suppose A2: T = 1 ; :: thesis: AddressParts T is product-like
take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis: AddressParts T = product (product" (AddressParts T))
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis: product (product" (AddressParts T)) c= AddressParts T
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product (product" (AddressParts T)) or x in AddressParts T )
assume x in product (product" (AddressParts T)) ; :: thesis: x in AddressParts T
then 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, Th17;
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 such that
A10: g = AddressPart I and
A11: InsCode I = T by A8;
consider d1, b being Data-Location such that
A12: I = d1 := b by A2, A11, AMI_5:47;
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 such that
A16: h = AddressPart J and
A17: InsCode J = T by A14;
consider a, d2 being Data-Location such that
A18: J = a := d2 by A2, A17, AMI_5:47;
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
proof
let k be set ; :: thesis: ( k in {1,2} implies <*d1,d2*> . k = f . k )
assume A22: k in {1,2} ; :: thesis: <*d1,d2*> . k = f . k
per cases ( k = 1 or k = 2 ) by A22, TARSKI:def 2;
suppose A23: k = 1 ; :: thesis: <*d1,d2*> . k = f . k
<*d1,d2*> . 1 = d1 by FINSEQ_1:61
.= f . 1 by A9, A20, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A23; :: thesis: verum
end;
suppose A24: k = 2 ; :: thesis: <*d1,d2*> . k = f . k
<*d1,d2*> . 2 = d2 by FINSEQ_1:61
.= f . 2 by A15, A19, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A24; :: thesis: verum
end;
end;
end;
A25: ( InsCode (d1 := d2) = 1 & AddressPart (d1 := d2) = <*d1,d2*> ) by MCART_1:7;
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; :: thesis: verum
end;
suppose A26: T = 2 ; :: thesis: AddressParts T is product-like
take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis: AddressParts T = product (product" (AddressParts T))
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis: product (product" (AddressParts T)) c= AddressParts T
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product (product" (AddressParts T)) or x in AddressParts T )
assume x in product (product" (AddressParts T)) ; :: thesis: x in AddressParts T
then 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, Th18;
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 such that
A34: g = AddressPart I and
A35: InsCode I = T by A32;
consider d1, b being Data-Location such that
A36: I = AddTo d1,b by A26, A35, AMI_5:48;
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 such that
A40: h = AddressPart J and
A41: InsCode J = T by A38;
consider a, d2 being Data-Location such that
A42: J = AddTo a,d2 by A26, A41, AMI_5:48;
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
proof
let k be set ; :: thesis: ( k in {1,2} implies <*d1,d2*> . k = f . k )
assume A46: k in {1,2} ; :: thesis: <*d1,d2*> . k = f . k
per cases ( k = 1 or k = 2 ) by A46, TARSKI:def 2;
suppose A47: k = 1 ; :: thesis: <*d1,d2*> . k = f . k
<*d1,d2*> . 1 = d1 by FINSEQ_1:61
.= f . 1 by A33, A44, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A47; :: thesis: verum
end;
suppose A48: k = 2 ; :: thesis: <*d1,d2*> . k = f . k
<*d1,d2*> . 2 = d2 by FINSEQ_1:61
.= f . 2 by A39, A43, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A48; :: thesis: verum
end;
end;
end;
A49: ( InsCode (AddTo d1,d2) = 2 & AddressPart (AddTo d1,d2) = <*d1,d2*> ) by MCART_1:7;
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; :: thesis: verum
end;
suppose A50: T = 3 ; :: thesis: AddressParts T is product-like
take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis: AddressParts T = product (product" (AddressParts T))
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis: product (product" (AddressParts T)) c= AddressParts T
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product (product" (AddressParts T)) or x in AddressParts T )
assume x in product (product" (AddressParts T)) ; :: thesis: x in AddressParts T
then 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, Th19;
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 such that
A58: g = AddressPart I and
A59: InsCode I = T by A56;
consider d1, b being Data-Location such that
A60: I = SubFrom d1,b by A50, A59, AMI_5:49;
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 such that
A64: h = AddressPart J and
A65: InsCode J = T by A62;
consider a, d2 being Data-Location such that
A66: J = SubFrom a,d2 by A50, A65, AMI_5:49;
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
proof
let k be set ; :: thesis: ( k in {1,2} implies <*d1,d2*> . k = f . k )
assume A70: k in {1,2} ; :: thesis: <*d1,d2*> . k = f . k
per cases ( k = 1 or k = 2 ) by A70, TARSKI:def 2;
suppose A71: k = 1 ; :: thesis: <*d1,d2*> . k = f . k
<*d1,d2*> . 1 = d1 by FINSEQ_1:61
.= f . 1 by A57, A68, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A71; :: thesis: verum
end;
suppose A72: k = 2 ; :: thesis: <*d1,d2*> . k = f . k
<*d1,d2*> . 2 = d2 by FINSEQ_1:61
.= f . 2 by A63, A67, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A72; :: thesis: verum
end;
end;
end;
A73: ( InsCode (SubFrom d1,d2) = 3 & AddressPart (SubFrom d1,d2) = <*d1,d2*> ) by MCART_1:7;
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; :: thesis: verum
end;
suppose A74: T = 4 ; :: thesis: AddressParts T is product-like
take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis: AddressParts T = product (product" (AddressParts T))
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis: product (product" (AddressParts T)) c= AddressParts T
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product (product" (AddressParts T)) or x in AddressParts T )
assume x in product (product" (AddressParts T)) ; :: thesis: x in AddressParts T
then 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, Th20;
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 such that
A82: g = AddressPart I and
A83: InsCode I = T by A80;
consider d1, b being Data-Location such that
A84: I = MultBy d1,b by A74, A83, AMI_5:50;
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 such that
A88: h = AddressPart J and
A89: InsCode J = T by A86;
consider a, d2 being Data-Location such that
A90: J = MultBy a,d2 by A74, A89, AMI_5:50;
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
proof
let k be set ; :: thesis: ( k in {1,2} implies <*d1,d2*> . k = f . k )
assume A94: k in {1,2} ; :: thesis: <*d1,d2*> . k = f . k
per cases ( k = 1 or k = 2 ) by A94, TARSKI:def 2;
suppose A95: k = 1 ; :: thesis: <*d1,d2*> . k = f . k
<*d1,d2*> . 1 = d1 by FINSEQ_1:61
.= f . 1 by A81, A92, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A95; :: thesis: verum
end;
suppose A96: k = 2 ; :: thesis: <*d1,d2*> . k = f . k
<*d1,d2*> . 2 = d2 by FINSEQ_1:61
.= f . 2 by A87, A91, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A96; :: thesis: verum
end;
end;
end;
A97: ( InsCode (MultBy d1,d2) = 4 & AddressPart (MultBy d1,d2) = <*d1,d2*> ) by MCART_1:7;
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; :: thesis: verum
end;
suppose A98: T = 5 ; :: thesis: AddressParts T is product-like
take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis: AddressParts T = product (product" (AddressParts T))
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis: product (product" (AddressParts T)) c= AddressParts T
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product (product" (AddressParts T)) or x in AddressParts T )
assume x in product (product" (AddressParts T)) ; :: thesis: x in AddressParts T
then 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, Th21;
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 such that
A106: g = AddressPart I and
A107: InsCode I = T by A104;
consider d1, b being Data-Location such that
A108: I = Divide d1,b by A98, A107, AMI_5:51;
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 such that
A112: h = AddressPart J and
A113: InsCode J = T by A110;
consider a, d2 being Data-Location such that
A114: J = Divide a,d2 by A98, A113, AMI_5:51;
A115: h = <*a,d2*> by A112, A114, MCART_1:def 2;
A116: g = <*d1,b*> by A106, A108, MCART_1:def 2;
A117: for k being set st k in {1,2} holds
<*d1,d2*> . k = f . k
proof
let k be set ; :: thesis: ( k in {1,2} implies <*d1,d2*> . k = f . k )
assume A118: k in {1,2} ; :: thesis: <*d1,d2*> . k = f . k
per cases ( k = 1 or k = 2 ) by A118, TARSKI:def 2;
suppose A119: k = 1 ; :: thesis: <*d1,d2*> . k = f . k
<*d1,d2*> . 1 = d1 by FINSEQ_1:61
.= f . 1 by A105, A116, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A119; :: thesis: verum
end;
suppose A120: k = 2 ; :: thesis: <*d1,d2*> . k = f . k
<*d1,d2*> . 2 = d2 by FINSEQ_1:61
.= f . 2 by A111, A115, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A120; :: thesis: verum
end;
end;
end;
A121: ( InsCode (Divide d1,d2) = 5 & AddressPart (Divide d1,d2) = <*d1,d2*> ) by MCART_1:7;
dom <*d1,d2*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
then <*d1,d2*> = f by A100, A102, A117, FUNCT_1:9;
hence x in AddressParts T by A98, A99, A121; :: thesis: verum
end;
suppose A122: T = 6 ; :: thesis: AddressParts T is product-like
take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis: AddressParts T = product (product" (AddressParts T))
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis: product (product" (AddressParts T)) c= AddressParts T
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product (product" (AddressParts T)) or x in AddressParts T )
assume x in product (product" (AddressParts T)) ; :: thesis: x in AddressParts T
then 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, Th22;
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 such that
A130: g = AddressPart I and
A131: InsCode I = T by A128;
consider i1 being Element of NAT such that
A132: I = SCM-goto i1 by A122, A131, AMI_5:52;
A133: for k being set st k in {1} holds
<*i1*> . k = f . k
proof
let k be set ; :: thesis: ( k in {1} implies <*i1*> . k = f . k )
assume k in {1} ; :: thesis: <*i1*> . k = f . k
then k = 1 by TARSKI:def 1;
hence <*i1*> . k = f . k by A129, A130, A132, MCART_1:def 2; :: thesis: verum
end;
A134: ( InsCode (SCM-goto i1) = 6 & AddressPart (SCM-goto i1) = <*i1*> ) by MCART_1:7;
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; :: thesis: verum
end;
suppose A135: T = 7 ; :: thesis: AddressParts T is product-like
take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis: AddressParts T = product (product" (AddressParts T))
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis: product (product" (AddressParts T)) c= AddressParts T
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product (product" (AddressParts T)) or x in AddressParts T )
assume x in product (product" (AddressParts T)) ; :: thesis: x in AddressParts T
then 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, Th23;
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 such that
A143: g = AddressPart I and
A144: InsCode I = T by A141;
consider i1 being Element of NAT , d1 being Data-Location such that
A145: I = d1 =0_goto i1 by A135, A144, AMI_5:53;
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 such that
A149: h = AddressPart J and
A150: InsCode J = T by A147;
consider i2 being Element of NAT , d2 being Data-Location such that
A151: J = d2 =0_goto i2 by A135, A150, AMI_5:53;
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
proof
let k be set ; :: thesis: ( k in {1,2} implies <*i1,d2*> . k = f . k )
assume A155: k in {1,2} ; :: thesis: <*i1,d2*> . k = f . k
per cases ( k = 1 or k = 2 ) by A155, TARSKI:def 2;
suppose A156: k = 1 ; :: thesis: <*i1,d2*> . k = f . k
<*i1,d2*> . 1 = i1 by FINSEQ_1:61
.= f . 1 by A142, A153, FINSEQ_1:61 ;
hence <*i1,d2*> . k = f . k by A156; :: thesis: verum
end;
suppose A157: k = 2 ; :: thesis: <*i1,d2*> . k = f . k
<*i1,d2*> . 2 = d2 by FINSEQ_1:61
.= f . 2 by A148, A152, FINSEQ_1:61 ;
hence <*i1,d2*> . k = f . k by A157; :: thesis: verum
end;
end;
end;
A158: ( InsCode (d2 =0_goto i1) = 7 & AddressPart (d2 =0_goto i1) = <*i1,d2*> ) by MCART_1:7;
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; :: thesis: verum
end;
suppose A159: T = 8 ; :: thesis: AddressParts T is product-like
take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis: AddressParts T = product (product" (AddressParts T))
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis: product (product" (AddressParts T)) c= AddressParts T
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product (product" (AddressParts T)) or x in AddressParts T )
assume x in product (product" (AddressParts T)) ; :: thesis: x in AddressParts T
then consider f being Function such that
A160: x = f and
A161: dom f = dom (product" (AddressParts T)) and
A162: for k being set st k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k by CARD_3:def 5;
A163: dom (product" (AddressParts T)) = {1,2} by A159, Th24;
then A164: 1 in dom (product" (AddressParts T)) by TARSKI:def 2;
then f . 1 in (product" (AddressParts T)) . 1 by A162;
then f . 1 in pi (AddressParts T),1 by A164, CARD_3:def 13;
then consider g being Function such that
A165: g in AddressParts T and
A166: g . 1 = f . 1 by CARD_3:def 6;
consider I being Instruction of SCM such that
A167: g = AddressPart I and
A168: InsCode I = T by A165;
consider i1 being Element of NAT , d1 being Data-Location such that
A169: I = d1 >0_goto i1 by A159, A168, AMI_5:54;
A170: 2 in dom (product" (AddressParts T)) by A163, TARSKI:def 2;
then f . 2 in (product" (AddressParts T)) . 2 by A162;
then f . 2 in pi (AddressParts T),2 by A170, CARD_3:def 13;
then consider h being Function such that
A171: h in AddressParts T and
A172: h . 2 = f . 2 by CARD_3:def 6;
consider J being Instruction of SCM such that
A173: h = AddressPart J and
A174: InsCode J = T by A171;
consider i2 being Element of NAT , d2 being Data-Location such that
A175: J = d2 >0_goto i2 by A159, A174, AMI_5:54;
A176: h = <*i2,d2*> by A173, A175, MCART_1:def 2;
A177: g = <*i1,d1*> by A167, A169, MCART_1:def 2;
A178: for k being set st k in {1,2} holds
<*i1,d2*> . k = f . k
proof
let k be set ; :: thesis: ( k in {1,2} implies <*i1,d2*> . k = f . k )
assume A179: k in {1,2} ; :: thesis: <*i1,d2*> . k = f . k
per cases ( k = 1 or k = 2 ) by A179, TARSKI:def 2;
suppose A180: k = 1 ; :: thesis: <*i1,d2*> . k = f . k
<*i1,d2*> . 1 = i1 by FINSEQ_1:61
.= f . 1 by A166, A177, FINSEQ_1:61 ;
hence <*i1,d2*> . k = f . k by A180; :: thesis: verum
end;
suppose A181: k = 2 ; :: thesis: <*i1,d2*> . k = f . k
<*i1,d2*> . 2 = d2 by FINSEQ_1:61
.= f . 2 by A172, A176, FINSEQ_1:61 ;
hence <*i1,d2*> . k = f . k by A181; :: thesis: verum
end;
end;
end;
A182: ( InsCode (d2 >0_goto i1) = 8 & AddressPart (d2 >0_goto i1) = <*i1,d2*> ) by MCART_1:7;
dom <*i1,d2*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
then <*i1,d2*> = f by A161, A163, A178, FUNCT_1:9;
hence x in AddressParts T by A159, A160, A182; :: thesis: verum
end;
end;