let I be Instruction of SCMPDS; ( InsCode I = 9 implies ex a, b being Int_position ex k1, k2 being Integer st I = AddTo (a,k1,b,k2) )
assume A1:
InsCode I = 9
; ex a, b being Int_position ex k1, k2 being Integer st I = AddTo (a,k1,b,k2)
( I in {[0,{},{}]} or I in { [14,{},<*k1*>] where k1 is Element of INT : verum } or I in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } or I in { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } or I in { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } or I in { [I3,{},<*d4,d5,k5,k6*>] where I3 is Element of Segm 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } )
by Lm1;
then consider I1 being Element of Segm 15, d1, d2 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A2:
I = [I1,{},<*d1,d2,k1,k2*>]
and
I1 in {9,10,11,12,13}
by A1, Lm9;
consider d1, d2 being Element of SCM-Data-Loc , k1, k2 being Integer such that
A3:
I = [9,{},<*d1,d2,k1,k2*>]
by A1, A2;
reconsider a = d1, b = d2 as Int_position by AMI_2:def 16;
take
a
; ex b being Int_position ex k1, k2 being Integer st I = AddTo (a,k1,b,k2)
take
b
; ex k1, k2 being Integer st I = AddTo (a,k1,b,k2)
take
k1
; ex k2 being Integer st I = AddTo (a,k1,b,k2)
take
k2
; I = AddTo (a,k1,b,k2)
thus
I = AddTo (a,k1,b,k2)
by A3; verum