let I be set ; ( I is Instruction of SCM iff ( 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 Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) )
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 Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc )
( ( 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 Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) implies I is Instruction of SCM )proof
assume
I is
Instruction of
SCM
;
( 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 Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc )
then
(
I in ({[SCM-Halt,{},{}]} \/ { [Y,<*a3*>,{}] where Y is Element of Segm 9, a3 is Nat : Y = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is 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 Nat : Y = 6 } or
I in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is 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
( I in {[SCM-Halt,{},{}]} or I in { [Y,<*a3*>,{}] where Y is Element of Segm 9, a3 is Nat : Y = 6 } or I in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is 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 A1, XBOOLE_0:def 3;
suppose
I in {[SCM-Halt,{},{}]}
;
( 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 Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc )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
Nat st
I = SCM-goto loc or ex
a being
Data-Location ex
loc being
Nat st
I = a =0_goto loc or ex
a being
Data-Location ex
loc being
Nat st
I = a >0_goto loc )
by TARSKI:def 1;
verum end; suppose
I in { [Y,<*a3*>,{}] where Y is Element of Segm 9, a3 is Nat : Y = 6 }
;
( 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 Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc )then consider Y being
Element of
Segm 9,
a3 being
Nat such that A2:
(
I = [Y,<*a3*>,{}] &
Y = 6 )
;
I = SCM-goto a3
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
Nat st
I = SCM-goto loc or ex
a being
Data-Location ex
loc being
Nat st
I = a =0_goto loc or ex
a being
Data-Location ex
loc being
Nat st
I = a >0_goto loc )
;
verum end; suppose
I in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} }
;
( 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 Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc )then consider K being
Element of
Segm 9,
a1 being
Nat,
b1 being
Element of
SCM-Data-Loc such that A3:
(
I = [K,<*a1*>,<*b1*>] &
K in {7,8} )
;
reconsider a =
b1 as
Data-Location by AMI_2:def 16;
reconsider loc =
a1 as
Nat ;
(
I = a =0_goto a1 or
I = a >0_goto a1 )
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
Nat st
I = SCM-goto loc or ex
a being
Data-Location ex
loc being
Nat st
I = a =0_goto loc or ex
a being
Data-Location ex
loc being
Nat st
I = a >0_goto loc )
;
verum 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} }
;
( 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 Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc )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 AMI_2:def 16;
(
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
Nat st
I = SCM-goto loc or ex
a being
Data-Location ex
loc being
Nat st
I = a =0_goto loc or ex
a being
Data-Location ex
loc being
Nat st
I = a >0_goto loc )
;
verum end;
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 Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) implies I is Instruction of SCM )
by SCM_INST:1; verum