let R be Ring; :: thesis: for I being set holds
( I is Instruction of (SCM R) iff ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Nat st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) )

let J be set ; :: thesis: ( J is Instruction of (SCM R) iff ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) )
A1: the InstructionsF of (SCM R) = SCM-Instr R by Def1;
thus ( not J is Instruction of (SCM R) or J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) :: thesis: ( ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) implies J is Instruction of (SCM R) )
proof
assume J is Instruction of (SCM R) ; :: thesis: ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r )
then ( J in (( \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of Data-Locations : verum } or J in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ) by ;
then ( J in ( \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } or J in { [7,<*i*>,<*a*>] where i is Nat, a is Element of Data-Locations : verum } or J in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ) by XBOOLE_0:def 3;
then A2: ( J in \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } or J in { [6,<*i*>,{}] where i is Nat : verum } or J in { [7,<*i*>,<*a*>] where i is Nat, a is Element of Data-Locations : verum } or J in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ) by XBOOLE_0:def 3;
per cases ( J in or J in { [6,<*i*>,{}] where i is Nat : verum } or J in { [7,<*i*>,<*a*>] where i is Nat, a is Element of Data-Locations : verum } or J in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } or J in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } ) by ;
suppose J in ; :: thesis: ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r )
hence ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) by TARSKI:def 1; :: thesis: verum
end;
suppose J in { [6,<*i*>,{}] where i is Nat : verum } ; :: thesis: ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r )
then consider i being Nat such that
A3: J = [6,<*i*>,{}] and
verum ;
J = goto (i,R) by A3;
hence ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) ; :: thesis: verum
end;
suppose J in { [7,<*i*>,<*a*>] where i is Nat, a is Element of Data-Locations : verum } ; :: thesis: ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r )
then consider i being Nat, a being Element of Data-Locations such that
A4: J = [7,<*i*>,<*a*>] and
verum ;
reconsider A = a as
Data-Location of R by ;
J = A =0_goto i by A4;
hence ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) ; :: thesis: verum
end;
suppose J in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ; :: thesis: ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r )
then consider a being Element of Data-Locations , r being Element of R such that
A5: J = [5,{},<*a,r*>] and
verum ;
reconsider A = a as
Data-Location of R by ;
J = A := r by A5;
hence ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) ; :: thesis: verum
end;
suppose J in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } ; :: thesis: ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r )
then consider I being Element of Segm 8, a, b being Element of Data-Locations such that
A6: ( J = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;
reconsider A = a, B = b as Data-Location of R by ;
( J = A := B or J = AddTo (A,B) or J = SubFrom (A,B) or J = MultBy (A,B) ) by ;
hence ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) ; :: thesis: verum
end;
end;
end;
thus ( ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) implies J is Instruction of (SCM R) ) by ; :: thesis: verum