:: SCMPDS_I semantic presentation
begin
theorem Th1: :: SCMPDS_I:1
for k being Integer holds k in SCM-Data-Loc \/ INT
proof
let k be Integer; ::_thesis: k in SCM-Data-Loc \/ INT
( k in INT & INT c= SCM-Data-Loc \/ INT ) by INT_1:def_2, XBOOLE_1:7;
hence k in SCM-Data-Loc \/ INT ; ::_thesis: verum
end;
begin
definition
func SCMPDS-Instr -> set equals :: SCMPDS_I:def 1
(((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) \/ { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ;
coherence
(((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) \/ { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } is set ;
end;
:: deftheorem defines SCMPDS-Instr SCMPDS_I:def_1_:_
SCMPDS-Instr = (((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) \/ { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ;
Lm1: [0,{},{}] in SCMPDS-Instr
proof
set S1 = { [14,{},<*k1*>] where k1 is Element of INT : verum } ;
set S2 = { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ;
set S3 = { [I2,{},<*d2,k2*>] where I2 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } ;
[0,{},{}] in {[0,{},{}]} by TARSKI:def_1;
then [0,{},{}] in {[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } by XBOOLE_0:def_3;
then [0,{},{}] in ({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } by XBOOLE_0:def_3;
then [0,{},{}] in (({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I2,{},<*d2,k2*>] where I2 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } by XBOOLE_0:def_3;
then [0,{},{}] in ((({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I2,{},<*d2,k2*>] where I2 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } ) \/ { [I3,{},<*d3,k3,k4*>] where I3 is Element of Segm 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I3 in {4,5,6,7,8} } by XBOOLE_0:def_3;
hence [0,{},{}] in SCMPDS-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem :: SCMPDS_I:2
[14,{},<*0*>] in SCMPDS-Instr
proof
set S1 = { [14,{},<*k1*>] where k1 is Element of INT : verum } ;
set S2 = { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ;
set S3 = { [I2,{},<*d2,k2*>] where I2 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } ;
0 is Element of INT by INT_1:def_2;
then [14,{},<*0*>] in { [14,{},<*k1*>] where k1 is Element of INT : verum } ;
then [14,{},<*0*>] in {[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } by XBOOLE_0:def_3;
then [14,{},<*0*>] in ({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } by XBOOLE_0:def_3;
then [14,{},<*0*>] in (({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I2,{},<*d2,k2*>] where I2 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } by XBOOLE_0:def_3;
then [14,{},<*0*>] in ((({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I2,{},<*d2,k2*>] where I2 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } ) \/ { [I3,{},<*d3,k3,k4*>] where I3 is Element of Segm 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I3 in {4,5,6,7,8} } by XBOOLE_0:def_3;
hence [14,{},<*0*>] in SCMPDS-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;
registration
cluster SCMPDS-Instr -> non empty ;
coherence
not SCMPDS-Instr is empty ;
end;
definition
let d be Element of SCM-Data-Loc ;
let s be Integer;
:: original: <*
redefine func<*d,s*> -> FinSequence of SCM-Data-Loc \/ INT;
coherence
<*d,s*> is FinSequence of SCM-Data-Loc \/ INT
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 \/ INT )
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 \/ INT
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 \/ INT
then y = d by A3, FINSEQ_1:44;
hence y in SCM-Data-Loc \/ INT by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA4: x = 2 ; ::_thesis: y in SCM-Data-Loc \/ INT
A5: s in INT by INT_1:def_2;
y = s by A3, A4, FINSEQ_1:44;
hence y in SCM-Data-Loc \/ INT by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;
definition
let x be Element of SCMPDS-Instr ;
given mk being Element of SCM-Data-Loc , I being Element of Segm 15 such that A1: x = [I,{},<*mk*>] ;
funcx address_1 -> Element of SCM-Data-Loc means :Def2: :: SCMPDS_I: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*> ; ::_thesis: ( <*mk*> = x `3_3 & mk = <*mk*> /. 1 )
thus ( <*mk*> = x `3_3 & mk = <*mk*> /. 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 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 ;
end;
:: deftheorem Def2 defines address_1 SCMPDS_I:def_2_:_
for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex I being Element of Segm 15 st x = [I,{},<*mk*>] 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 ) );
theorem :: SCMPDS_I:3
for I being Element of Segm 15
for x being Element of SCMPDS-Instr
for mk being Element of SCM-Data-Loc st x = [I,{},<*mk*>] holds
x address_1 = mk
proof
let I be Element of Segm 15; ::_thesis: for x being Element of SCMPDS-Instr
for mk being Element of SCM-Data-Loc st x = [I,{},<*mk*>] holds
x address_1 = mk
let x be Element of SCMPDS-Instr ; ::_thesis: for mk being Element of SCM-Data-Loc st x = [I,{},<*mk*>] holds
x address_1 = mk
let mk be Element of SCM-Data-Loc ; ::_thesis: ( x = [I,{},<*mk*>] implies x address_1 = mk )
assume A1: x = [I,{},<*mk*>] ; ::_thesis: x address_1 = mk
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*> by A1, A2, RECDEF_2:def_3;
hence x address_1 = mk by A3, FINSEQ_4:16; ::_thesis: verum
end;
definition
let x be Element of SCMPDS-Instr ;
given r being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*r*>] ;
funcx const_INT -> Integer means :Def3: :: SCMPDS_I:def 3
ex f being FinSequence of INT st
( f = x `3_3 & it = f /. 1 );
existence
ex b1 being Integer ex f being FinSequence of INT st
( f = x `3_3 & b1 = f /. 1 )
proof
reconsider mm = r as Element of INT by INT_1:def_2;
take r ; ::_thesis: ex f being FinSequence of INT st
( f = x `3_3 & r = f /. 1 )
take <*mm*> ; ::_thesis: ( <*mm*> = x `3_3 & r = <*mm*> /. 1 )
thus ( <*mm*> = x `3_3 & r = <*mm*> /. 1 ) by A1, FINSEQ_4:16, RECDEF_2:def_3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of INT st
( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of INT st
( f = x `3_3 & b2 = f /. 1 ) holds
b1 = b2 ;
end;
:: deftheorem Def3 defines const_INT SCMPDS_I:def_3_:_
for x being Element of SCMPDS-Instr st ex r being Integer ex I being Element of Segm 15 st x = [I,{},<*r*>] holds
for b2 being Integer holds
( b2 = x const_INT iff ex f being FinSequence of INT st
( f = x `3_3 & b2 = f /. 1 ) );
theorem :: SCMPDS_I:4
for I being Element of Segm 15
for x being Element of SCMPDS-Instr
for k being Integer st x = [I,{},<*k*>] holds
x const_INT = k
proof
let I be Element of Segm 15; ::_thesis: for x being Element of SCMPDS-Instr
for k being Integer st x = [I,{},<*k*>] holds
x const_INT = k
let x be Element of SCMPDS-Instr ; ::_thesis: for k being Integer st x = [I,{},<*k*>] holds
x const_INT = k
let k be Integer; ::_thesis: ( x = [I,{},<*k*>] implies x const_INT = k )
assume A1: x = [I,{},<*k*>] ; ::_thesis: x const_INT = k
then consider f being FinSequence of INT such that
A2: f = x `3_3 and
A3: x const_INT = f /. 1 by Def3;
( k is Element of INT & f = <*k*> ) by A1, A2, INT_1:def_2, RECDEF_2:def_3;
hence x const_INT = k by A3, FINSEQ_4:16; ::_thesis: verum
end;
definition
let x be Element of SCMPDS-Instr ;
given mk being Element of SCM-Data-Loc , r being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*mk,r*>] ;
funcx P21address -> Element of SCM-Data-Loc means :Def4: :: SCMPDS_I:def 4
ex f being FinSequence of SCM-Data-Loc \/ INT 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 \/ INT st
( f = x `3_3 & b1 = f /. 1 )
proof
take mk ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & mk = f /. 1 )
take <*mk,r*> ; ::_thesis: ( <*mk,r*> = x `3_3 & mk = <*mk,r*> /. 1 )
r in INT by INT_1:def_2;
then ( mk is Element of SCM-Data-Loc \/ INT & r is Element of SCM-Data-Loc \/ INT ) 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 \/ INT st
( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) holds
b1 = b2 ;
funcx P22const -> Integer means :Def5: :: SCMPDS_I:def 5
ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & it = f /. 2 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 )
proof
take r ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & r = f /. 2 )
take <*mk,r*> ; ::_thesis: ( <*mk,r*> = x `3_3 & r = <*mk,r*> /. 2 )
r in INT by INT_1:def_2;
then ( mk is Element of SCM-Data-Loc \/ INT & r is Element of SCM-Data-Loc \/ INT ) 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 Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) holds
b1 = b2 ;
end;
:: deftheorem Def4 defines P21address SCMPDS_I:def_4_:_
for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex r being Integer ex I being Element of Segm 15 st x = [I,{},<*mk,r*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P21address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) );
:: deftheorem Def5 defines P22const SCMPDS_I:def_5_:_
for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex r being Integer ex I being Element of Segm 15 st x = [I,{},<*mk,r*>] holds
for b2 being Integer holds
( b2 = x P22const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) );
theorem :: SCMPDS_I:5
for I being Element of Segm 15
for x being Element of SCMPDS-Instr
for mk being Element of SCM-Data-Loc
for r being Integer st x = [I,{},<*mk,r*>] holds
( x P21address = mk & x P22const = r )
proof
let I be Element of Segm 15; ::_thesis: for x being Element of SCMPDS-Instr
for mk being Element of SCM-Data-Loc
for r being Integer st x = [I,{},<*mk,r*>] holds
( x P21address = mk & x P22const = r )
let x be Element of SCMPDS-Instr ; ::_thesis: for mk being Element of SCM-Data-Loc
for r being Integer st x = [I,{},<*mk,r*>] holds
( x P21address = mk & x P22const = r )
let mk be Element of SCM-Data-Loc ; ::_thesis: for r being Integer st x = [I,{},<*mk,r*>] holds
( x P21address = mk & x P22const = r )
let r be Integer; ::_thesis: ( x = [I,{},<*mk,r*>] implies ( x P21address = mk & x P22const = r ) )
r in INT by INT_1:def_2;
then A1: ( mk is Element of SCM-Data-Loc \/ INT & r is Element of SCM-Data-Loc \/ INT ) by XBOOLE_0:def_3;
assume A2: x = [I,{},<*mk,r*>] ; ::_thesis: ( x P21address = mk & x P22const = r )
then consider f being FinSequence of SCM-Data-Loc \/ INT such that
A3: f = x `3_3 and
A4: x P21address = f /. 1 by Def4;
f = <*mk,r*> by A2, A3, RECDEF_2:def_3;
hence x P21address = mk by A4, A1, FINSEQ_4:17; ::_thesis: x P22const = r
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A5: f = x `3_3 and
A6: x P22const = f /. 2 by A2, Def5;
f = <*mk,r*> by A2, A5, RECDEF_2:def_3;
hence x P22const = r by A1, A6, FINSEQ_4:17; ::_thesis: verum
end;
definition
let x be Element of SCMPDS-Instr ;
given m1 being Element of SCM-Data-Loc , k1, k2 being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*m1,k1,k2*>] ;
funcx P31address -> Element of SCM-Data-Loc means :Def6: :: SCMPDS_I:def 6
ex f being FinSequence of SCM-Data-Loc \/ INT 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 \/ INT st
( f = x `3_3 & b1 = f /. 1 )
proof
reconsider mm = m1, k1 = k1, k2 = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def_3;
take m1 ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & m1 = f /. 1 )
take f = <*mm,k1,k2*>; ::_thesis: ( f = x `3_3 & m1 = f /. 1 )
thus f = x `3_3 by A1, RECDEF_2:def_3; ::_thesis: m1 = f /. 1
thus m1 = f /. 1 by FINSEQ_4:18; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) holds
b1 = b2 ;
funcx P32const -> Integer means :Def7: :: SCMPDS_I:def 7
ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & it = f /. 2 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 )
proof
reconsider m1 = m1, mm = k1, k2 = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def_3;
take k1 ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & k1 = f /. 2 )
take f = <*m1,mm,k2*>; ::_thesis: ( f = x `3_3 & k1 = f /. 2 )
thus f = x `3_3 by A1, RECDEF_2:def_3; ::_thesis: k1 = f /. 2
thus k1 = f /. 2 by FINSEQ_4:18; ::_thesis: verum
end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) holds
b1 = b2 ;
funcx P33const -> Integer means :Def8: :: SCMPDS_I:def 8
ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & it = f /. 3 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 )
proof
reconsider m1 = m1, k1 = k1, mm = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def_3;
take k2 ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & k2 = f /. 3 )
take f = <*m1,k1,mm*>; ::_thesis: ( f = x `3_3 & k2 = f /. 3 )
thus f = x `3_3 by A1, RECDEF_2:def_3; ::_thesis: k2 = f /. 3
thus k2 = f /. 3 by FINSEQ_4:18; ::_thesis: verum
end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 3 ) holds
b1 = b2 ;
end;
:: deftheorem Def6 defines P31address SCMPDS_I:def_6_:_
for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,k1,k2*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P31address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) );
:: deftheorem Def7 defines P32const SCMPDS_I:def_7_:_
for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P32const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) );
:: deftheorem Def8 defines P33const SCMPDS_I:def_8_:_
for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P33const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 3 ) );
theorem :: SCMPDS_I:6
for I being Element of Segm 15
for x being Element of SCMPDS-Instr
for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,{},<*d1,k1,k2*>] holds
( x P31address = d1 & x P32const = k1 & x P33const = k2 )
proof
let I be Element of Segm 15; ::_thesis: for x being Element of SCMPDS-Instr
for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,{},<*d1,k1,k2*>] holds
( x P31address = d1 & x P32const = k1 & x P33const = k2 )
let x be Element of SCMPDS-Instr ; ::_thesis: for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,{},<*d1,k1,k2*>] holds
( x P31address = d1 & x P32const = k1 & x P33const = k2 )
let d1 be Element of SCM-Data-Loc ; ::_thesis: for k1, k2 being Integer st x = [I,{},<*d1,k1,k2*>] holds
( x P31address = d1 & x P32const = k1 & x P33const = k2 )
let k1, k2 be Integer; ::_thesis: ( x = [I,{},<*d1,k1,k2*>] implies ( x P31address = d1 & x P32const = k1 & x P33const = k2 ) )
k1 in INT by INT_1:def_2;
then A1: ( d1 is Element of SCM-Data-Loc \/ INT & k1 is Element of SCM-Data-Loc \/ INT ) by XBOOLE_0:def_3;
k2 in INT by INT_1:def_2;
then A2: k2 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def_3;
assume A3: x = [I,{},<*d1,k1,k2*>] ; ::_thesis: ( x P31address = d1 & x P32const = k1 & x P33const = k2 )
then consider f being FinSequence of SCM-Data-Loc \/ INT such that
A4: f = x `3_3 and
A5: x P31address = f /. 1 by Def6;
f = <*d1,k1,k2*> by A3, A4, RECDEF_2:def_3;
hence x P31address = d1 by A1, A2, A5, FINSEQ_4:18; ::_thesis: ( x P32const = k1 & x P33const = k2 )
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A6: f = x `3_3 and
A7: x P32const = f /. 2 by A3, Def7;
f = <*d1,k1,k2*> by A3, A6, RECDEF_2:def_3;
hence x P32const = k1 by A1, A2, A7, FINSEQ_4:18; ::_thesis: x P33const = k2
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A8: f = x `3_3 and
A9: x P33const = f /. 3 by A3, Def8;
f = <*d1,k1,k2*> by A3, A8, RECDEF_2:def_3;
hence x P33const = k2 by A1, A2, A9, FINSEQ_4:18; ::_thesis: verum
end;
definition
let x be Element of SCMPDS-Instr ;
given m1, m2 being Element of SCM-Data-Loc , k1, k2 being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*m1,m2,k1,k2*>] ;
funcx P41address -> Element of SCM-Data-Loc means :Def9: :: SCMPDS_I:def 9
ex f being FinSequence of SCM-Data-Loc \/ INT 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 \/ INT st
( f = x `3_3 & b1 = f /. 1 )
proof
reconsider mm = m1, m2 = m2, k1 = k1, k2 = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def_3;
take m1 ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & m1 = f /. 1 )
take f = <*mm,m2,k1,k2*>; ::_thesis: ( f = x `3_3 & m1 = f /. 1 )
thus f = x `3_3 by A1, RECDEF_2:def_3; ::_thesis: m1 = f /. 1
thus m1 = f /. 1 by FINSEQ_4:80; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) holds
b1 = b2 ;
funcx P42address -> Element of SCM-Data-Loc means :Def10: :: SCMPDS_I:def 10
ex f being FinSequence of SCM-Data-Loc \/ INT 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 \/ INT st
( f = x `3_3 & b1 = f /. 2 )
proof
reconsider m1 = m1, mm = m2, k1 = k1, k2 = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def_3;
take m2 ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & m2 = f /. 2 )
take f = <*m1,mm,k1,k2*>; ::_thesis: ( f = x `3_3 & m2 = f /. 2 )
thus f = x `3_3 by A1, RECDEF_2:def_3; ::_thesis: m2 = f /. 2
thus m2 = f /. 2 by FINSEQ_4:80; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) holds
b1 = b2 ;
funcx P43const -> Integer means :Def11: :: SCMPDS_I:def 11
ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & it = f /. 3 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 )
proof
reconsider m1 = m1, m2 = m2, mm = k1, k2 = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def_3;
take k1 ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & k1 = f /. 3 )
take f = <*m1,m2,mm,k2*>; ::_thesis: ( f = x `3_3 & k1 = f /. 3 )
thus f = x `3_3 by A1, RECDEF_2:def_3; ::_thesis: k1 = f /. 3
thus k1 = f /. 3 by FINSEQ_4:80; ::_thesis: verum
end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 3 ) holds
b1 = b2 ;
funcx P44const -> Integer means :Def12: :: SCMPDS_I:def 12
ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & it = f /. 4 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 4 )
proof
reconsider m1 = m1, m2 = m2, k1 = k1, mm = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def_3;
take k2 ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & k2 = f /. 4 )
take f = <*m1,m2,k1,mm*>; ::_thesis: ( f = x `3_3 & k2 = f /. 4 )
thus f = x `3_3 by A1, RECDEF_2:def_3; ::_thesis: k2 = f /. 4
thus k2 = f /. 4 by FINSEQ_4:80; ::_thesis: verum
end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 4 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 4 ) holds
b1 = b2 ;
end;
:: deftheorem Def9 defines P41address SCMPDS_I:def_9_:_
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,m2,k1,k2*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P41address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) );
:: deftheorem Def10 defines P42address SCMPDS_I:def_10_:_
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,m2,k1,k2*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P42address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) );
:: deftheorem Def11 defines P43const SCMPDS_I:def_11_:_
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,m2,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P43const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 3 ) );
:: deftheorem Def12 defines P44const SCMPDS_I:def_12_:_
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,m2,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P44const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 4 ) );
theorem :: SCMPDS_I:7
for I being Element of Segm 15
for x being Element of SCMPDS-Instr
for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,{},<*d1,d2,k1,k2*>] holds
( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
proof
let I be Element of Segm 15; ::_thesis: for x being Element of SCMPDS-Instr
for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,{},<*d1,d2,k1,k2*>] holds
( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
let x be Element of SCMPDS-Instr ; ::_thesis: for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,{},<*d1,d2,k1,k2*>] holds
( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
let d1, d2 be Element of SCM-Data-Loc ; ::_thesis: for k1, k2 being Integer st x = [I,{},<*d1,d2,k1,k2*>] holds
( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
let k1, k2 be Integer; ::_thesis: ( x = [I,{},<*d1,d2,k1,k2*>] implies ( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 ) )
A1: ( d1 is Element of SCM-Data-Loc \/ INT & d2 is Element of SCM-Data-Loc \/ INT ) by XBOOLE_0:def_3;
k1 in INT by INT_1:def_2;
then A2: k1 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def_3;
k2 in INT by INT_1:def_2;
then A3: k2 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def_3;
assume A4: x = [I,{},<*d1,d2,k1,k2*>] ; ::_thesis: ( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
then consider f being FinSequence of SCM-Data-Loc \/ INT such that
A5: f = x `3_3 and
A6: x P41address = f /. 1 by Def9;
f = <*d1,d2,k1,k2*> by A4, A5, RECDEF_2:def_3;
hence x P41address = d1 by A1, A2, A3, A6, FINSEQ_4:80; ::_thesis: ( x P42address = d2 & x P43const = k1 & x P44const = k2 )
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A7: f = x `3_3 and
A8: x P42address = f /. 2 by A4, Def10;
f = <*d1,d2,k1,k2*> by A4, A7, RECDEF_2:def_3;
hence x P42address = d2 by A1, A2, A3, A8, FINSEQ_4:80; ::_thesis: ( x P43const = k1 & x P44const = k2 )
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A9: f = x `3_3 and
A10: x P43const = f /. 3 by A4, Def11;
f = <*d1,d2,k1,k2*> by A4, A9, RECDEF_2:def_3;
hence x P43const = k1 by A1, A2, A3, A10, FINSEQ_4:80; ::_thesis: x P44const = k2
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A11: f = x `3_3 and
A12: x P44const = f /. 4 by A4, Def12;
f = <*d1,d2,k1,k2*> by A4, A11, RECDEF_2:def_3;
hence x P44const = k2 by A1, A2, A3, A12, FINSEQ_4:80; ::_thesis: verum
end;
definition
func RetSP -> Element of NAT equals :: SCMPDS_I:def 13
0 ;
coherence
0 is Element of NAT ;
func RetIC -> Element of NAT equals :: SCMPDS_I:def 14
1;
coherence
1 is Element of NAT ;
end;
:: deftheorem defines RetSP SCMPDS_I:def_13_:_
RetSP = 0 ;
:: deftheorem defines RetIC SCMPDS_I:def_14_:_
RetIC = 1;
theorem Th8: :: SCMPDS_I:8
for x being Element of SCMPDS-Instr holds
( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [14,{},<*l*>] where l is Element of INT : verum } & InsCode x = 14 ) or ( x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } & InsCode x = 1 ) or ( x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } & ( InsCode x = 2 or InsCode x = 3 ) ) or ( x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } & ( InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) ) or ( x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } & ( InsCode x = 9 or InsCode x = 10 or InsCode x = 11 or InsCode x = 12 or InsCode x = 13 ) ) )
proof
let x be Element of SCMPDS-Instr ; ::_thesis: ( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [14,{},<*l*>] where l is Element of INT : verum } & InsCode x = 14 ) or ( x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } & InsCode x = 1 ) or ( x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } & ( InsCode x = 2 or InsCode x = 3 ) ) or ( x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } & ( InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) ) or ( x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } & ( InsCode x = 9 or InsCode x = 10 or InsCode x = 11 or InsCode x = 12 or InsCode x = 13 ) ) )
( x in ((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by XBOOLE_0:def_3;
then ( x in (({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by XBOOLE_0:def_3;
then ( x in ({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } or x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by XBOOLE_0:def_3;
then ( x in {[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } or x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } or x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by XBOOLE_0:def_3;
percasesthen ( x in {[0,{},{}]} or x in { [14,{},<*l*>] where l is Element of INT : verum } or x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } or x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) 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 { [14,{},<*l*>] where l is Element of INT : verum } ; ::_thesis: InsCode x = 14
then ex l being Element of INT st x = [14,{},<*l*>] ;
hence InsCode x = 14 by RECDEF_2:def_1; ::_thesis: verum
end;
case x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; ::_thesis: InsCode x = 1
then ex sp being Element of SCM-Data-Loc st x = [1,{},<*sp*>] ;
hence InsCode x = 1 by RECDEF_2:def_1; ::_thesis: verum
end;
case x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ; ::_thesis: ( InsCode x = 2 or InsCode x = 3 )
then consider I being Element of Segm 15, v being Element of SCM-Data-Loc , c being Element of INT such that
A1: x = [I,{},<*v,c*>] and
A2: I in {2,3} ;
InsCode x = I by A1, RECDEF_2:def_1;
hence ( InsCode x = 2 or InsCode x = 3 ) by A2, TARSKI:def_2; ::_thesis: verum
end;
case x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ; ::_thesis: ( InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 )
then consider I being Element of Segm 15, v being Element of SCM-Data-Loc , c1, c2 being Element of INT such that
A3: x = [I,{},<*v,c1,c2*>] and
A4: I in {4,5,6,7,8} ;
InsCode x = I by A3, RECDEF_2:def_1;
hence ( InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) by A4, ENUMSET1:def_3; ::_thesis: verum
end;
case x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ; ::_thesis: ( InsCode x = 9 or InsCode x = 10 or InsCode x = 11 or InsCode x = 12 or InsCode x = 13 )
then consider I being Element of Segm 15, v1, v2 being Element of SCM-Data-Loc , c1, c2 being Element of INT such that
A5: x = [I,{},<*v1,v2,c1,c2*>] and
A6: I in {9,10,11,12,13} ;
InsCode x = I by A5, RECDEF_2:def_1;
hence ( InsCode x = 9 or InsCode x = 10 or InsCode x = 11 or InsCode x = 12 or InsCode x = 13 ) by A6, ENUMSET1:def_3; ::_thesis: verum
end;
end;
end;
begin
registration
cluster proj2 SCMPDS-Instr -> FinSequence-membered ;
coherence
proj2 SCMPDS-Instr is FinSequence-membered
proof
let f be set ; :: according to FINSEQ_1:def_18 ::_thesis: ( not f in proj2 SCMPDS-Instr or f is set )
assume f in proj2 SCMPDS-Instr ; ::_thesis: f is set
then consider y being set such that
A1: [y,f] in SCMPDS-Instr by XTUPLE_0:def_13;
set x = [y,f];
percases ( [y,f] in ((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or [y,f] in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by A1, XBOOLE_0:def_3;
supposeA2: [y,f] in ((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ; ::_thesis: f is set
percases ( [y,f] in (({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or [y,f] in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) by A2, XBOOLE_0:def_3;
suppose [y,f] in (({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ; ::_thesis: f is set
then [y,f] in ({[0,{},{}]} \/ ( { [14,{},<*l*>] where l is Element of INT : verum } \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } )) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } by XBOOLE_1:4;
then ( [y,f] in {[0,{},{}]} \/ ( { [14,{},<*l*>] where l is Element of INT : verum } \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) or [y,f] in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) by XBOOLE_0:def_3;
percasesthen ( [y,f] in {[0,{},{}]} or [y,f] in { [14,{},<*l*>] where l is Element of INT : verum } \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } or [y,f] in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) by XBOOLE_0:def_3;
suppose [y,f] in {[0,{},{}]} ; ::_thesis: f is set
then [y,f] = [0,{},{}] by TARSKI:def_1;
hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum
end;
supposeA3: [y,f] in { [14,{},<*l*>] where l is Element of INT : verum } \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; ::_thesis: f is set
percases ( [y,f] in { [14,{},<*l*>] where l is Element of INT : verum } or [y,f] in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) by A3, XBOOLE_0:def_3;
suppose [y,f] in { [14,{},<*l*>] where l is Element of INT : verum } ; ::_thesis: f is set
then ex l being Element of INT st [y,f] = [14,{},<*l*>] ;
hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum
end;
suppose [y,f] in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; ::_thesis: f is set
then ex sp being Element of SCM-Data-Loc st [y,f] = [1,{},<*sp*>] ;
hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
suppose [y,f] in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ; ::_thesis: f is set
then ex I being Element of Segm 15 ex v being Element of SCM-Data-Loc ex c being Element of INT st
( [y,f] = [I,{},<*v,c*>] & I in {2,3} ) ;
hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
suppose [y,f] in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ; ::_thesis: f is set
then ex I being Element of Segm 15 ex v being Element of SCM-Data-Loc ex c1, c2 being Element of INT st
( [y,f] = [I,{},<*v,c1,c2*>] & I in {4,5,6,7,8} ) ;
hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
suppose [y,f] in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ; ::_thesis: f is set
then ex I being Element of Segm 15 ex v1, v2 being Element of SCM-Data-Loc ex c1, c2 being Element of INT st
( [y,f] = [I,{},<*v1,v2,c1,c2*>] & I in {9,10,11,12,13} ) ;
hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
end;
registration
cluster SCMPDS-Instr -> standard-ins ;
coherence
SCMPDS-Instr is standard-ins
proof
consider X being non empty set such that
A1: proj2 SCMPDS-Instr c= X * by FINSEQ_1:85;
take X ; :: according to COMPOS_0:def_1 ::_thesis: SCMPDS-Instr c= [:NAT,(NAT *),(X *):]
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SCMPDS-Instr or x in [:NAT,(NAT *),(X *):] )
assume A2: x in SCMPDS-Instr ; ::_thesis: x in [:NAT,(NAT *),(X *):]
A3: {} in NAT * by FINSEQ_1:49;
percases ( x in ((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by A2, XBOOLE_0:def_3;
suppose x in ((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ; ::_thesis: x in [:NAT,(NAT *),(X *):]
percasesthen ( x in (({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) by XBOOLE_0:def_3;
supposeA4: x in (({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ; ::_thesis: x in [:NAT,(NAT *),(X *):]
percases ( x in ({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } or x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) by A4, XBOOLE_0:def_3;
supposeA5: x in ({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; ::_thesis: x in [:NAT,(NAT *),(X *):]
percases ( x in {[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } or x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) by A5, XBOOLE_0:def_3;
suppose x in {[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ; ::_thesis: x in [:NAT,(NAT *),(X *):]
percasesthen ( x in {[0,{},{}]} or x in { [14,{},<*l*>] where l is Element of INT : verum } ) by XBOOLE_0:def_3;
suppose x in {[0,{},{}]} ; ::_thesis: x in [:NAT,(NAT *),(X *):]
then A6: x = [0,{},{}] by TARSKI:def_1;
{} in X * by FINSEQ_1:49;
hence x in [:NAT,(NAT *),(X *):] by A6, A3, MCART_1:69; ::_thesis: verum
end;
suppose x in { [14,{},<*l*>] where l is Element of INT : verum } ; ::_thesis: x in [:NAT,(NAT *),(X *):]
then consider l being Element of INT such that
A7: x = [14,{},<*l*>] ;
<*l*> in proj2 SCMPDS-Instr by A2, A7, XTUPLE_0:def_13;
hence x in [:NAT,(NAT *),(X *):] by A1, A7, A3, MCART_1:69; ::_thesis: verum
end;
end;
end;
suppose x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; ::_thesis: x in [:NAT,(NAT *),(X *):]
then consider sp being Element of SCM-Data-Loc such that
A8: x = [1,{},<*sp*>] ;
<*sp*> in proj2 SCMPDS-Instr by A2, A8, XTUPLE_0:def_13;
hence x in [:NAT,(NAT *),(X *):] by A1, A8, A3, MCART_1:69; ::_thesis: verum
end;
end;
end;
suppose x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ; ::_thesis: x in [:NAT,(NAT *),(X *):]
then consider I being Element of Segm 15, v being Element of SCM-Data-Loc , c being Element of INT such that
A9: ( x = [I,{},<*v,c*>] & I in {2,3} ) ;
<*v,c*> in proj2 SCMPDS-Instr by A2, A9, XTUPLE_0:def_13;
hence x in [:NAT,(NAT *),(X *):] by A1, A9, A3, MCART_1:69; ::_thesis: verum
end;
end;
end;
suppose x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ; ::_thesis: x in [:NAT,(NAT *),(X *):]
then consider I being Element of Segm 15, v being Element of SCM-Data-Loc , c1, c2 being Element of INT such that
A10: ( x = [I,{},<*v,c1,c2*>] & I in {4,5,6,7,8} ) ;
<*v,c1,c2*> in proj2 SCMPDS-Instr by A2, A10, XTUPLE_0:def_13;
hence x in [:NAT,(NAT *),(X *):] by A1, A10, A3, MCART_1:69; ::_thesis: verum
end;
end;
end;
suppose x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ; ::_thesis: x in [:NAT,(NAT *),(X *):]
then consider I being Element of Segm 15, v1, v2 being Element of SCM-Data-Loc , c1, c2 being Element of INT such that
A11: ( x = [I,{},<*v1,v2,c1,c2*>] & I in {9,10,11,12,13} ) ;
<*v1,v2,c1,c2*> in proj2 SCMPDS-Instr by A2, A11, XTUPLE_0:def_13;
hence x in [:NAT,(NAT *),(X *):] by A1, A11, A3, MCART_1:69; ::_thesis: verum
end;
end;
end;
end;
Lm2: for l being Element of SCMPDS-Instr holds InsCode l <= 14
proof
let l be Element of SCMPDS-Instr ; ::_thesis: InsCode l <= 14
( 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 or InsCode l = 9 or InsCode l = 10 or InsCode l = 11 or InsCode l = 12 or InsCode l = 13 or InsCode l = 14 ) by Th8;
hence InsCode l <= 14 ; ::_thesis: verum
end;
Lm3: for i being Element of SCMPDS-Instr st InsCode i = 0 holds
JumpPart i = {}
proof
let i be Element of SCMPDS-Instr ; ::_thesis: ( InsCode i = 0 implies JumpPart i = {} )
assume InsCode i = 0 ; ::_thesis: JumpPart i = {}
then i in {[0,{},{}]} by Th8;
then i = [0,{},{}] by TARSKI:def_1;
hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum
end;
Lm4: for i being Element of SCMPDS-Instr st InsCode i = 14 holds
JumpPart i = {}
proof
let i be Element of SCMPDS-Instr ; ::_thesis: ( InsCode i = 14 implies JumpPart i = {} )
assume InsCode i = 14 ; ::_thesis: JumpPart i = {}
then i in { [14,{},<*l*>] where l is Element of INT : verum } by Th8;
then ex l being Element of INT st i = [14,{},<*l*>] ;
hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum
end;
Lm5: for i being Element of SCMPDS-Instr st InsCode i = 1 holds
JumpPart i = {}
proof
let i be Element of SCMPDS-Instr ; ::_thesis: ( InsCode i = 1 implies JumpPart i = {} )
assume InsCode i = 1 ; ::_thesis: JumpPart i = {}
then i in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } by Th8;
then ex sp being Element of SCM-Data-Loc st i = [1,{},<*sp*>] ;
hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum
end;
Lm6: for i being Element of SCMPDS-Instr st ( InsCode i = 2 or InsCode i = 3 ) holds
JumpPart i = {}
proof
let i be Element of SCMPDS-Instr ; ::_thesis: ( ( InsCode i = 2 or InsCode i = 3 ) implies JumpPart i = {} )
assume ( InsCode i = 2 or InsCode i = 3 ) ; ::_thesis: JumpPart i = {}
then i in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } by Th8;
then ex I being Element of Segm 15 ex v being Element of SCM-Data-Loc ex c being Element of INT st
( i = [I,{},<*v,c*>] & I in {2,3} ) ;
hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum
end;
Lm7: for i being Element of SCMPDS-Instr st ( InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) holds
JumpPart i = {}
proof
let i be Element of SCMPDS-Instr ; ::_thesis: ( ( InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) implies JumpPart i = {} )
assume ( InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) ; ::_thesis: JumpPart i = {}
then i in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } by Th8;
then ex I being Element of Segm 15 ex v being Element of SCM-Data-Loc ex c1, c2 being Element of INT st
( i = [I,{},<*v,c1,c2*>] & I in {4,5,6,7,8} ) ;
hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum
end;
Lm8: for i being Element of SCMPDS-Instr st ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) holds
JumpPart i = {}
proof
let i be Element of SCMPDS-Instr ; ::_thesis: ( ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) implies JumpPart i = {} )
assume ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) ; ::_thesis: JumpPart i = {}
then i in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } by Th8;
then ex I being Element of Segm 15 ex v1, v2 being Element of SCM-Data-Loc ex c1, c2 being Element of INT st
( i = [I,{},<*v1,v2,c1,c2*>] & I in {9,10,11,12,13} ) ;
hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum
end;
registration
cluster SCMPDS-Instr -> homogeneous ;
coherence
SCMPDS-Instr is homogeneous
proof
let i, j be Element of SCMPDS-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)
percases ( InsCode i = 0 or InsCode i = 14 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 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) by Lm2, NAT_1:60;
suppose InsCode i = 0 ; ::_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 = 14 ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm4;
hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
suppose InsCode i = 1 ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm5;
hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
suppose ( InsCode i = 2 or InsCode i = 3 ) ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm6;
hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
suppose ( InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm7;
hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
suppose ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm8;
hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
end;
end;
end;
registration
cluster SCMPDS-Instr -> J/A-independent ;
coherence
SCMPDS-Instr is J/A-independent
proof
let T be InsType of SCMPDS-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 SCMPDS-Instr or [T,b2,b3] in SCMPDS-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 SCMPDS-Instr or [T,f2,b1] in SCMPDS-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 SCMPDS-Instr or [T,f2,b1] in SCMPDS-Instr )
let p be set ; ::_thesis: ( not [T,f1,p] in SCMPDS-Instr or [T,f2,p] in SCMPDS-Instr )
assume A3: [T,f1,p] in SCMPDS-Instr ; ::_thesis: [T,f2,p] in SCMPDS-Instr
reconsider i = [T,f1,p] as Element of SCMPDS-Instr by A3;
( 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 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 or InsCode i = 14 ) by Lm2, NAT_1:60;
then A4: JumpPart i = {} by Lm4, Lm5, Lm6, Lm7, Lm8, Lm3;
T = InsCode i by RECDEF_2:def_1;
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 SCMPDS-Instr by A3; ::_thesis: verum
end;
end;
registration
cluster SCMPDS-Instr -> with_halt ;
coherence
SCMPDS-Instr is with_halt
proof
thus [0,{},{}] in SCMPDS-Instr by Lm1; :: according to COMPOS_0:def_10 ::_thesis: verum
end;
end;