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) )

( 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

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 A1, SCMRINGI:6; :: thesis: verum
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 (({[0,{},{}]} \/ { [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 A1, AMI_3:27, XBOOLE_0:def 3;

then ( J in ({[0,{},{}]} \/ { [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 {[0,{},{}]} \/ { [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;

end;then ( J in (({[0,{},{}]} \/ { [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 A1, AMI_3:27, XBOOLE_0:def 3;

then ( J in ({[0,{},{}]} \/ { [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 {[0,{},{}]} \/ { [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 {[0,{},{}]} 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 A2, XBOOLE_0:def 3;

end;

suppose
J in {[0,{},{}]}
; :: 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;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

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 Th1, AMI_3:27;

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;A4: J = [7,<*i*>,<*a*>] and

verum ;

reconsider A = a as Data-Location of R by Th1, AMI_3:27;

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

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 Th1, AMI_3:27;

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;A5: J = [5,{},<*a,r*>] and

verum ;

reconsider A = a as Data-Location of R by Th1, AMI_3:27;

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

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 Th1, AMI_3:27;

( J = A := B or J = AddTo (A,B) or J = SubFrom (A,B) or J = MultBy (A,B) ) by A6, ENUMSET1:def 2;

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;A6: ( J = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;

reconsider A = a, B = b as Data-Location of R by Th1, AMI_3:27;

( J = A := B or J = AddTo (A,B) or J = SubFrom (A,B) or J = MultBy (A,B) ) by A6, ENUMSET1:def 2;

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