let I be set ; :: thesis: ( not I is Instruction of SCMPDS or ex k1 being Integer st I = goto k1 or ex a being Int_position st I = return a or ex a being Int_position ex k1 being Integer st I = saveIC a,k1 or ex a being Int_position ex k1 being Integer st I = a := k1 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 := k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = MultBy a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = Divide a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = a,k1 := b,k2 )
assume I is Instruction of SCMPDS ; :: thesis: ( ex k1 being Integer st I = goto k1 or ex a being Int_position st I = return a or ex a being Int_position ex k1 being Integer st I = saveIC a,k1 or ex a being Int_position ex k1 being Integer st I = a := k1 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 := k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = MultBy a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = Divide a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = a,k1 := b,k2 )
then reconsider I = I as Instruction of SCMPDS ;

per cases ( I in { [0 ,{} ,<*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 14, 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 14, 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 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;

suppose I in { [0 ,{} ,<*k1*>] where k1 is Element of INT : verum } ; :: thesis: ( ex k1 being Integer st I = goto k1 or ex a being Int_position st I = return a or ex a being Int_position ex k1 being Integer st I = saveIC a,k1 or ex a being Int_position ex k1 being Integer st I = a := k1 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 := k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = MultBy a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = Divide a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = a,k1 := b,k2 )

then consider k1 being Element of INT such that
A1: I = [0 ,{} ,<*k1*>] ;
I = goto k1 by A1;
hence ( ex k1 being Integer st I = goto k1 or ex a being Int_position st I = return a or ex a being Int_position ex k1 being Integer st I = saveIC a,k1 or ex a being Int_position ex k1 being Integer st I = a := k1 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 := k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = MultBy a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = Divide a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = a,k1 := b,k2 ) ; :: thesis: verum

end;

suppose I in { [1,{} ,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ; :: thesis: ( ex k1 being Integer st I = goto k1 or ex a being Int_position st I = return a or ex a being Int_position ex k1 being Integer st I = saveIC a,k1 or ex a being Int_position ex k1 being Integer st I = a := k1 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 := k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = MultBy a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = Divide a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = a,k1 := b,k2 )

then consider d1 being Element of SCM-Data-Loc such that
A2: I = [1,{} ,<*d1*>] ;
reconsider a = d1 as Int_position by Def2;
I = return a by A2;
hence ( ex k1 being Integer st I = goto k1 or ex a being Int_position st I = return a or ex a being Int_position ex k1 being Integer st I = saveIC a,k1 or ex a being Int_position ex k1 being Integer st I = a := k1 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 := k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = MultBy a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = Divide a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = a,k1 := b,k2 ) ; :: thesis: verum

end;

suppose I in { [I1,{} ,<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } ; :: thesis: ( ex k1 being Integer st I = goto k1 or ex a being Int_position st I = return a or ex a being Int_position ex k1 being Integer st I = saveIC a,k1 or ex a being Int_position ex k1 being Integer st I = a := k1 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 := k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = MultBy a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = Divide a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = a,k1 := b,k2 )

then consider I2 being Element of Segm 14, d2 being Element of SCM-Data-Loc , k2 being Element of INT such that
A3: ( I = [I2,{} ,<*d2,k2*>] & I2 in {2,3} ) ;
reconsider a = d2 as Int_position by Def2;
( I = saveIC a,k2 or I = a := k2 ) by A3, TARSKI:def 2;
hence ( ex k1 being Integer st I = goto k1 or ex a being Int_position st I = return a or ex a being Int_position ex k1 being Integer st I = saveIC a,k1 or ex a being Int_position ex k1 being Integer st I = a := k1 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 := k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = MultBy a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = Divide a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = a,k1 := b,k2 ) ; :: thesis: verum

end;

suppose I in { [I2,{} ,<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } ; :: thesis: ( ex k1 being Integer st I = goto k1 or ex a being Int_position st I = return a or ex a being Int_position ex k1 being Integer st I = saveIC a,k1 or ex a being Int_position ex k1 being Integer st I = a := k1 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 := k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = MultBy a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = Divide a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = a,k1 := b,k2 )

then consider I3 being Element of Segm 14, d3 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A4: ( I = [I3,{} ,<*d3,k1,k2*>] & I3 in {4,5,6,7,8} ) ;
reconsider a = d3 as Int_position by Def2;
( I = a,k1 <>0_goto k2 or I = a,k1 <=0_goto k2 or I = a,k1 >=0_goto k2 or I = a,k1 := k2 or I = AddTo a,k1,k2 ) by A4, ENUMSET1:def 3;
hence ( ex k1 being Integer st I = goto k1 or ex a being Int_position st I = return a or ex a being Int_position ex k1 being Integer st I = saveIC a,k1 or ex a being Int_position ex k1 being Integer st I = a := k1 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 := k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = MultBy a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = Divide a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = a,k1 := b,k2 ) ; :: thesis: verum

end;

suppose I in { [I3,{} ,<*d4,d5,k5,k6*>] where I3 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ; :: thesis: ( ex k1 being Integer st I = goto k1 or ex a being Int_position st I = return a or ex a being Int_position ex k1 being Integer st I = saveIC a,k1 or ex a being Int_position ex k1 being Integer st I = a := k1 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 := k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = MultBy a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = Divide a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = a,k1 := b,k2 )

then consider I3 being Element of Segm 14, d4, d5 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A5: ( I = [I3,{} ,<*d4,d5,k1,k2*>] & I3 in {9,10,11,12,13} ) ;
reconsider a = d4, b = d5 as Int_position by Def2;
( I = AddTo a,k1,b,k2 or I = SubFrom a,k1,b,k2 or I = MultBy a,k1,b,k2 or I = Divide a,k1,b,k2 or I = a,k1 := b,k2 ) by A5, ENUMSET1:def 3;
hence ( ex k1 being Integer st I = goto k1 or ex a being Int_position st I = return a or ex a being Int_position ex k1 being Integer st I = saveIC a,k1 or ex a being Int_position ex k1 being Integer st I = a := k1 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 := k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = a,k1 >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = MultBy a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = Divide a,k1,b,k2 or ex a, b being Int_position ex k1, k2 being Integer st I = a,k1 := b,k2 ) ; :: thesis: verum

end;

end;