let I be Instruction of SCM+FSA ; :: thesis: ( InsCode I = 0 implies I = [0 ,{} ] )
assume A1:
InsCode I = 0
; :: thesis: I = [0 ,{} ]
now assume
I in { [K,<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} }
;
:: thesis: contradictionthen consider K being
Element of
Segm 13,
dC being
Element of
SCM+FSA-Data-Loc ,
fB being
Element of
SCM+FSA-Data*-Loc such that A2:
I = [K,<*dC,fB*>]
and A3:
K in {11,12}
;
(
K = 12 or
K = 11 )
by A3, TARSKI:def 2;
hence
contradiction
by A1, A2, MCART_1:7;
:: thesis: verum end;
then A4:
I in SCM-Instr \/ { [L,<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} }
by XBOOLE_0:def 3;
now assume
I in { [L,<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} }
;
:: thesis: contradictionthen consider L being
Element of
Segm 13,
dB,
dA being
Element of
SCM+FSA-Data-Loc ,
fA being
Element of
SCM+FSA-Data*-Loc such that A5:
I = [L,<*dB,fA,dA*>]
and A6:
L in {9,10}
;
(
L = 9 or
L = 10 )
by A6, TARSKI:def 2;
hence
contradiction
by A1, A5, MCART_1:7;
:: thesis: verum end;
then A7:
I in SCM-Instr
by A4, XBOOLE_0:def 3;
now assume
I in { [R,<*DA,DC*>] where R is Element of Segm 9, DA, DC is Element of SCM-Data-Loc : R in {1,2,3,4,5} }
;
:: thesis: contradictionthen consider R being
Element of
Segm 9,
DA,
DC being
Element of
SCM-Data-Loc such that A8:
I = [R,<*DA,DC*>]
and A9:
R in {1,2,3,4,5}
;
(
R = 1 or
R = 2 or
R = 3 or
R = 4 or
R = 5 )
by A9, ENUMSET1:def 3;
hence
contradiction
by A1, A8, MCART_1:7;
:: thesis: verum end;
then A10:
I in ({[SCM-Halt ,{} ]} \/ { [O,<*LA*>] where O is Element of Segm 9, LA is Element of NAT : O = 6 } ) \/ { [P,<*LB,DB*>] where P is Element of Segm 9, LB is Element of NAT , DB is Element of SCM-Data-Loc : P in {7,8} }
by A7, XBOOLE_0:def 3;
now assume
I in { [P,<*LB,DB*>] where P is Element of Segm 9, LB is Element of NAT , DB is Element of SCM-Data-Loc : P in {7,8} }
;
:: thesis: contradictionthen consider P being
Element of
Segm 9,
LB being
Element of
NAT ,
DB being
Element of
SCM-Data-Loc such that A11:
I = [P,<*LB,DB*>]
and A12:
P in {7,8}
;
(
P = 7 or
P = 8 )
by A12, TARSKI:def 2;
hence
contradiction
by A1, A11, MCART_1:7;
:: thesis: verum end;
then A13:
I in {[SCM-Halt ,{} ]} \/ { [O,<*LA*>] where O is Element of Segm 9, LA is Element of NAT : O = 6 }
by A10, XBOOLE_0:def 3;
then
I in {[SCM-Halt ,{} ]}
by A13, XBOOLE_0:def 3;
hence
I = [0 ,{} ]
by TARSKI:def 1; :: thesis: verum