thus ( not SCMPDS is empty & SCMPDS is stored-program ) by COMPOS_1:def 2, STRUCT_0:def 1; :: thesis: SCMPDS is standard-ins
consider X being non empty set such that
WW: proj2 SCMPDS-Instr c= X * by FINSEQ_1:106;
take X ; :: according to COMPOS_1:def 17 :: thesis: the Instructions of SCMPDS c= [:K97(),(K97() * ),(X * ):]
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the Instructions of SCMPDS or x in [:K97(),(K97() * ),(X * ):] )
assume Z: x in the Instructions of SCMPDS ; :: thesis: x in [:K97(),(K97() * ),(X * ):]
X: {} in NAT * by FINSEQ_1:66;

per cases ( x in (({ [0 ,{} ,<*l*>] where l is Element of INT : verum } \/ { [1,{} ,<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{} ,<*v,c*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{} ,<*v,c1,c2*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or x in { [I,{} ,<*v1,v2,c1,c2*>] where I is Element of Segm 14, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by Z, XBOOLE_0:def 3;

suppose S: x in (({ [0 ,{} ,<*l*>] where l is Element of INT : verum } \/ { [1,{} ,<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{} ,<*v,c*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{} ,<*v,c1,c2*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ; :: thesis: x in [:K97(),(K97() * ),(X * ):]

per cases ( x in ({ [0 ,{} ,<*l*>] where l is Element of INT : verum } \/ { [1,{} ,<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{} ,<*v,c*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or x in { [I,{} ,<*v,c1,c2*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) by S, XBOOLE_0:def 3;

suppose S: x in ({ [0 ,{} ,<*l*>] where l is Element of INT : verum } \/ { [1,{} ,<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{} ,<*v,c*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ; :: thesis: x in [:K97(),(K97() * ),(X * ):]

per cases ( x in { [0 ,{} ,<*l*>] where l is Element of INT : verum } \/ { [1,{} ,<*sp*>] where sp is Element of SCM-Data-Loc : verum } or x in { [I,{} ,<*v,c*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) by S, XBOOLE_0:def 3;

suppose S: x in { [0 ,{} ,<*l*>] where l is Element of INT : verum } \/ { [1,{} ,<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; :: thesis: x in [:K97(),(K97() * ),(X * ):]

per cases ( x in { [0 ,{} ,<*l*>] where l is Element of INT : verum } or x in { [1,{} ,<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) by S, XBOOLE_0:def 3;

suppose x in { [0 ,{} ,<*l*>] where l is Element of INT : verum } ; :: thesis: x in [:K97(),(K97() * ),(X * ):]

then consider l being Element of INT such that
W: x = [0 ,{} ,<*l*>] ;
<*l*> in proj2 SCMPDS-Instr by Z, W, RELAT_1:def 5;
then <*l*> in X * by WW;
hence x in [:NAT ,(NAT * ),(X * ):] by W, X, MCART_1:73; :: thesis: verum

end;

suppose x in { [1,{} ,<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; :: thesis: x in [:K97(),(K97() * ),(X * ):]

then consider sp being Element of SCM-Data-Loc such that
W: x = [1,{} ,<*sp*>] ;
<*sp*> in proj2 SCMPDS-Instr by Z, W, RELAT_1:def 5;
then <*sp*> in X * by WW;
hence x in [:NAT ,(NAT * ),(X * ):] by W, X, MCART_1:73; :: thesis: verum

end;

end;

end;

suppose x in { [I,{} ,<*v,c*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ; :: thesis: x in [:K97(),(K97() * ),(X * ):]

then consider I being Element of Segm 14, v being Element of SCM-Data-Loc , c being Element of INT such that
W: ( x = [I,{} ,<*v,c*>] & I in {2,3} ) ;
<*v,c*> in proj2 SCMPDS-Instr by Z, W, RELAT_1:def 5;
then <*v,c*> in X * by WW;
hence x in [:NAT ,(NAT * ),(X * ):] by W, X, MCART_1:73; :: thesis: verum

end;

end;

end;

suppose x in { [I,{} ,<*v,c1,c2*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ; :: thesis: x in [:K97(),(K97() * ),(X * ):]

then consider I being Element of Segm 14, v being Element of SCM-Data-Loc , c1, c2 being Element of INT such that
W: ( x = [I,{} ,<*v,c1,c2*>] & I in {4,5,6,7,8} ) ;
<*v,c1,c2*> in proj2 SCMPDS-Instr by Z, W, RELAT_1:def 5;
then <*v,c1,c2*> in X * by WW;
hence x in [:NAT ,(NAT * ),(X * ):] by W, X, MCART_1:73; :: thesis: verum

end;

end;

end;

suppose x in { [I,{} ,<*v1,v2,c1,c2*>] where I is Element of Segm 14, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ; :: thesis: x in [:K97(),(K97() * ),(X * ):]

then consider I being Element of Segm 14, v1, v2 being Element of SCM-Data-Loc , c1, c2 being Element of INT such that
W: ( x = [I,{} ,<*v1,v2,c1,c2*>] & I in {9,10,11,12,13} ) ;
<*v1,v2,c1,c2*> in proj2 SCMPDS-Instr by Z, W, RELAT_1:def 5;
then <*v1,v2,c1,c2*> in X * by WW;
hence x in [:NAT ,(NAT * ),(X * ):] by W, X, MCART_1:73; :: thesis: verum

end;

end;