:: SCM_INST semantic presentation
begin
notation
synonym SCM-Halt for {} ;
end;
definition
:: original: SCM-Halt
redefine func SCM-Halt -> Element of Segm 9;
correctness
coherence
SCM-Halt is Element of Segm 9;
by NAT_1:44;
end;
definition
func SCM-Data-Loc -> set equals :: SCM_INST:def 1
[:{1},NAT:];
coherence
[:{1},NAT:] is set ;
end;
:: deftheorem defines SCM-Data-Loc SCM_INST:def_1_:_
SCM-Data-Loc = [:{1},NAT:];
registration
cluster SCM-Data-Loc -> non empty ;
coherence
not SCM-Data-Loc is empty ;
end;
definition
func SCM-Instr -> non empty set equals :: SCM_INST:def 2
(({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 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} } ) \/ { [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 Element of NAT : J = 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} } ) \/ { [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 Element of NAT : J = 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} } ) \/ { [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 Th1: :: SCM_INST:1
[0,{},{}] in SCM-Instr
proof
[0,{},{}] in {[SCM-Halt,{},{}]} by TARSKI:def_1;
then [0,{},{}] in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } by XBOOLE_0:def_3;
then [0,{},{}] in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 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} } by XBOOLE_0:def_3;
hence [0,{},{}] in SCM-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;
registration
cluster SCM-Instr -> non empty ;
coherence
not SCM-Instr is empty ;
end;
theorem Th2: :: SCM_INST:2
for a2 being Element of NAT holds [6,<*a2*>,{}] in SCM-Instr
proof
let a2 be Element of NAT ; ::_thesis: [6,<*a2*>,{}] in SCM-Instr
reconsider x = 6 as Element of Segm 9 by NAT_1:44;
[x,<*a2*>,{}] in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ;
then [x,<*a2*>,{}] in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } by XBOOLE_0:def_3;
then [x,<*a2*>,{}] in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 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} } by XBOOLE_0:def_3;
hence [6,<*a2*>,{}] in SCM-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th3: :: SCM_INST:3
for x being set
for a2 being Element of NAT
for b2 being Element of SCM-Data-Loc st x in {7,8} holds
[x,<*a2*>,<*b2*>] in SCM-Instr
proof
let x be set ; ::_thesis: for a2 being Element of NAT
for b2 being Element of SCM-Data-Loc st x in {7,8} holds
[x,<*a2*>,<*b2*>] in SCM-Instr
let a2 be Element of NAT ; ::_thesis: for b2 being Element of SCM-Data-Loc st x in {7,8} holds
[x,<*a2*>,<*b2*>] in SCM-Instr
let b2 be Element of SCM-Data-Loc ; ::_thesis: ( x in {7,8} implies [x,<*a2*>,<*b2*>] in SCM-Instr )
assume A1: x in {7,8} ; ::_thesis: [x,<*a2*>,<*b2*>] in SCM-Instr
then ( x = 7 or x = 8 ) by TARSKI:def_2;
then reconsider x = x as Element of Segm 9 by NAT_1:44;
[x,<*a2*>,<*b2*>] 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} } by A1;
then [x,<*a2*>,<*b2*>] in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 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} } by XBOOLE_0:def_3;
hence [x,<*a2*>,<*b2*>] in SCM-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th4: :: SCM_INST:4
for x being set
for b1, c1 being Element of SCM-Data-Loc st x in {1,2,3,4,5} holds
[x,{},<*b1,c1*>] in SCM-Instr
proof
let x be set ; ::_thesis: for b1, c1 being Element of SCM-Data-Loc st x in {1,2,3,4,5} holds
[x,{},<*b1,c1*>] in SCM-Instr
let b1, c1 be Element of SCM-Data-Loc ; ::_thesis: ( x in {1,2,3,4,5} implies [x,{},<*b1,c1*>] in SCM-Instr )
assume A1: x in {1,2,3,4,5} ; ::_thesis: [x,{},<*b1,c1*>] in SCM-Instr
then ( x = 1 or x = 2 or x = 3 or x = 4 or x = 5 ) by ENUMSET1:def_3;
then reconsider x = x as Element of Segm 9 by NAT_1:44;
[x,{},<*b1,c1*>] in { [J,{},<*b,c*>] where J is Element of Segm 9, b, c is Element of SCM-Data-Loc : J in {1,2,3,4,5} } by A1;
hence [x,{},<*b1,c1*>] in SCM-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;
definition
let x be Element of SCM-Instr ;
given mk, ml being Element of SCM-Data-Loc , I being Element of Segm 9 such that A1: x = [I,{},<*mk,ml*>] ;
funcx address_1 -> Element of SCM-Data-Loc means :Def3: :: SCM_INST:def 3
ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b1 = f /. 1 )
proof
take mk ; ::_thesis: ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & mk = f /. 1 )
take <*mk,ml*> ; ::_thesis: ( <*mk,ml*> = x `3_3 & mk = <*mk,ml*> /. 1 )
thus ( <*mk,ml*> = x `3_3 & mk = <*mk,ml*> /. 1 ) by A1, FINSEQ_4:17, RECDEF_2:def_3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b2 = f /. 1 ) holds
b1 = b2 ;
funcx address_2 -> Element of SCM-Data-Loc means :Def4: :: SCM_INST:def 4
ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & it = f /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b1 = f /. 2 )
proof
take ml ; ::_thesis: ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & ml = f /. 2 )
take <*mk,ml*> ; ::_thesis: ( <*mk,ml*> = x `3_3 & ml = <*mk,ml*> /. 2 )
thus ( <*mk,ml*> = x `3_3 & ml = <*mk,ml*> /. 2 ) by A1, FINSEQ_4:17, RECDEF_2:def_3; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b2 = f /. 2 ) holds
b1 = b2;
;
end;
:: deftheorem Def3 defines address_1 SCM_INST:def_3_:_
for x being Element of SCM-Instr st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,{},<*mk,ml*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x address_1 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b2 = f /. 1 ) );
:: deftheorem Def4 defines address_2 SCM_INST:def_4_:_
for x being Element of SCM-Instr st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,{},<*mk,ml*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x address_2 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b2 = f /. 2 ) );
theorem :: SCM_INST:5
for x being Element of SCM-Instr
for mk, ml being Element of SCM-Data-Loc
for I being Element of Segm 9 st x = [I,{},<*mk,ml*>] holds
( x address_1 = mk & x address_2 = ml )
proof
let x be Element of SCM-Instr ; ::_thesis: for mk, ml being Element of SCM-Data-Loc
for I being Element of Segm 9 st x = [I,{},<*mk,ml*>] holds
( x address_1 = mk & x address_2 = ml )
let mk, ml be Element of SCM-Data-Loc ; ::_thesis: for I being Element of Segm 9 st x = [I,{},<*mk,ml*>] holds
( x address_1 = mk & x address_2 = ml )
let I be Element of Segm 9; ::_thesis: ( x = [I,{},<*mk,ml*>] implies ( x address_1 = mk & x address_2 = ml ) )
assume A1: x = [I,{},<*mk,ml*>] ; ::_thesis: ( x address_1 = mk & x address_2 = ml )
then consider f being FinSequence of SCM-Data-Loc such that
A2: f = x `3_3 and
A3: x address_1 = f /. 1 by Def3;
f = <*mk,ml*> by A1, A2, RECDEF_2:def_3;
hence x address_1 = mk by A3, FINSEQ_4:17; ::_thesis: x address_2 = ml
consider f being FinSequence of SCM-Data-Loc such that
A4: f = x `3_3 and
A5: x address_2 = f /. 2 by A1, Def4;
f = <*mk,ml*> by A1, A4, RECDEF_2:def_3;
hence x address_2 = ml by A5, FINSEQ_4:17; ::_thesis: verum
end;
definition
let x be Element of SCM-Instr ;
given mk being Element of NAT , I being Element of Segm 9 such that A1: x = [I,<*mk*>,{}] ;
funcx jump_address -> Element of NAT means :Def5: :: SCM_INST:def 5
ex f being FinSequence of NAT st
( f = x `2_3 & it = f /. 1 );
existence
ex b1 being Element of NAT ex f being FinSequence of NAT st
( f = x `2_3 & b1 = f /. 1 )
proof
take mk ; ::_thesis: ex f being FinSequence of NAT st
( f = x `2_3 & mk = f /. 1 )
take <*mk*> ; ::_thesis: ( <*mk*> = x `2_3 & mk = <*mk*> /. 1 )
thus ( <*mk*> = x `2_3 & mk = <*mk*> /. 1 ) by A1, FINSEQ_4:16, RECDEF_2:def_2; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Element of NAT st ex f being FinSequence of NAT st
( f = x `2_3 & b1 = f /. 1 ) & ex f being FinSequence of NAT st
( f = x `2_3 & b2 = f /. 1 ) holds
b1 = b2;
;
end;
:: deftheorem Def5 defines jump_address SCM_INST:def_5_:_
for x being Element of SCM-Instr st ex mk being Element of NAT ex I being Element of Segm 9 st x = [I,<*mk*>,{}] holds
for b2 being Element of NAT holds
( b2 = x jump_address iff ex f being FinSequence of NAT st
( f = x `2_3 & b2 = f /. 1 ) );
theorem :: SCM_INST:6
for x being Element of SCM-Instr
for mk being Element of NAT
for I being Element of Segm 9 st x = [I,<*mk*>,{}] holds
x jump_address = mk
proof
let x be Element of SCM-Instr ; ::_thesis: for mk being Element of NAT
for I being Element of Segm 9 st x = [I,<*mk*>,{}] holds
x jump_address = mk
let mk be Element of NAT ; ::_thesis: for I being Element of Segm 9 st x = [I,<*mk*>,{}] holds
x jump_address = mk
let I be Element of Segm 9; ::_thesis: ( x = [I,<*mk*>,{}] implies x jump_address = mk )
assume A1: x = [I,<*mk*>,{}] ; ::_thesis: x jump_address = mk
then consider f being FinSequence of NAT such that
A2: f = x `2_3 and
A3: x jump_address = f /. 1 by Def5;
f = <*mk*> by A1, A2, RECDEF_2:def_2;
hence x jump_address = mk by A3, FINSEQ_4:16; ::_thesis: verum
end;
definition
let x be Element of SCM-Instr ;
given mk being Element of NAT , ml being Element of SCM-Data-Loc , I being Element of Segm 9 such that A1: x = [I,<*mk*>,<*ml*>] ;
funcx cjump_address -> Element of NAT means :Def6: :: SCM_INST:def 6
ex mk being Element of NAT st
( <*mk*> = x `2_3 & it = <*mk*> /. 1 );
existence
ex b1, mk being Element of NAT st
( <*mk*> = x `2_3 & b1 = <*mk*> /. 1 )
proof
take mk ; ::_thesis: ex mk being Element of NAT st
( <*mk*> = x `2_3 & mk = <*mk*> /. 1 )
take mk ; ::_thesis: ( <*mk*> = x `2_3 & mk = <*mk*> /. 1 )
thus ( <*mk*> = x `2_3 & mk = <*mk*> /. 1 ) by A1, FINSEQ_4:16, RECDEF_2:def_2; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Element of NAT st ex mk being Element of NAT st
( <*mk*> = x `2_3 & b1 = <*mk*> /. 1 ) & ex mk being Element of NAT st
( <*mk*> = x `2_3 & b2 = <*mk*> /. 1 ) holds
b1 = b2;
;
funcx cond_address -> Element of SCM-Data-Loc means :Def7: :: SCM_INST:def 7
ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & it = <*ml*> /. 1 );
existence
ex b1, ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b1 = <*ml*> /. 1 )
proof
take ml ; ::_thesis: ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & ml = <*ml*> /. 1 )
take ml ; ::_thesis: ( <*ml*> = x `3_3 & ml = <*ml*> /. 1 )
thus ( <*ml*> = x `3_3 & ml = <*ml*> /. 1 ) by A1, FINSEQ_4:16, RECDEF_2:def_3; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b1 = <*ml*> /. 1 ) & ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b2 = <*ml*> /. 1 ) holds
b1 = b2;
;
end;
:: deftheorem Def6 defines cjump_address SCM_INST:def_6_:_
for x being Element of SCM-Instr st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
for b2 being Element of NAT holds
( b2 = x cjump_address iff ex mk being Element of NAT st
( <*mk*> = x `2_3 & b2 = <*mk*> /. 1 ) );
:: deftheorem Def7 defines cond_address SCM_INST:def_7_:_
for x being Element of SCM-Instr st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x cond_address iff ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b2 = <*ml*> /. 1 ) );
theorem :: SCM_INST:7
for x being Element of SCM-Instr
for mk being Element of NAT
for ml being Element of SCM-Data-Loc
for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )
proof
let x be Element of SCM-Instr ; ::_thesis: for mk being Element of NAT
for ml being Element of SCM-Data-Loc
for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )
let mk be Element of NAT ; ::_thesis: for ml being Element of SCM-Data-Loc
for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )
let ml be Element of SCM-Data-Loc ; ::_thesis: for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )
let I be Element of Segm 9; ::_thesis: ( x = [I,<*mk*>,<*ml*>] implies ( x cjump_address = mk & x cond_address = ml ) )
assume A1: x = [I,<*mk*>,<*ml*>] ; ::_thesis: ( x cjump_address = mk & x cond_address = ml )
then consider mk9 being Element of NAT such that
A2: <*mk9*> = x `2_3 and
A3: x cjump_address = <*mk9*> /. 1 by Def6;
<*mk9*> = <*mk*> by A1, A2, RECDEF_2:def_2;
hence x cjump_address = mk by A3, FINSEQ_4:16; ::_thesis: x cond_address = ml
consider ml9 being Element of SCM-Data-Loc such that
A4: <*ml9*> = x `3_3 and
A5: x cond_address = <*ml9*> /. 1 by A1, Def7;
<*ml9*> = <*ml*> by A1, A4, RECDEF_2:def_3;
hence x cond_address = ml by A5, FINSEQ_4:16; ::_thesis: verum
end;
theorem Th8: :: SCM_INST:8
SCM-Instr c= [:NAT,(NAT *),(proj2 SCM-Instr):]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SCM-Instr or x in [:NAT,(NAT *),(proj2 SCM-Instr):] )
assume A1: x in SCM-Instr ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
percases ( x in ({[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 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 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} } ) by A1, XBOOLE_0:def_3;
supposeA2: x in ({[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 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} } ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
percases ( x in {[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } or x 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} } ) by A2, XBOOLE_0:def_3;
supposeA3: x in {[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
A4: SCM-Halt = 0 ;
percases ( x in {[SCM-Halt,{},{}]} or x in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } ) by A3, XBOOLE_0:def_3;
suppose x in {[SCM-Halt,{},{}]} ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
then A5: x = [SCM-Halt,{},{}] by TARSKI:def_1;
then ( SCM-Halt in NAT & {} in NAT * & {} in proj2 SCM-Instr ) by A1, A4, FINSEQ_1:49, XTUPLE_0:def_13;
hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A5, DOMAIN_1:3; ::_thesis: verum
end;
suppose x in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
then consider J being Element of Segm 9, a being Element of NAT such that
A6: ( x = [J,<*a*>,{}] & J = 6 ) ;
( J in NAT & <*a*> in NAT * & {} in proj2 SCM-Instr ) by A1, A6, FUNCT_7:18, XTUPLE_0:def_13;
hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A6, DOMAIN_1:3; ::_thesis: verum
end;
end;
end;
suppose x 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} } ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of SCM-Data-Loc such that
A7: ( x = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;
( K in NAT & <*a1*> in NAT * & <*b1*> in proj2 SCM-Instr ) by A1, A7, FUNCT_7:18, XTUPLE_0:def_13;
hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A7, DOMAIN_1:3; ::_thesis: verum
end;
end;
end;
suppose 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} } ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
then consider I being Element of Segm 9, b, c being Element of SCM-Data-Loc such that
A8: ( x = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;
( I in NAT & {} in NAT * & <*b,c*> in proj2 SCM-Instr ) by A1, A8, FINSEQ_1:49, XTUPLE_0:def_13;
hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A8, DOMAIN_1:3; ::_thesis: verum
end;
end;
end;
registration
cluster proj2 SCM-Instr -> FinSequence-membered ;
coherence
proj2 SCM-Instr is FinSequence-membered
proof
let f be set ; :: according to FINSEQ_1:def_18 ::_thesis: ( not f in proj2 SCM-Instr or f is set )
assume f in proj2 SCM-Instr ; ::_thesis: f is set
then consider y being set such that
A1: [y,f] in SCM-Instr by XTUPLE_0:def_13;
set x = [y,f];
percases ( [y,f] in ({[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 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 [y,f] 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} } ) by A1, XBOOLE_0:def_3;
supposeA2: [y,f] in ({[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 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} } ; ::_thesis: f is set
percases ( [y,f] in {[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } or [y,f] 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} } ) by A2, XBOOLE_0:def_3;
supposeA3: [y,f] in {[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } ; ::_thesis: f is set
percases ( [y,f] in {[SCM-Halt,{},{}]} or [y,f] in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } ) by A3, XBOOLE_0:def_3;
suppose [y,f] in {[SCM-Halt,{},{}]} ; ::_thesis: f is set
then [y,f] = [SCM-Halt,{},{}] by TARSKI:def_1;
hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum
end;
suppose [y,f] in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } ; ::_thesis: f is set
then ex J being Element of Segm 9 ex a being Element of NAT st
( [y,f] = [J,<*a*>,{}] & J = 6 ) ;
hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
suppose [y,f] 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} } ; ::_thesis: f is set
then ex K being Element of Segm 9 ex a1 being Element of NAT ex b1 being Element of SCM-Data-Loc st
( [y,f] = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;
hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
suppose [y,f] 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} } ; ::_thesis: f is set
then ex I being Element of Segm 9 ex b, c being Element of SCM-Data-Loc st
( [y,f] = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;
hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
end;
theorem Th9: :: SCM_INST:9
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 Element of NAT : J = 6 } & InsCode x = 6 ) or ( x 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} } & ( 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 ) ) )
proof
let x be Element of SCM-Instr ; ::_thesis: ( ( x in {[SCM-Halt,{},{}]} & InsCode x = 0 ) or ( x in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } & InsCode x = 6 ) or ( x 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} } & ( 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 ) ) )
( x in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 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 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} } ) by XBOOLE_0:def_3;
then ( x in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } or x 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 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} } ) by XBOOLE_0:def_3;
percasesthen ( x in {[SCM-Halt,{},{}]} or x in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } or x 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 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} } ) by XBOOLE_0:def_3;
case x in {[SCM-Halt,{},{}]} ; ::_thesis: InsCode x = 0
then x = [SCM-Halt,{},{}] by TARSKI:def_1;
hence InsCode x = 0 by RECDEF_2:def_1; ::_thesis: verum
end;
case x in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ; ::_thesis: InsCode x = 6
then ex J being Element of Segm 9 ex a being Element of NAT st
( x = [J,<*a*>,{}] & J = 6 ) ;
hence InsCode x = 6 by RECDEF_2:def_1; ::_thesis: verum
end;
case x 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} } ; ::_thesis: ( InsCode x = 7 or InsCode x = 8 )
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of SCM-Data-Loc such that
A1: x = [K,<*a1*>,<*b1*>] and
A2: K in {7,8} ;
InsCode x = K by A1, RECDEF_2:def_1;
hence ( InsCode x = 7 or InsCode x = 8 ) by A2, TARSKI:def_2; ::_thesis: verum
end;
case 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} } ; ::_thesis: ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 )
then consider I being Element of Segm 9, b, c being Element of SCM-Data-Loc such that
A3: x = [I,{},<*b,c*>] and
A4: I in {1,2,3,4,5} ;
InsCode x = I by A3, RECDEF_2:def_1;
hence ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 ) by A4, ENUMSET1:def_3; ::_thesis: verum
end;
end;
end;
begin
registration
cluster SCM-Instr -> non empty standard-ins ;
coherence
SCM-Instr is standard-ins
proof
consider X being non empty set such that
A1: proj2 SCM-Instr c= X * by FINSEQ_1:85;
take X ; :: according to COMPOS_0:def_1 ::_thesis: SCM-Instr c= [:NAT,(NAT *),(X *):]
A2: SCM-Instr c= [:NAT,(NAT *),(proj2 SCM-Instr):] by Th8;
[:NAT,(NAT *),(proj2 SCM-Instr):] c= [:NAT,(NAT *),(X *):] by A1, MCART_1:73;
hence SCM-Instr c= [:NAT,(NAT *),(X *):] by A2, XBOOLE_1:1; ::_thesis: verum
end;
end;
theorem Th10: :: SCM_INST:10
for l being Element of SCM-Instr holds InsCode l <= 8
proof
let l be Element of SCM-Instr ; ::_thesis: InsCode l <= 8
( InsCode l = 0 or InsCode l = 1 or InsCode l = 2 or InsCode l = 3 or InsCode l = 4 or InsCode l = 5 or InsCode l = 6 or InsCode l = 7 or InsCode l = 8 ) by Th9;
hence InsCode l <= 8 ; ::_thesis: verum
end;
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 = {}
proof
let i be Element of SCM-Instr ; ::_thesis: ( ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 ) implies JumpPart i = {} )
assume ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 ) ; ::_thesis: JumpPart i = {}
then i 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} } by Th9;
then ex I being Element of Segm 9 ex b, c being Element of SCM-Data-Loc st
( i = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;
hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum
end;
Lm2: for i being Element of SCM-Instr st ( InsCode i = 7 or InsCode i = 8 ) holds
dom (JumpPart i) = Seg 1
proof
let i be Element of SCM-Instr ; ::_thesis: ( ( InsCode i = 7 or InsCode i = 8 ) implies dom (JumpPart i) = Seg 1 )
assume ( InsCode i = 7 or InsCode i = 8 ) ; ::_thesis: dom (JumpPart i) = Seg 1
then 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} } by Th9;
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of SCM-Data-Loc such that
A1: i = [K,<*a1*>,<*b1*>] and
K in {7,8} ;
JumpPart i = <*a1*> by A1, RECDEF_2:def_2;
hence dom (JumpPart i) = Seg 1 by FINSEQ_1:38; ::_thesis: verum
end;
Lm3: for i being Element of SCM-Instr st InsCode i = 6 holds
dom (JumpPart i) = Seg 1
proof
let i be Element of SCM-Instr ; ::_thesis: ( InsCode i = 6 implies dom (JumpPart i) = Seg 1 )
assume InsCode i = 6 ; ::_thesis: dom (JumpPart i) = Seg 1
then i in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } by Th9;
then consider J being Element of Segm 9, a being Element of NAT such that
A1: i = [J,<*a*>,{}] and
J = 6 ;
JumpPart i = <*a*> by A1, RECDEF_2:def_2;
hence dom (JumpPart i) = Seg 1 by FINSEQ_1:38; ::_thesis: verum
end;
registration
cluster SCM-Instr -> non empty homogeneous ;
coherence
SCM-Instr is homogeneous
proof
let i, j be Element of SCM-Instr ; :: according to COMPOS_0:def_5 ::_thesis: ( not InsCode i = InsCode j or dom (i `2_3) = dom (j `2_3) )
assume A1: InsCode i = InsCode j ; ::_thesis: dom (i `2_3) = dom (j `2_3)
InsCode i <= 8 by Th10;
percasesthen ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 7 or InsCode i = 8 or InsCode i = 6 ) by NAT_1:32;
suppose InsCode i = 0 ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then ( i in {[SCM-Halt,{},{}]} & j in {[SCM-Halt,{},{}]} ) by A1, Th9;
then ( i = [SCM-Halt,{},{}] & j = [SCM-Halt,{},{}] ) by TARSKI:def_1;
hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
suppose ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 ) ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm1;
hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
suppose ( InsCode i = 7 or InsCode i = 8 ) ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then ( dom (JumpPart i) = Seg 1 & dom (JumpPart j) = Seg 1 ) by A1, Lm2;
hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
suppose InsCode i = 6 ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then ( dom (JumpPart i) = Seg 1 & dom (JumpPart j) = Seg 1 ) by A1, Lm3;
hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
end;
end;
end;
Lm4: for T being InsType of SCM-Instr holds
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 )
proof
let T be InsType of SCM-Instr; ::_thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 )
consider y being set such that
A1: [T,y] in proj1 SCM-Instr by XTUPLE_0:def_12;
consider x being set such that
A2: [[T,y],x] in SCM-Instr by A1, XTUPLE_0:def_12;
reconsider I = [T,y,x] as Element of SCM-Instr by A2;
T = InsCode I by RECDEF_2:def_1;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 ) by Th10, NAT_1:32; ::_thesis: verum
end;
Lm5: for T being InsType of SCM-Instr st T = 0 holds
JumpParts T = {0}
proof
let T be InsType of SCM-Instr; ::_thesis: ( T = 0 implies JumpParts T = {0} )
assume A1: T = 0 ; ::_thesis: JumpParts T = {0}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {0} c= JumpParts T
let a be set ; ::_thesis: ( a in JumpParts T implies a in {0} )
assume a in JumpParts T ; ::_thesis: a in {0}
then consider I being Element of SCM-Instr such that
A2: a = JumpPart I and
A3: InsCode I = T ;
I in {[SCM-Halt,{},{}]} by A1, A3, Th9;
then I = [SCM-Halt,{},{}] by TARSKI:def_1;
then a = 0 by A2, RECDEF_2:def_2;
hence a in {0} by TARSKI:def_1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {0} or a in JumpParts T )
assume a in {0} ; ::_thesis: a in JumpParts T
then A4: a = 0 by TARSKI:def_1;
A5: JumpPart [SCM-Halt,{},{}] = {} ;
A6: InsCode [SCM-Halt,{},{}] = SCM-Halt ;
[SCM-Halt,{},{}] in SCM-Instr by Th1;
hence a in JumpParts T by A1, A4, A5, A6; ::_thesis: verum
end;
Lm6: for T being InsType of SCM-Instr st ( T = 1 or T = 2 or T = 3 or T = 4 or T = 5 ) holds
JumpParts T = {{}}
proof
let T be InsType of SCM-Instr; ::_thesis: ( ( T = 1 or T = 2 or T = 3 or T = 4 or T = 5 ) implies JumpParts T = {{}} )
assume A1: ( T = 1 or T = 2 or T = 3 or T = 4 or T = 5 ) ; ::_thesis: JumpParts T = {{}}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T
let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} )
assume x in JumpParts T ; ::_thesis: x in {{}}
then consider I being Element of SCM-Instr such that
A2: x = JumpPart I and
A3: InsCode I = T ;
I in { [J,{},<*b,c*>] where J is Element of Segm 9, b, c is Element of SCM-Data-Loc : J in {1,2,3,4,5} } by A1, A3, Th9;
then consider J being Element of Segm 9, b, c being Element of SCM-Data-Loc such that
A4: I = [J,{},<*b,c*>] and
J in {1,2,3,4,5} ;
x = {} by A2, A4, RECDEF_2:def_2;
hence x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set a = the Element of SCM-Data-Loc ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T )
assume x in {{}} ; ::_thesis: x in JumpParts T
then A5: x = {} by TARSKI:def_1;
A6: JumpPart [T,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] = {} ;
A7: InsCode [T,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] = T ;
T in {1,2,3,4,5} by A1, ENUMSET1:def_3;
then [T,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in SCM-Instr by Th4;
hence x in JumpParts T by A5, A6, A7; ::_thesis: verum
end;
registration
cluster SCM-Instr -> non empty J/A-independent ;
coherence
SCM-Instr is J/A-independent
proof
let T be InsType of SCM-Instr; :: according to COMPOS_0:def_7 ::_thesis: for b1, b2 being set holds
( not b1 in JumpParts T or not proj1 b1 = proj1 b2 or for b3 being set holds
( not [T,b1,b3] in SCM-Instr or [T,b2,b3] in SCM-Instr ) )
let f1, f2 be natural-valued Function; ::_thesis: ( not f1 in JumpParts T or not proj1 f1 = proj1 f2 or for b1 being set holds
( not [T,f1,b1] in SCM-Instr or [T,f2,b1] in SCM-Instr ) )
assume that
A1: f1 in JumpParts T and
A2: dom f1 = dom f2 ; ::_thesis: for b1 being set holds
( not [T,f1,b1] in SCM-Instr or [T,f2,b1] in SCM-Instr )
let p be set ; ::_thesis: ( not [T,f1,p] in SCM-Instr or [T,f2,p] in SCM-Instr )
assume A3: [T,f1,p] in SCM-Instr ; ::_thesis: [T,f2,p] in SCM-Instr
percases ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 ) by Lm4;
suppose T = 0 ; ::_thesis: [T,f2,p] in SCM-Instr
then JumpParts T = {0} by Lm5;
then f1 = 0 by A1, TARSKI:def_1;
then f1 = f2 by A2;
hence [T,f2,p] in SCM-Instr by A3; ::_thesis: verum
end;
suppose ( T = 1 or T = 2 or T = 3 or T = 4 or T = 5 ) ; ::_thesis: [T,f2,p] in SCM-Instr
then A4: JumpParts T = {0} by Lm6;
f1 = 0 by A4, A1, TARSKI:def_1;
then f1 = f2 by A2;
hence [T,f2,p] in SCM-Instr by A3; ::_thesis: verum
end;
supposeA5: T = 6 ; ::_thesis: [T,f2,p] in SCM-Instr
reconsider J = [T,f1,p] as Element of SCM-Instr by A3;
InsCode J = 6 by A5, RECDEF_2:def_1;
then J in { [K,<*i1*>,{}] where K is Element of Segm 9, i1 is Element of NAT : K = 6 } by Th9;
then consider K being Element of Segm 9, i1 being Element of NAT such that
A6: ( J = [K,<*i1*>,{}] & K = 6 ) ;
A7: p = {} by A6, XTUPLE_0:3;
f1 = <*i1*> by A6, XTUPLE_0:3;
then A8: dom f2 = {1} by A2, FINSEQ_1:2, FINSEQ_1:38;
reconsider l = f2 . 1 as Element of NAT by ORDINAL1:def_12;
set I = [T,f2,{}];
[T,f2,{}] = [6,<*l*>,{}] by A5, A8, FINSEQ_1:2, FINSEQ_1:def_8;
then reconsider I = [T,f2,{}] as Element of SCM-Instr by Th2;
f2 = JumpPart I by RECDEF_2:def_2;
hence [T,f2,p] in SCM-Instr by A7; ::_thesis: verum
end;
supposeA9: ( T = 7 or T = 8 ) ; ::_thesis: [T,f2,p] in SCM-Instr
reconsider J = [T,f1,p] as Element of SCM-Instr by A3;
InsCode J = T by RECDEF_2:def_1;
then J in { [K,<*i1*>,<*a*>] where K is Element of Segm 9, i1 is Element of NAT , a is Element of SCM-Data-Loc : K in {7,8} } by A9, Th9;
then consider K being Element of Segm 9, i1 being Element of NAT , a being Element of SCM-Data-Loc such that
A10: J = [K,<*i1*>,<*a*>] and
K in {7,8} ;
A11: p = <*a*> by A10, XTUPLE_0:3;
f1 = <*i1*> by A10, XTUPLE_0:3;
then A12: dom f2 = {1} by A2, FINSEQ_1:2, FINSEQ_1:38;
reconsider l = f2 . 1 as Element of NAT by ORDINAL1:def_12;
set I = [T,f2,p];
A13: T in {7,8} by A9, TARSKI:def_2;
[T,f2,p] = [T,<*l*>,<*a*>] by A11, A12, FINSEQ_1:2, FINSEQ_1:def_8;
then reconsider I = [T,f2,p] as Element of SCM-Instr by A13, Th3;
InsCode I = T by RECDEF_2:def_1;
then I in { [L,<*i2*>,<*b*>] where L is Element of Segm 9, i2 is Element of NAT , b is Element of SCM-Data-Loc : L in {7,8} } by A9, Th9;
then consider L being Element of Segm 9, i2 being Element of NAT , b being Element of SCM-Data-Loc such that
A14: I = [L,<*i2*>,<*b*>] and
L in {7,8} ;
L = InsCode I by A14, RECDEF_2:def_1
.= T by RECDEF_2:def_1 ;
then A15: I = [T,<*i2*>,<*b*>] by A14;
thus [T,f2,p] in SCM-Instr by A15; ::_thesis: verum
end;
end;
end;
end;
registration
cluster SCM-Instr -> non empty with_halt ;
coherence
SCM-Instr is with_halt
proof
thus [0,{},{}] in SCM-Instr by Th1; :: according to COMPOS_0:def_10 ::_thesis: verum
end;
end;