let ins be Instruction of SCM+FSA; ( InsCode ins = 9 implies ex a, b being Int-Location ex fa being FinSeq-Location st ins = b := (fa,a) )
assume A1:
InsCode ins = 9
; ex a, b being Int-Location ex fa being FinSeq-Location st ins = b := (fa,a)
A2:
now not ins in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } assume
ins in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} }
;
contradictionthen consider K being
Element of
Segm 13,
dC being
Element of
SCM+FSA-Data-Loc ,
fB being
Element of
SCM+FSA-Data*-Loc such that A3:
ins = [K,{},<*dC,fB*>]
and A4:
K in {11,12}
;
(
K = 11 or
K = 12 )
by A4, TARSKI:def 2;
hence
contradiction
by A1, A3;
verum end;
( ins in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } or ins in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } )
by XBOOLE_0:def 3;
then
( ins in SCM-Instr or ins in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } )
by A2, XBOOLE_0:def 3;
then consider L being Element of Segm 13, dA, dB being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A5:
ins = [L,{},<*dB,fA,dA*>]
and
L in {9,10}
by A1, AMI_5:5;
reconsider f = fA as FinSeq-Location by Def3;
reconsider c = dB, b = dA as Int-Location by AMI_2:def 16;
take
b
; ex b being Int-Location ex fa being FinSeq-Location st ins = b := (fa,b)
take
c
; ex fa being FinSeq-Location st ins = c := (fa,b)
take
f
; ins = c := (f,b)
thus
ins = c := (f,b)
by A1, A5; verum