environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, XBOOLE_0, CARD_1, ZFMISC_1, FINSEQ_1, FUNCT_1, RELAT_1, AMI_1, PARTFUN1, XXREAL_0, TARSKI, AMI_2, RECDEF_2, UNIALG_1, AMISTD_2, VALUED_0, COMPOS_0, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, RELAT_1, FUNCT_1, PARTFUN1, VALUED_0, XXREAL_0, MCART_1, DOMAIN_1, FINSEQ_1, FINSEQ_4, RECDEF_2, COMPOS_0;
definitions TARSKI, XBOOLE_0, FINSEQ_1, COMPOS_0;
theorems TARSKI, ENUMSET1, FINSEQ_4, MCART_1, XBOOLE_0, ORDINAL1, NAT_1, DOMAIN_1, FINSEQ_1, FUNCT_7, XTUPLE_0;
schemes ;
registrations XBOOLE_0, ORDINAL1, XREAL_0, FINSEQ_1, RELAT_1, CARD_1, FUNCT_1, COMPOS_0, VALUED_0, XTUPLE_0;
constructors HIDDEN, DOMAIN_1, FINSEQ_4, FINSEQ_2, VALUED_1, COMPOS_0, XTUPLE_0;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE;
equalities TARSKI, COMPOS_0, XTUPLE_0;
expansions TARSKI, COMPOS_0;
definition
func SCM-Instr -> non
empty set equals
(({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 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} } ) \/ { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ;
coherence
(({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 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} } ) \/ { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } is non empty set
;
end;
::
deftheorem defines
SCM-Instr SCM_INST:def 2 :
SCM-Instr = (({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 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} } ) \/ { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ;
theorem Th9:
for
x being
Element of
SCM-Instr holds
( (
x in {[SCM-Halt,{},{}]} &
InsCode x = 0 ) or (
x in { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } &
InsCode x = 6 ) or (
x 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} } & (
InsCode x = 7 or
InsCode x = 8 ) ) or (
x in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } & (
InsCode x = 1 or
InsCode x = 2 or
InsCode x = 3 or
InsCode x = 4 or
InsCode x = 5 ) ) )
Lm1:
for i being Element of SCM-Instr st ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 ) holds
JumpPart i = {}
Lm2:
for i being Element of SCM-Instr st ( InsCode i = 7 or InsCode i = 8 ) holds
dom (JumpPart i) = Seg 1
Lm3:
for i being Element of SCM-Instr st InsCode i = 6 holds
dom (JumpPart i) = Seg 1
Lm4:
for T being InsType of SCM-Instr holds
not not T = 0 & ... & not T = 8
Lm5:
for T being InsType of SCM-Instr st T = 0 holds
JumpParts T = {{}}
Lm6:
for T being InsType of SCM-Instr st not not T = 1 & ... & not T = 5 holds
JumpParts T = {{}}