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 Element of NAT : Y = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of 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 Element of NAT : Y = 6 } or
I in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of 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 Element of NAT : Y = 6 } or I in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of 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 Element of 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
Element of
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 Element of 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
Element of
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 Def2;
reconsider loc =
a1 as
Element of
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 Def2;
(
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 AMI_2:2; verum