let a be Int-Location ; for f being FinSeq-Location holds (product" (AddressParts (InsCode (f :=<0,...,0> a)))) . 1 = SCM+FSA-Data-Loc
let f be FinSeq-Location ; (product" (AddressParts (InsCode (f :=<0,...,0> a)))) . 1 = SCM+FSA-Data-Loc
dom (product" (AddressParts (InsCode (f :=<0,...,0> a)))) = {1,2}
by Th42, SCMFSA_2:53;
then A1:
1 in dom (product" (AddressParts (InsCode (f :=<0,...,0> a))))
by TARSKI:def 2;
hereby TARSKI:def 3,
XBOOLE_0:def 10 SCM+FSA-Data-Loc c= (product" (AddressParts (InsCode (f :=<0,...,0> a)))) . 1
let x be
set ;
( x in (product" (AddressParts (InsCode (f :=<0,...,0> a)))) . 1 implies x in SCM+FSA-Data-Loc )assume
x in (product" (AddressParts (InsCode (f :=<0,...,0> a)))) . 1
;
x in SCM+FSA-Data-Loc then
x in pi (AddressParts (InsCode (f :=<0,...,0> a))),1
by A1, CARD_3:93;
then consider g being
Function such that A2:
g in AddressParts (InsCode (f :=<0,...,0> a))
and A3:
x = g . 1
by CARD_3:def 6;
consider I being
Instruction of
SCM+FSA such that A4:
g = AddressPart I
and A5:
InsCode I = InsCode (f :=<0,...,0> a)
by A2;
consider a being
Int-Location ,
f being
FinSeq-Location such that A6:
I = f :=<0,...,0> a
by A5, SCMFSA_2:53, SCMFSA_2:65;
g = <*a,f*>
by A4, A6, MCART_1:def 2;
then
x = a
by A3, FINSEQ_1:61;
hence
x in SCM+FSA-Data-Loc
by SCMFSA_2:def 4;
verum
end;
let x be set ; TARSKI:def 3 ( not x in SCM+FSA-Data-Loc or x in (product" (AddressParts (InsCode (f :=<0,...,0> a)))) . 1 )
assume
x in SCM+FSA-Data-Loc
; x in (product" (AddressParts (InsCode (f :=<0,...,0> a)))) . 1
then reconsider x = x as Int-Location by SCMFSA_2:28;
A7:
<*x,f*> . 1 = x
by FINSEQ_1:61;
InsCode (f :=<0,...,0> a) = 12
by SCMFSA_2:53;
then A8:
InsCode (f :=<0,...,0> x) = InsCode (f :=<0,...,0> a)
by SCMFSA_2:53;
AddressPart (f :=<0,...,0> x) = <*x,f*>
by MCART_1:def 2;
then
<*x,f*> in AddressParts (InsCode (f :=<0,...,0> a))
by A8;
then
x in pi (AddressParts (InsCode (f :=<0,...,0> a))),1
by A7, CARD_3:def 6;
hence
x in (product" (AddressParts (InsCode (f :=<0,...,0> a)))) . 1
by A1, CARD_3:93; verum