:: SCMRINGI semantic presentation
begin
registration
cluster SCM-Instr -> non trivial ;
coherence
not SCM-Instr is trivial
proof
set e = the Element of SCM-Data-Loc ;
( 1 in {1,2,3,4,5} & 1 is Element of Segm 9 ) by ENUMSET1:def_3, NAT_1:44;
then [1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in { [K,{},<*b,c*>] where K is Element of Segm 9, b, c is Element of SCM-Data-Loc : K in {1,2,3,4,5} } ;
then A1: [1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in SCM-Instr by XBOOLE_0:def_3;
( 2 in {1,2,3,4,5} & 2 is Element of Segm 9 ) by ENUMSET1:def_3, NAT_1:44;
then [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in { [K,{},<*b,c*>] where K is Element of Segm 9, b, c is Element of SCM-Data-Loc : K in {1,2,3,4,5} } ;
then A2: [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in SCM-Instr by XBOOLE_0:def_3;
[1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] <> [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] by XTUPLE_0:3;
hence not SCM-Instr is trivial by A1, A2, SUBSET_1:def_7; ::_thesis: verum
end;
end;
definition
let S be non empty 1-sorted ;
func SCM-Instr S -> non empty set equals :: SCMRINGI:def 1
((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ;
coherence
((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } is non empty set ;
end;
:: deftheorem defines SCM-Instr SCMRINGI:def_1_:_
for S being non empty 1-sorted holds SCM-Instr S = ((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ;
registration
let S be non empty 1-sorted ;
cluster SCM-Instr S -> non empty non trivial ;
coherence
not SCM-Instr S is trivial
proof
set e1 = the Element of SCM-Data-Loc ;
A1: SCM-Instr S = (({[0,{},{}]} \/ { [I,{},<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i1*>,{}] where i1 is Element of NAT : verum } ) \/ ( { [7,<*i2*>,<*d3*>] where i2 is Element of NAT , d3 is Element of SCM-Data-Loc : verum } \/ { [5,{},<*d4,r*>] where d4 is Element of SCM-Data-Loc , r is Element of S : verum } ) by XBOOLE_1:4
.= ({[0,{},{}]} \/ { [I,{},<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ ( { [6,<*i1*>,{}] where i1 is Element of NAT : verum } \/ ( { [7,<*i2*>,<*d3*>] where i2 is Element of NAT , d3 is Element of SCM-Data-Loc : verum } \/ { [5,{},<*d4,r*>] where d4 is Element of SCM-Data-Loc , r is Element of S : verum } )) by XBOOLE_1:4
.= { [I,{},<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } \/ ({[0,{},{}]} \/ ( { [6,<*i1*>,{}] where i1 is Element of NAT : verum } \/ ( { [7,<*i2*>,<*d3*>] where i2 is Element of NAT , d3 is Element of SCM-Data-Loc : verum } \/ { [5,{},<*d4,r*>] where d4 is Element of SCM-Data-Loc , r is Element of S : verum } ))) by XBOOLE_1:4 ;
( 2 in Segm 8 & 2 in {1,2,3,4} ) by ENUMSET1:def_2, NAT_1:44;
then [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in { [I,{},<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } ;
then A2: [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in SCM-Instr S by A1, XBOOLE_0:def_3;
A3: [1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] <> [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] by XTUPLE_0:3;
( 1 in Segm 8 & 1 in {1,2,3,4} ) by ENUMSET1:def_2, NAT_1:44;
then [1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in { [I,{},<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } ;
then [1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in SCM-Instr S by A1, XBOOLE_0:def_3;
hence not SCM-Instr S is trivial by A2, A3, SUBSET_1:def_7; ::_thesis: verum
end;
end;
definition
let S be non empty 1-sorted ;
let x be Element of SCM-Instr S;
given mk, ml being Element of SCM-Data-Loc , I being Element of Segm 8 such that A1: x = [I,{},<*mk,ml*>] ;
funcx address_1 -> Element of SCM-Data-Loc means :Def2: :: SCMRINGI:def 2
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 :Def3: :: SCMRINGI:def 3
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;
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 Def2 defines address_1 SCMRINGI:def_2_:_
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,{},<*mk,ml*>] holds
for b3 being Element of SCM-Data-Loc holds
( b3 = x address_1 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b3 = f /. 1 ) );
:: deftheorem Def3 defines address_2 SCMRINGI:def_3_:_
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,{},<*mk,ml*>] holds
for b3 being Element of SCM-Data-Loc holds
( b3 = x address_2 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b3 = f /. 2 ) );
theorem :: SCMRINGI:1
for I being Element of Segm 8
for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk, ml being Element of SCM-Data-Loc st x = [I,{},<*mk,ml*>] holds
( x address_1 = mk & x address_2 = ml )
proof
let I be Element of Segm 8; ::_thesis: for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk, ml being Element of SCM-Data-Loc st x = [I,{},<*mk,ml*>] holds
( x address_1 = mk & x address_2 = ml )
let S be non empty 1-sorted ; ::_thesis: for x being Element of SCM-Instr S
for mk, ml being Element of SCM-Data-Loc st x = [I,{},<*mk,ml*>] holds
( x address_1 = mk & x address_2 = ml )
let x be Element of SCM-Instr S; ::_thesis: for mk, ml being Element of SCM-Data-Loc st x = [I,{},<*mk,ml*>] holds
( x address_1 = mk & x address_2 = ml )
let mk, ml be Element of SCM-Data-Loc ; ::_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 Def2;
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, Def3;
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 R be non empty 1-sorted ;
let x be Element of SCM-Instr R;
given mk being Element of NAT , I being Element of Segm 8 such that A1: x = [I,<*mk*>,{}] ;
funcx jump_address -> Element of NAT means :Def4: :: SCMRINGI:def 4
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;
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 Def4 defines jump_address SCMRINGI:def_4_:_
for R being non empty 1-sorted
for x being Element of SCM-Instr R st ex mk being Element of NAT ex I being Element of Segm 8 st x = [I,<*mk*>,{}] holds
for b3 being Element of NAT holds
( b3 = x jump_address iff ex f being FinSequence of NAT st
( f = x `2_3 & b3 = f /. 1 ) );
theorem :: SCMRINGI:2
for I being Element of Segm 8
for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk being Element of NAT st x = [I,<*mk*>,{}] holds
x jump_address = mk
proof
let I be Element of Segm 8; ::_thesis: for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk being Element of NAT st x = [I,<*mk*>,{}] holds
x jump_address = mk
let S be non empty 1-sorted ; ::_thesis: for x being Element of SCM-Instr S
for mk being Element of NAT st x = [I,<*mk*>,{}] holds
x jump_address = mk
let x be Element of SCM-Instr S; ::_thesis: for mk being Element of NAT st x = [I,<*mk*>,{}] holds
x jump_address = mk
let mk be Element of NAT ; ::_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 Def4;
f = <*mk*> by A1, A2, RECDEF_2:def_2;
hence x jump_address = mk by A3, FINSEQ_4:16; ::_thesis: verum
end;
definition
let S be non empty 1-sorted ;
let x be Element of SCM-Instr S;
given mk being Element of NAT , ml being Element of SCM-Data-Loc , I being Element of Segm 8 such that A1: x = [I,<*mk*>,<*ml*>] ;
funcx cjump_address -> Element of NAT means :Def5: :: SCMRINGI:def 5
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;
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 :Def6: :: SCMRINGI:def 6
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;
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 Def5 defines cjump_address SCMRINGI:def_5_:_
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,<*mk*>,<*ml*>] holds
for b3 being Element of NAT holds
( b3 = x cjump_address iff ex mk being Element of NAT st
( <*mk*> = x `2_3 & b3 = <*mk*> /. 1 ) );
:: deftheorem Def6 defines cond_address SCMRINGI:def_6_:_
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,<*mk*>,<*ml*>] holds
for b3 being Element of SCM-Data-Loc holds
( b3 = x cond_address iff ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b3 = <*ml*> /. 1 ) );
theorem :: SCMRINGI:3
for I being Element of Segm 8
for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk being Element of NAT
for ml being Element of SCM-Data-Loc st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )
proof
let I be Element of Segm 8; ::_thesis: for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk being Element of NAT
for ml being Element of SCM-Data-Loc st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )
let S be non empty 1-sorted ; ::_thesis: for x being Element of SCM-Instr S
for mk being Element of NAT
for ml being Element of SCM-Data-Loc st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )
let x be Element of SCM-Instr S; ::_thesis: for mk being Element of NAT
for ml being Element of SCM-Data-Loc 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 st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )
let ml be Element of SCM-Data-Loc ; ::_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 Def5;
<*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, Def6;
<*ml9*> = <*ml*> by A1, A4, RECDEF_2:def_3;
hence x cond_address = ml by A5, FINSEQ_4:16; ::_thesis: verum
end;
definition
let S be non empty 1-sorted ;
let d be Element of SCM-Data-Loc ;
let s be Element of S;
:: original: <*
redefine func<*d,s*> -> FinSequence of SCM-Data-Loc \/ the carrier of S;
coherence
<*d,s*> is FinSequence of SCM-Data-Loc \/ the carrier of S
proof
let y be set ; :: according to TARSKI:def_3,FINSEQ_1:def_4 ::_thesis: ( not y in proj2 <*d,s*> or y in SCM-Data-Loc \/ the carrier of S )
A1: dom <*d,s*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
assume y in rng <*d,s*> ; ::_thesis: y in SCM-Data-Loc \/ the carrier of S
then consider x being set such that
A2: x in dom <*d,s*> and
A3: <*d,s*> . x = y by FUNCT_1:def_3;
percases ( x = 1 or x = 2 ) by A2, A1, TARSKI:def_2;
suppose x = 1 ; ::_thesis: y in SCM-Data-Loc \/ the carrier of S
then y = d by A3, FINSEQ_1:44;
hence y in SCM-Data-Loc \/ the carrier of S by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x = 2 ; ::_thesis: y in SCM-Data-Loc \/ the carrier of S
then y = s by A3, FINSEQ_1:44;
hence y in SCM-Data-Loc \/ the carrier of S by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;
definition
let S be non empty 1-sorted ;
let x be Element of SCM-Instr S;
given mk being Element of SCM-Data-Loc , r being Element of S, I being Element of Segm 8 such that A1: x = [I,{},<*mk,r*>] ;
funcx const_address -> Element of SCM-Data-Loc means :Def7: :: SCMRINGI:def 7
ex f being FinSequence of SCM-Data-Loc \/ the carrier of S 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 \/ the carrier of S st
( f = x `3_3 & b1 = f /. 1 )
proof
take mk ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & mk = f /. 1 )
take <*mk,r*> ; ::_thesis: ( <*mk,r*> = x `3_3 & mk = <*mk,r*> /. 1 )
( mk is Element of SCM-Data-Loc \/ the carrier of S & r is Element of SCM-Data-Loc \/ the carrier of S ) by XBOOLE_0:def_3;
hence ( <*mk,r*> = x `3_3 & mk = <*mk,r*> /. 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 \/ the carrier of S st
( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b2 = f /. 1 ) holds
b1 = b2 ;
funcx const_value -> Element of S means :Def8: :: SCMRINGI:def 8
ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & it = f /. 2 );
existence
ex b1 being Element of S ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b1 = f /. 2 )
proof
take r ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & r = f /. 2 )
take <*mk,r*> ; ::_thesis: ( <*mk,r*> = x `3_3 & r = <*mk,r*> /. 2 )
( mk is Element of SCM-Data-Loc \/ the carrier of S & r is Element of SCM-Data-Loc \/ the carrier of S ) by XBOOLE_0:def_3;
hence ( <*mk,r*> = x `3_3 & r = <*mk,r*> /. 2 ) by A1, FINSEQ_4:17, RECDEF_2:def_3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of S st ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b2 = f /. 2 ) holds
b1 = b2 ;
end;
:: deftheorem Def7 defines const_address SCMRINGI:def_7_:_
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of SCM-Data-Loc ex r being Element of S ex I being Element of Segm 8 st x = [I,{},<*mk,r*>] holds
for b3 being Element of SCM-Data-Loc holds
( b3 = x const_address iff ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b3 = f /. 1 ) );
:: deftheorem Def8 defines const_value SCMRINGI:def_8_:_
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of SCM-Data-Loc ex r being Element of S ex I being Element of Segm 8 st x = [I,{},<*mk,r*>] holds
for b3 being Element of S holds
( b3 = x const_value iff ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b3 = f /. 2 ) );
theorem :: SCMRINGI:4
for I being Element of Segm 8
for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk being Element of SCM-Data-Loc
for r being Element of S st x = [I,{},<*mk,r*>] holds
( x const_address = mk & x const_value = r )
proof
let I be Element of Segm 8; ::_thesis: for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk being Element of SCM-Data-Loc
for r being Element of S st x = [I,{},<*mk,r*>] holds
( x const_address = mk & x const_value = r )
let S be non empty 1-sorted ; ::_thesis: for x being Element of SCM-Instr S
for mk being Element of SCM-Data-Loc
for r being Element of S st x = [I,{},<*mk,r*>] holds
( x const_address = mk & x const_value = r )
let x be Element of SCM-Instr S; ::_thesis: for mk being Element of SCM-Data-Loc
for r being Element of S st x = [I,{},<*mk,r*>] holds
( x const_address = mk & x const_value = r )
let mk be Element of SCM-Data-Loc ; ::_thesis: for r being Element of S st x = [I,{},<*mk,r*>] holds
( x const_address = mk & x const_value = r )
let r be Element of S; ::_thesis: ( x = [I,{},<*mk,r*>] implies ( x const_address = mk & x const_value = r ) )
A1: ( mk is Element of SCM-Data-Loc \/ the carrier of S & r is Element of SCM-Data-Loc \/ the carrier of S ) by XBOOLE_0:def_3;
assume A2: x = [I,{},<*mk,r*>] ; ::_thesis: ( x const_address = mk & x const_value = r )
then consider f being FinSequence of SCM-Data-Loc \/ the carrier of S such that
A3: f = x `3_3 and
A4: x const_address = f /. 1 by Def7;
f = <*mk,r*> by A2, A3, RECDEF_2:def_3;
hence x const_address = mk by A4, A1, FINSEQ_4:17; ::_thesis: x const_value = r
consider f being FinSequence of SCM-Data-Loc \/ the carrier of S such that
A5: f = x `3_3 and
A6: x const_value = f /. 2 by A2, Def8;
f = <*mk,r*> by A2, A5, RECDEF_2:def_3;
hence x const_value = r by A1, A6, FINSEQ_4:17; ::_thesis: verum
end;
theorem Th5: :: SCMRINGI:5
for S being non empty 1-sorted holds SCM-Instr S c= [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
proof
let S be non empty 1-sorted ; ::_thesis: SCM-Instr S c= [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
set X = proj2 (SCM-Instr S);
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in SCM-Instr S or u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] )
assume A1: u in SCM-Instr S ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
A2: {} in NAT * by FINSEQ_1:49;
percases ( u in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or u in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ) by A1, XBOOLE_0:def_3;
supposeA3: u in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
percases ( u in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } or u in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ) by A3, XBOOLE_0:def_3;
supposeA4: u in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
percases ( u in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } or u in { [6,<*i*>,{}] where i is Element of NAT : verum } ) by A4, XBOOLE_0:def_3;
supposeA5: u in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
percases ( u in {[0,{},{}]} or u in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) by A5, XBOOLE_0:def_3;
suppose u in {[0,{},{}]} ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
then A6: u = [0,{},{}] by TARSKI:def_1;
then ( 0 in NAT & {} in proj2 (SCM-Instr S) ) by A1, XTUPLE_0:def_13;
hence u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A6, A2, MCART_1:69; ::_thesis: verum
end;
suppose u in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
then consider I being Element of Segm 8, a, b being Element of SCM-Data-Loc such that
A7: ( u = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;
( I in NAT & <*a,b*> in proj2 (SCM-Instr S) ) by A7, A1, XTUPLE_0:def_13;
hence u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A7, A2, MCART_1:69; ::_thesis: verum
end;
end;
end;
suppose u in { [6,<*i*>,{}] where i is Element of NAT : verum } ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
then consider i being Element of NAT such that
A8: u = [6,<*i*>,{}] ;
A9: <*i*> in NAT * by FUNCT_7:18;
( 6 in NAT & {} in proj2 (SCM-Instr S) ) by A8, A1, XTUPLE_0:def_13;
hence u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A8, A9, MCART_1:69; ::_thesis: verum
end;
end;
end;
suppose u in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
then consider i being Element of NAT , a being Element of SCM-Data-Loc such that
A10: u = [7,<*i*>,<*a*>] ;
A11: <*i*> in NAT * by FUNCT_7:18;
( 7 in NAT & <*a*> in proj2 (SCM-Instr S) ) by A10, A1, XTUPLE_0:def_13;
hence u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A10, A11, MCART_1:69; ::_thesis: verum
end;
end;
end;
suppose u in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
then consider a being Element of SCM-Data-Loc , r being Element of S such that
A12: u = [5,{},<*a,r*>] ;
( 5 in NAT & <*a,r*> in proj2 (SCM-Instr S) ) by A12, A1, XTUPLE_0:def_13;
hence u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A12, A2, MCART_1:69; ::_thesis: verum
end;
end;
end;
registration
let S be non empty 1-sorted ;
cluster proj2 (SCM-Instr S) -> FinSequence-membered ;
coherence
proj2 (SCM-Instr S) is FinSequence-membered
proof
let f be set ; :: according to FINSEQ_1:def_18 ::_thesis: ( not f in proj2 (SCM-Instr S) or f is set )
assume f in proj2 (SCM-Instr S) ; ::_thesis: f is set
then consider y being set such that
A1: [y,f] in SCM-Instr S by XTUPLE_0:def_13;
set u = [y,f];
percases ( [y,f] in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or [y,f] in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ) by A1, XBOOLE_0:def_3;
supposeA2: [y,f] in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ; ::_thesis: f is set
percases ( [y,f] in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } or [y,f] in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ) by A2, XBOOLE_0:def_3;
supposeA3: [y,f] in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ; ::_thesis: f is set
percases ( [y,f] in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } or [y,f] in { [6,<*i*>,{}] where i is Element of NAT : verum } ) by A3, XBOOLE_0:def_3;
supposeA4: [y,f] in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ; ::_thesis: f is set
percases ( [y,f] in {[0,{},{}]} or [y,f] in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) by A4, XBOOLE_0:def_3;
suppose [y,f] in {[0,{},{}]} ; ::_thesis: f is set
then [y,f] = [0,{},{}] by TARSKI:def_1;
then f = {} by XTUPLE_0:1;
hence f is FinSequence ; ::_thesis: verum
end;
suppose [y,f] in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ; ::_thesis: f is set
then consider I being Element of Segm 8, a, b being Element of SCM-Data-Loc such that
A5: ( [y,f] = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;
f = <*a,b*> by A5, XTUPLE_0:1;
hence f is FinSequence ; ::_thesis: verum
end;
end;
end;
suppose [y,f] in { [6,<*i*>,{}] where i is Element of NAT : verum } ; ::_thesis: f is set
then consider i being Element of NAT such that
A6: [y,f] = [6,<*i*>,{}] ;
f = {} by A6, XTUPLE_0:1;
hence f is FinSequence ; ::_thesis: verum
end;
end;
end;
suppose [y,f] in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ; ::_thesis: f is set
then consider i being Element of NAT , a being Element of SCM-Data-Loc such that
A7: [y,f] = [7,<*i*>,<*a*>] ;
f = <*a*> by A7, XTUPLE_0:1;
hence f is FinSequence ; ::_thesis: verum
end;
end;
end;
suppose [y,f] in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ; ::_thesis: f is set
then consider a being Element of SCM-Data-Loc , r being Element of S such that
A8: [y,f] = [5,{},<*a,r*>] ;
f = <*a,r*> by A8, XTUPLE_0:1;
hence f is FinSequence ; ::_thesis: verum
end;
end;
end;
end;
theorem Th6: :: SCMRINGI:6
for S being non empty 1-sorted holds [0,{},{}] in SCM-Instr S
proof
let S be non empty 1-sorted ; ::_thesis: [0,{},{}] in SCM-Instr S
[0,{},{}] in {[0,{},{}]} by TARSKI:def_1;
then [0,{},{}] in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } by XBOOLE_0:def_3;
then [0,{},{}] in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } by XBOOLE_0:def_3;
then [0,{},{}] in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } by XBOOLE_0:def_3;
hence [0,{},{}] in SCM-Instr S by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th7: :: SCMRINGI:7
for S being non empty 1-sorted
for x being Element of SCM-Instr S holds
( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } & ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 ) ) or ( x in { [6,<*i*>,{}] where i is Element of NAT : verum } & InsCode x = 6 ) or ( x in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } & InsCode x = 7 ) or ( x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } & InsCode x = 5 ) )
proof
let S be non empty 1-sorted ; ::_thesis: for x being Element of SCM-Instr S holds
( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } & ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 ) ) or ( x in { [6,<*i*>,{}] where i is Element of NAT : verum } & InsCode x = 6 ) or ( x in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } & InsCode x = 7 ) or ( x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } & InsCode x = 5 ) )
let x be Element of SCM-Instr S; ::_thesis: ( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } & ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 ) ) or ( x in { [6,<*i*>,{}] where i is Element of NAT : verum } & InsCode x = 6 ) or ( x in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } & InsCode x = 7 ) or ( x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } & InsCode x = 5 ) )
( x in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ) by XBOOLE_0:def_3;
then ( x in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } or x in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ) by XBOOLE_0:def_3;
then ( x in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } or x in { [6,<*i*>,{}] where i is Element of NAT : verum } or x in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ) by XBOOLE_0:def_3;
percasesthen ( x in {[0,{},{}]} or x in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } or x in { [6,<*i*>,{}] where i is Element of NAT : verum } or x in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ) by XBOOLE_0:def_3;
case x in {[0,{},{}]} ; ::_thesis: InsCode x = 0
then x = [0,{},{}] by TARSKI:def_1;
hence InsCode x = 0 by RECDEF_2:def_1; ::_thesis: verum
end;
case x in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ; ::_thesis: ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 )
then consider I being Element of Segm 8, a, b being Element of SCM-Data-Loc such that
A1: x = [I,{},<*a,b*>] and
A2: I in {1,2,3,4} ;
InsCode x = I by A1, RECDEF_2:def_1;
hence ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 ) by A2, ENUMSET1:def_2; ::_thesis: verum
end;
case x in { [6,<*i*>,{}] where i is Element of NAT : verum } ; ::_thesis: InsCode x = 6
then ex i being Element of NAT st x = [6,<*i*>,{}] ;
hence InsCode x = 6 by RECDEF_2:def_1; ::_thesis: verum
end;
case x in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ; ::_thesis: InsCode x = 7
then ex i being Element of NAT ex a being Element of SCM-Data-Loc st x = [7,<*i*>,<*a*>] ;
hence InsCode x = 7 by RECDEF_2:def_1; ::_thesis: verum
end;
case x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ; ::_thesis: InsCode x = 5
then ex a being Element of SCM-Data-Loc ex r being Element of S st x = [5,{},<*a,r*>] ;
hence InsCode x = 5 by RECDEF_2:def_1; ::_thesis: verum
end;
end;
end;
begin
registration
cluster non empty trivial right_complementable strict V92() V93() V94() V103() V110() V111() for doubleLoopStr ;
existence
ex b1 being Ring st
( b1 is strict & b1 is trivial )
proof
take the 1 -element strict doubleLoopStr ; ::_thesis: ( the 1 -element strict doubleLoopStr is strict & the 1 -element strict doubleLoopStr is trivial )
thus ( the 1 -element strict doubleLoopStr is strict & the 1 -element strict doubleLoopStr is trivial ) ; ::_thesis: verum
end;
end;
registration
let R be Ring;
cluster SCM-Instr R -> non empty standard-ins ;
coherence
SCM-Instr R is standard-ins
proof
consider X being non empty set such that
A1: proj2 (SCM-Instr R) c= X * by FINSEQ_1:85;
take X ; :: according to COMPOS_0:def_1 ::_thesis: SCM-Instr R c= [:NAT,(NAT *),(X *):]
A2: SCM-Instr R c= [:NAT,(NAT *),(proj2 (SCM-Instr R)):] by Th5;
[:NAT,(NAT *),(proj2 (SCM-Instr R)):] c= [:NAT,(NAT *),(X *):] by A1, MCART_1:73;
hence SCM-Instr R c= [:NAT,(NAT *),(X *):] by A2, XBOOLE_1:1; ::_thesis: verum
end;
end;
Lm1: for R being Ring
for i being Element of SCM-Instr R holds InsCode i <= 7
proof
let R be Ring; ::_thesis: for i being Element of SCM-Instr R holds InsCode i <= 7
let i be Element of SCM-Instr R; ::_thesis: InsCode i <= 7
( 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 = 6 or InsCode i = 7 ) by Th7;
hence InsCode i <= 7 ; ::_thesis: verum
end;
Lm2: for S being non empty 1-sorted
for i being Element of SCM-Instr S st ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 ) holds
JumpPart i = {}
proof
let S be non empty 1-sorted ; ::_thesis: for i being Element of SCM-Instr S st ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 ) holds
JumpPart i = {}
let i be Element of SCM-Instr S; ::_thesis: ( ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 ) implies JumpPart i = {} )
assume ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 ) ; ::_thesis: JumpPart i = {}
then i in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } by Th7;
then ex I being Element of Segm 8 ex a, b being Element of SCM-Data-Loc st
( i = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;
hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum
end;
Lm3: for S being non empty 1-sorted
for i being Element of SCM-Instr S st InsCode i = 5 holds
JumpPart i = {}
proof
let S be non empty 1-sorted ; ::_thesis: for i being Element of SCM-Instr S st InsCode i = 5 holds
JumpPart i = {}
let i be Element of SCM-Instr S; ::_thesis: ( InsCode i = 5 implies JumpPart i = {} )
assume InsCode i = 5 ; ::_thesis: JumpPart i = {}
then i in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } by Th7;
then ex a being Element of SCM-Data-Loc ex r being Element of S st i = [5,{},<*a,r*>] ;
hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum
end;
Lm4: for R being Ring
for I being Element of SCM-Instr R st InsCode I = 6 holds
dom (JumpPart I) = Seg 1
proof
let R be Ring; ::_thesis: for I being Element of SCM-Instr R st InsCode I = 6 holds
dom (JumpPart I) = Seg 1
let I be Element of SCM-Instr R; ::_thesis: ( InsCode I = 6 implies dom (JumpPart I) = Seg 1 )
assume InsCode I = 6 ; ::_thesis: dom (JumpPart I) = Seg 1
then I in { [6,<*i*>,{}] where i is Element of NAT : verum } by Th7;
then consider i being Element of NAT such that
A1: I = [6,<*i*>,{}] ;
JumpPart I = <*i*> by A1, RECDEF_2:def_2;
hence dom (JumpPart I) = Seg 1 by FINSEQ_1:38; ::_thesis: verum
end;
Lm5: for R being Ring
for I being Element of SCM-Instr R st InsCode I = 7 holds
dom (JumpPart I) = Seg 1
proof
let R be Ring; ::_thesis: for I being Element of SCM-Instr R st InsCode I = 7 holds
dom (JumpPart I) = Seg 1
let I be Element of SCM-Instr R; ::_thesis: ( InsCode I = 7 implies dom (JumpPart I) = Seg 1 )
assume InsCode I = 7 ; ::_thesis: dom (JumpPart I) = Seg 1
then I in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } by Th7;
then consider i being Element of NAT , a being Element of SCM-Data-Loc such that
A1: I = [7,<*i*>,<*a*>] ;
JumpPart I = <*i*> by A1, RECDEF_2:def_2;
hence dom (JumpPart I) = Seg 1 by FINSEQ_1:38; ::_thesis: verum
end;
registration
let R be Ring;
cluster SCM-Instr R -> non empty homogeneous ;
coherence
SCM-Instr R is homogeneous
proof
let i, j be Element of SCM-Instr R; :: 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 <= 7 by Lm1;
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 = 6 or InsCode i = 7 ) by NAT_1:31;
suppose InsCode i = 0 ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then ( i in {[0,{},{}]} & j in {[0,{},{}]} ) by A1, Th7;
then ( i = [0,{},{}] & j = [0,{},{}] ) 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 ) ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm2;
hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
suppose InsCode i = 5 ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm3;
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, Lm4;
hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
suppose InsCode i = 7 ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then ( dom (JumpPart i) = Seg 1 & dom (JumpPart j) = Seg 1 ) by A1, Lm5;
hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
end;
end;
end;
registration
let R be Ring;
cluster SCM-Instr R -> non empty J/A-independent ;
coherence
SCM-Instr R is J/A-independent
proof
let T be InsType of (SCM-Instr R); :: 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 R or [T,b2,b3] in SCM-Instr R ) )
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 R or [T,f2,b1] in SCM-Instr R ) )
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 R or [T,f2,b1] in SCM-Instr R )
let p be set ; ::_thesis: ( not [T,f1,p] in SCM-Instr R or [T,f2,p] in SCM-Instr R )
assume A3: [T,f1,p] in SCM-Instr R ; ::_thesis: [T,f2,p] in SCM-Instr R
reconsider II = [T,f1,p] as Element of SCM-Instr R by A3;
A4: InsCode II = T by RECDEF_2:def_1;
InsCode II <= 7 by Lm1;
percasesthen ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 ) by A4, NAT_1:31;
suppose T = 0 ; ::_thesis: [T,f2,p] in SCM-Instr R
then II in {[0,{},{}]} by A4, Th7;
then II = [0,{},{}] by TARSKI:def_1;
then JumpPart II = {} by RECDEF_2:def_2;
then A5: JumpParts T = {0} by A4, COMPOS_0:11;
f1 = 0 by A5, A1, TARSKI:def_1;
then f1 = f2 by A2;
hence [T,f2,p] in SCM-Instr R by A3; ::_thesis: verum
end;
suppose ( T = 1 or T = 2 or T = 3 or T = 4 ) ; ::_thesis: [T,f2,p] in SCM-Instr R
then II in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } by A4, Th7;
then ex I being Element of Segm 8 ex a, b being Element of SCM-Data-Loc st
( II = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;
then JumpPart II = {} by RECDEF_2:def_2;
then A6: JumpParts T = {0} by A4, COMPOS_0:11;
f1 = 0 by A6, A1, TARSKI:def_1;
then f1 = f2 by A2;
hence [T,f2,p] in SCM-Instr R by A3; ::_thesis: verum
end;
suppose T = 5 ; ::_thesis: [T,f2,p] in SCM-Instr R
then II in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of R : verum } by A4, Th7;
then ex a being Element of SCM-Data-Loc ex r being Element of R st II = [5,{},<*a,r*>] ;
then JumpPart II = {} by RECDEF_2:def_2;
then A7: JumpParts T = {0} by A4, COMPOS_0:11;
f1 = 0 by A7, A1, TARSKI:def_1;
then f1 = f2 by A2;
hence [T,f2,p] in SCM-Instr R by A3; ::_thesis: verum
end;
supposeA8: T = 6 ; ::_thesis: [T,f2,p] in SCM-Instr R
reconsider J = [T,f1,p] as Element of SCM-Instr R by A3;
InsCode J = 6 by A8, RECDEF_2:def_1;
then J in { [6,<*i*>,{}] where i is Element of NAT : verum } by Th7;
then consider i1 being Element of NAT such that
A9: J = [6,<*i1*>,{}] ;
A10: p = {} by A9, XTUPLE_0:3;
f1 = <*i1*> by A9, XTUPLE_0:3;
then A11: 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,{}];
A12: [T,f2,{}] = [6,<*l*>,{}] by A8, A11, FINSEQ_1:2, FINSEQ_1:def_8;
[6,<*l*>,{}] in { [6,<*n*>,{}] where n is Element of NAT : verum } ;
then [6,<*l*>,{}] in ({[0,{},{}]} \/ { [H,{},<*a,b*>] where H is Element of Segm 8, a, b is Element of SCM-Data-Loc : H in {1,2,3,4} } ) \/ { [6,<*n*>,{}] where n is Element of NAT : verum } by XBOOLE_0:def_3;
then [6,<*l*>,{}] in (({[0,{},{}]} \/ { [H,{},<*a,b*>] where H is Element of Segm 8, a, b is Element of SCM-Data-Loc : H in {1,2,3,4} } ) \/ { [6,<*n*>,{}] where n is Element of NAT : verum } ) \/ { [7,<*n*>,<*a*>] where n is Element of NAT , a is Element of SCM-Data-Loc : verum } by XBOOLE_0:def_3;
then [6,<*l*>,{}] in SCM-Instr R by XBOOLE_0:def_3;
then reconsider I = [T,f2,{}] as Element of SCM-Instr R by A12;
f2 = JumpPart I by RECDEF_2:def_2;
hence [T,f2,p] in SCM-Instr R by A10; ::_thesis: verum
end;
supposeA13: T = 7 ; ::_thesis: [T,f2,p] in SCM-Instr R
reconsider J = [T,f1,p] as Element of SCM-Instr R by A3;
InsCode J = T by RECDEF_2:def_1;
then J in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } by A13, Th7;
then consider i1 being Element of NAT , a being Element of SCM-Data-Loc such that
A14: J = [7,<*i1*>,<*a*>] ;
A15: p = <*a*> by A14, XTUPLE_0:3;
f1 = <*i1*> by A14, XTUPLE_0:3;
then A16: 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];
A17: [T,f2,p] = [T,<*l*>,<*a*>] by A15, A16, FINSEQ_1:2, FINSEQ_1:def_8;
[(InsCode [T,f2,p]),<*l*>,<*a*>] in { [7,<*n*>,<*c*>] where n is Element of NAT , c is Element of SCM-Data-Loc : verum } by A13;
then [(InsCode [T,f2,p]),<*l*>,<*a*>] in (({[0,{},{}]} \/ { [H,{},<*a7,b7*>] where H is Element of Segm 8, a7, b7 is Element of SCM-Data-Loc : H in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a7*>] where i is Element of NAT , a7 is Element of SCM-Data-Loc : verum } by XBOOLE_0:def_3;
then [(InsCode [T,f2,p]),<*l*>,<*a*>] in ((({[0,{},{}]} \/ { [H,{},<*a7,b7*>] where H is Element of Segm 8, a7, b7 is Element of SCM-Data-Loc : H in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a7*>] where i is Element of NAT , a7 is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a7,r7*>] where a7 is Element of SCM-Data-Loc , r7 is Element of R : verum } by XBOOLE_0:def_3;
then [(InsCode [T,f2,p]),<*l*>,<*a*>] in SCM-Instr R ;
then reconsider I = [T,f2,p] as Element of SCM-Instr R by A17;
InsCode I = T by RECDEF_2:def_1;
then I in { [7,<*i2*>,<*b*>] where i2 is Element of NAT , b is Element of SCM-Data-Loc : verum } by A13, Th7;
then consider i2 being Element of NAT , b being Element of SCM-Data-Loc such that
A18: I = [7,<*i2*>,<*b*>] ;
7 = InsCode I by A18, RECDEF_2:def_1
.= T by RECDEF_2:def_1 ;
then A19: I = [T,<*i2*>,<*b*>] by A18;
thus [T,f2,p] in SCM-Instr R by A19; ::_thesis: verum
end;
end;
end;
end;
theorem :: SCMRINGI:8
for S being non empty 1-sorted
for x being set
for d1, d2 being Element of SCM-Data-Loc st x in {1,2,3,4} holds
[x,{},<*d1,d2*>] in SCM-Instr S
proof
let S be non empty 1-sorted ; ::_thesis: for x being set
for d1, d2 being Element of SCM-Data-Loc st x in {1,2,3,4} holds
[x,{},<*d1,d2*>] in SCM-Instr S
let x be set ; ::_thesis: for d1, d2 being Element of SCM-Data-Loc st x in {1,2,3,4} holds
[x,{},<*d1,d2*>] in SCM-Instr S
let d1, d2 be Element of SCM-Data-Loc ; ::_thesis: ( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S )
reconsider D1 = d1, D2 = d2 as Element of SCM-Data-Loc ;
assume A1: x in {1,2,3,4} ; ::_thesis: [x,{},<*d1,d2*>] in SCM-Instr S
then ( x = 1 or x = 2 or x = 3 or x = 4 ) by ENUMSET1:def_2;
then reconsider x = x as Element of Segm 8 by NAT_1:44;
[x,{},<*D1,D2*>] in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } by A1;
then [x,{},<*D1,D2*>] in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } by XBOOLE_0:def_3;
then [x,{},<*D1,D2*>] in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } by XBOOLE_0:def_3;
then [x,{},<*D1,D2*>] in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } by XBOOLE_0:def_3;
hence [x,{},<*d1,d2*>] in SCM-Instr S by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem :: SCMRINGI:9
for S being non empty 1-sorted
for t being Element of S
for d1 being Element of SCM-Data-Loc holds [5,{},<*d1,t*>] in SCM-Instr S
proof
let S be non empty 1-sorted ; ::_thesis: for t being Element of S
for d1 being Element of SCM-Data-Loc holds [5,{},<*d1,t*>] in SCM-Instr S
let t be Element of S; ::_thesis: for d1 being Element of SCM-Data-Loc holds [5,{},<*d1,t*>] in SCM-Instr S
let d1 be Element of SCM-Data-Loc ; ::_thesis: [5,{},<*d1,t*>] in SCM-Instr S
reconsider D1 = d1 as Element of SCM-Data-Loc ;
[5,{},<*D1,t*>] in { [5,{},<*i,a*>] where i is Element of SCM-Data-Loc , a is Element of S : verum } ;
hence [5,{},<*d1,t*>] in SCM-Instr S by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem :: SCMRINGI:10
for S being non empty 1-sorted
for i1 being Element of NAT holds [6,<*i1*>,{}] in SCM-Instr S
proof
let S be non empty 1-sorted ; ::_thesis: for i1 being Element of NAT holds [6,<*i1*>,{}] in SCM-Instr S
let i1 be Element of NAT ; ::_thesis: [6,<*i1*>,{}] in SCM-Instr S
reconsider I1 = i1 as Element of NAT ;
[6,<*I1*>,{}] in { [6,<*i*>,{}] where i is Element of NAT : verum } ;
then [6,<*I1*>,{}] in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } by XBOOLE_0:def_3;
then [6,<*I1*>,{}] in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } by XBOOLE_0:def_3;
hence [6,<*i1*>,{}] in SCM-Instr S by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem :: SCMRINGI:11
for S being non empty 1-sorted
for d1 being Element of SCM-Data-Loc
for i1 being Element of NAT holds [7,<*i1*>,<*d1*>] in SCM-Instr S
proof
let S be non empty 1-sorted ; ::_thesis: for d1 being Element of SCM-Data-Loc
for i1 being Element of NAT holds [7,<*i1*>,<*d1*>] in SCM-Instr S
let d1 be Element of SCM-Data-Loc ; ::_thesis: for i1 being Element of NAT holds [7,<*i1*>,<*d1*>] in SCM-Instr S
let i1 be Element of NAT ; ::_thesis: [7,<*i1*>,<*d1*>] in SCM-Instr S
reconsider D1 = d1 as Element of SCM-Data-Loc ;
reconsider I1 = i1 as Element of NAT ;
[7,<*I1*>,<*D1*>] in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ;
then [7,<*I1*>,<*D1*>] in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } by XBOOLE_0:def_3;
hence [7,<*i1*>,<*d1*>] in SCM-Instr S by XBOOLE_0:def_3; ::_thesis: verum
end;
registration
let S be non empty 1-sorted ;
cluster SCM-Instr S -> non empty with_halt ;
coherence
SCM-Instr S is with_halt
proof
thus [0,{},{}] in SCM-Instr S by Th6; :: according to COMPOS_0:def_10 ::_thesis: verum
end;
end;