let I be set ; :: thesis:
thus ( not I is Instruction of SCM or I = [0 ,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex loc being Instruction-Location of SCM st I = goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a =0_goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a >0_goto loc ) :: thesis:

assume I is Instruction of SCM ; :: thesis:
then ( I in ({[SCM-Halt ,{} ]} \/ { [Y,<*a3*>] where Y is Element of Segm 9, a3 is Element of NAT : Y = 6 } ) \/ { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or I in { [T,<*c2,c3*>] where T is Element of Segm 9, c2, c3 is Element of SCM-Data-Loc : T in {1,2,3,4,5} } ) by XBOOLE_0:def 3;
then A1: ( I in {[SCM-Halt ,{} ]} \/ { [Y,<*a3*>] where Y is Element of Segm 9, a3 is Element of NAT : Y = 6 } or I in { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or I in { [T,<*c2,c3*>] where T is Element of Segm 9, c2, c3 is Element of SCM-Data-Loc : T in {1,2,3,4,5} } ) by XBOOLE_0:def 3;

per cases by A1, XBOOLE_0:def 3;

suppose I in {[SCM-Halt ,{} ]} ; :: thesis:

hence ( I = [0 ,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex loc being Instruction-Location of SCM st I = goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a =0_goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a >0_goto loc ) by TARSKI:def 1; :: thesis:

end;

suppose I in { [Y,<*a3*>] where Y is Element of Segm 9, a3 is Element of NAT : Y = 6 } ; :: thesis:

then consider Y being Element of Segm 9, a3 being Element of NAT such that
A2: ( I = [Y,<*a3*>] & Y = 6 ) ;
reconsider loc = a3 as Instruction-Location of SCM by AMI_1:def 4;
I = goto loc by A2;
hence ( I = [0 ,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex loc being Instruction-Location of SCM st I = goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a =0_goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a >0_goto loc ) ; :: thesis:

end;

suppose I in { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } ; :: thesis:

then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of SCM-Data-Loc such that
A3: ( I = [K,<*a1,b1*>] & K in {7,8} ) ;
reconsider loc = a1 as Instruction-Location of SCM by AMI_1:def 4;
reconsider a = b1 as Data-Location by Def2;
( I = a =0_goto loc or I = a >0_goto loc ) by A3, TARSKI:def 2;
hence ( I = [0 ,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex loc being Instruction-Location of SCM st I = goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a =0_goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a >0_goto loc ) ; :: thesis:

end;

suppose I in { [T,<*c2,c3*>] where T is Element of Segm 9, c2, c3 is Element of SCM-Data-Loc : T in {1,2,3,4,5} } ; :: thesis:

then consider T being Element of Segm 9, c2, c3 being Element of SCM-Data-Loc such that
A4: ( I = [T,<*c2,c3*>] & T in {1,2,3,4,5} ) ;
reconsider a = c2, b = c3 as Data-Location by Def2;
( I = a := b or I = AddTo a,b or I = SubFrom a,b or I = MultBy a,b or I = Divide a,b ) by A4, ENUMSET1:def 3;
hence ( I = [0 ,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex loc being Instruction-Location of SCM st I = goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a =0_goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a >0_goto loc ) ; :: thesis:

end;

thus ( ( I = [0 ,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex loc being Instruction-Location of SCM st I = goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a =0_goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a >0_goto loc ) implies I is Instruction of SCM ) by AMI_2:2; :: thesis: