:: SCMRING1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
cluster infinite -> non trivial set ;
coherence
for b1 being set st not b1 is finite holds
not b1 is trivial
proof end;
cluster infinite -> non trivial 1-sorted ;
coherence
for b1 being 1-sorted st not b1 is finite holds
not b1 is trivial
proof end;
end;

registration
cluster non empty trivial -> non empty Abelian add-associative right_zeroed right_complementable LoopStr ;
coherence
for b1 being non empty LoopStr st b1 is trivial holds
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable )
proof end;
cluster non empty trivial -> non empty right-distributive right_unital doubleLoopStr ;
coherence
for b1 being non empty doubleLoopStr st b1 is trivial holds
( b1 is right_unital & b1 is right-distributive )
proof end;
end;

registration
cluster -> natural Element of SCM-Data-Loc ;
coherence
for b1 being Element of SCM-Data-Loc holds b1 is natural by ORDINAL2:def 21;
end;

registration
cluster SCM-Instr -> non trivial ;
coherence
not SCM-Instr is trivial
proof end;
cluster SCM-Instr-Loc -> infinite non trivial ;
coherence
not SCM-Instr-Loc is finite
proof end;
end;

definition
let S be non empty 1-sorted ;
func SCM-Instr S -> Subset of [:(Segm 8),(((union {the carrier of S}) \/ NAT ) * ):] equals :: SCMRING1: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 SCM-Instr-Loc : verum } ) \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc , 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 SCM-Instr-Loc : verum } ) \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc , 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 Subset of [:(Segm 8),(((union {the carrier of S}) \/ NAT ) * ):]
proof end;
end;

:: deftheorem defines SCM-Instr SCMRING1: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 SCM-Instr-Loc : verum } ) \/ { [7,<*i,a*>] where i is Element of SCM-Instr-Loc , 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 trivial ;
coherence
not SCM-Instr S is trivial
proof end;
end;

definition
let S be non empty 1-sorted ;
attr S is good means :Def2: :: SCMRING1:def 2
( the carrier of S <> SCM-Instr-Loc & the carrier of S <> SCM-Instr S );
end;

:: deftheorem Def2 defines good SCMRING1:def 2 :
for S being non empty 1-sorted holds
( S is good iff ( the carrier of S <> SCM-Instr-Loc & the carrier of S <> SCM-Instr S ) );

registration
cluster non empty trivial -> non empty good 1-sorted ;
coherence
for b1 being non empty 1-sorted st b1 is trivial holds
b1 is good
proof end;
end;

registration
cluster strict non empty trivial good 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is strict & b1 is trivial & not b1 is empty )
proof end;
end;

registration
cluster non empty Abelian add-associative right_zeroed right_complementable strict right-distributive right_unital trivial good doubleLoopStr ;
existence
ex b1 being doubleLoopStr st
( b1 is strict & b1 is trivial & not b1 is empty )
proof end;
end;

registration
cluster strict trivial good doubleLoopStr ;
existence
ex b1 being Ring st
( b1 is strict & b1 is trivial )
proof end;
end;

Lm1: now
let k be Nat; :: thesis: ( k = 0 or ex j being Nat st k = (2 * j) + 1 or ex j being Nat st k = (2 * j) + 2 )
consider i being Nat such that
A1: ( k = 2 * i or k = (2 * i) + 1 ) by SCHEME1:1;
now
assume A2: k = 2 * i ; :: thesis: ( k = 0 or ex j being Nat st k = (2 * j) + 2 )
A3: ( i = 0 or ex j being Nat st i = j + 1 ) by NAT_1:22;
now
given j being Nat such that A4: i = j + 1 ; :: thesis: ex j being Nat st k = (2 * j) + (2 * 1)
take j = j; :: thesis: k = (2 * j) + (2 * 1)
thus k = (2 * j) + (2 * 1) by A2, A4; :: thesis: verum
end;
hence ( k = 0 or ex j being Nat st k = (2 * j) + 2 ) by A2, A3; :: thesis: verum
end;
hence ( k = 0 or ex j being Nat st k = (2 * j) + 1 or ex j being Nat st k = (2 * j) + 2 ) by A1; :: thesis: verum
end;

Lm2: now
let k be Nat; :: thesis: ( ( ex j being Nat st k = (2 * j) + 1 implies ( k <> 0 & ( for j being Nat holds not k = (2 * j) + 2 ) ) ) & ( ex j being Nat st k = (2 * j) + (1 + 1) implies ( k <> 0 & ( for i being Nat holds not k = (2 * i) + 1 ) ) ) )
thus ( ex j being Nat st k = (2 * j) + 1 implies ( k <> 0 & ( for j being Nat holds not k = (2 * j) + 2 ) ) ) :: thesis: ( ex j being Nat st k = (2 * j) + (1 + 1) implies ( k <> 0 & ( for i being Nat holds not k = (2 * i) + 1 ) ) )
proof
given j being Nat such that A1: k = (2 * j) + 1 ; :: thesis: ( k <> 0 & ( for j being Nat holds not k = (2 * j) + 2 ) )
thus k <> 0 by A1; :: thesis: for j being Nat holds not k = (2 * j) + 2
given i being Nat such that A2: k = (2 * i) + 2 ; :: thesis: contradiction
A3: (2 * i) + (2 * 1) = (2 * (i + 1)) + 0 ;
1 = ((2 * i) + 2) mod 2 by A1, A2, NAT_1:def 2
.= 0 by A3, NAT_1:def 2 ;
hence contradiction ; :: thesis: verum
end;
given j being Nat such that A4: k = (2 * j) + (1 + 1) ; :: thesis: ( k <> 0 & ( for i being Nat holds not k = (2 * i) + 1 ) )
thus k <> 0 by A4; :: thesis: for i being Nat holds not k = (2 * i) + 1
given i being Nat such that A5: k = (2 * i) + 1 ; :: thesis: contradiction
A6: (2 * j) + (2 * 1) = (2 * (j + 1)) + 0 ;
1 = ((2 * j) + 2) mod 2 by A4, A5, NAT_1:def 2
.= 0 by A6, NAT_1:def 2 ;
hence contradiction ; :: thesis: verum
end;

definition
let S be non empty 1-sorted ;
func SCM-OK S -> Function of NAT ,{the carrier of S} \/ {(SCM-Instr S),SCM-Instr-Loc } means :Def3: :: SCMRING1:def 3
( it . 0 = SCM-Instr-Loc & ( for k being Nat holds
( it . ((2 * k) + 1) = the carrier of S & it . ((2 * k) + 2) = SCM-Instr S ) ) );
existence
ex b1 being Function of NAT ,{the carrier of S} \/ {(SCM-Instr S),SCM-Instr-Loc } st
( b1 . 0 = SCM-Instr-Loc & ( for k being Nat holds
( b1 . ((2 * k) + 1) = the carrier of S & b1 . ((2 * k) + 2) = SCM-Instr S ) ) )
proof end;
uniqueness
for b1, b2 being Function of NAT ,{the carrier of S} \/ {(SCM-Instr S),SCM-Instr-Loc } st b1 . 0 = SCM-Instr-Loc & ( for k being Nat holds
( b1 . ((2 * k) + 1) = the carrier of S & b1 . ((2 * k) + 2) = SCM-Instr S ) ) & b2 . 0 = SCM-Instr-Loc & ( for k being Nat holds
( b2 . ((2 * k) + 1) = the carrier of S & b2 . ((2 * k) + 2) = SCM-Instr S ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines SCM-OK SCMRING1:def 3 :
for S being non empty 1-sorted
for b2 being Function of NAT ,{the carrier of S} \/ {(SCM-Instr S),SCM-Instr-Loc } holds
( b2 = SCM-OK S iff ( b2 . 0 = SCM-Instr-Loc & ( for k being Nat holds
( b2 . ((2 * k) + 1) = the carrier of S & b2 . ((2 * k) + 2) = SCM-Instr S ) ) ) );

definition
let S be non empty 1-sorted ;
mode SCM-State of S is Element of product (SCM-OK S);
end;

theorem Th1: :: SCMRING1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty 1-sorted holds SCM-Instr-Loc <> SCM-Instr S
proof end;

theorem Th2: :: SCMRING1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for G being non empty good 1-sorted holds
( (SCM-OK G) . i = SCM-Instr-Loc iff i = 0 )
proof end;

theorem Th3: :: SCMRING1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for G being non empty good 1-sorted holds
( (SCM-OK G) . i = the carrier of G iff ex k being Nat st i = (2 * k) + 1 )
proof end;

theorem Th4: :: SCMRING1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for G being non empty good 1-sorted holds
( (SCM-OK G) . i = SCM-Instr G iff ex k being Nat st i = (2 * k) + 2 )
proof end;

theorem Th5: :: SCMRING1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for d1 being Element of SCM-Data-Loc
for G being non empty good 1-sorted holds (SCM-OK G) . d1 = the carrier of G
proof end;

theorem Th6: :: SCMRING1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1 being Element of SCM-Instr-Loc
for G being non empty good 1-sorted holds (SCM-OK G) . i1 = SCM-Instr G
proof end;

theorem Th7: :: SCMRING1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty 1-sorted holds pi (product (SCM-OK S)),0 = SCM-Instr-Loc
proof end;

theorem Th8: :: SCMRING1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for d1 being Element of SCM-Data-Loc
for G being non empty good 1-sorted holds pi (product (SCM-OK G)),d1 = the carrier of G
proof end;

theorem :: SCMRING1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1 being Element of SCM-Instr-Loc
for G being non empty good 1-sorted holds pi (product (SCM-OK G)),i1 = SCM-Instr G
proof end;

definition
let S be non empty 1-sorted ;
let s be SCM-State of S;
func IC s -> Element of SCM-Instr-Loc equals :: SCMRING1:def 4
s . 0;
coherence
s . 0 is Element of SCM-Instr-Loc
proof end;
end;

:: deftheorem defines IC SCMRING1:def 4 :
for S being non empty 1-sorted
for s being SCM-State of S holds IC s = s . 0;

definition
let R be non empty good 1-sorted ;
let s be SCM-State of R;
let u be Element of SCM-Instr-Loc ;
func SCM-Chg s,u -> SCM-State of R equals :: SCMRING1:def 5
s +* (0 .--> u);
coherence
s +* (0 .--> u) is SCM-State of R
proof end;
end;

:: deftheorem defines SCM-Chg SCMRING1:def 5 :
for R being non empty good 1-sorted
for s being SCM-State of R
for u being Element of SCM-Instr-Loc holds SCM-Chg s,u = s +* (0 .--> u);

theorem :: SCMRING1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty good 1-sorted
for s being SCM-State of G
for u being Element of SCM-Instr-Loc holds (SCM-Chg s,u) . 0 = u
proof end;

theorem :: SCMRING1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty good 1-sorted
for s being SCM-State of G
for u being Element of SCM-Instr-Loc
for mk being Element of SCM-Data-Loc holds (SCM-Chg s,u) . mk = s . mk
proof end;

theorem :: SCMRING1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty good 1-sorted
for s being SCM-State of G
for u, v being Element of SCM-Instr-Loc holds (SCM-Chg s,u) . v = s . v
proof end;

definition
let R be non empty good 1-sorted ;
let s be SCM-State of R;
let t be Element of SCM-Data-Loc ;
let u be Element of R;
func SCM-Chg s,t,u -> SCM-State of R equals :: SCMRING1:def 6
s +* (t .--> u);
coherence
s +* (t .--> u) is SCM-State of R
proof end;
end;

:: deftheorem defines SCM-Chg SCMRING1:def 6 :
for R being non empty good 1-sorted
for s being SCM-State of R
for t being Element of SCM-Data-Loc
for u being Element of R holds SCM-Chg s,t,u = s +* (t .--> u);

theorem :: SCMRING1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty good 1-sorted
for s being SCM-State of G
for t being Element of SCM-Data-Loc
for u being Element of G holds (SCM-Chg s,t,u) . 0 = s . 0
proof end;

theorem :: SCMRING1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty good 1-sorted
for s being SCM-State of G
for t being Element of SCM-Data-Loc
for u being Element of G holds (SCM-Chg s,t,u) . t = u
proof end;

theorem :: SCMRING1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty good 1-sorted
for s being SCM-State of G
for t being Element of SCM-Data-Loc
for u being Element of G
for mk being Element of SCM-Data-Loc st mk <> t holds
(SCM-Chg s,t,u) . mk = s . mk
proof end;

theorem :: SCMRING1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty good 1-sorted
for s being SCM-State of G
for t being Element of SCM-Data-Loc
for u being Element of G
for v being Element of SCM-Instr-Loc holds (SCM-Chg s,t,u) . v = s . v
proof end;

definition
let R be non empty good 1-sorted ;
let s be SCM-State of R;
let a be Element of SCM-Data-Loc ;
:: original: .
redefine func s . a -> Element of R;
coherence
s . a is Element of R
proof 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*>] ;
func x address_1 -> Element of SCM-Data-Loc means :Def7: :: SCMRING1:def 7
 ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & b1 = f /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & b2 = f /. 1 ) holds
b1 = b2 ;
func x address_2 -> Element of SCM-Data-Loc means :Def8: :: SCMRING1:def 8
 ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & it = f /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & b1 = f /. 2 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & b2 = f /. 2 ) holds
b1 = b2 ;
end;

:: deftheorem Def7 defines address_1 SCMRING1:def 7 :
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 `2 & b3 = f /. 1 ) );

:: deftheorem Def8 defines address_2 SCMRING1:def 8 :
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 `2 & b3 = f /. 2 ) );

theorem :: SCMRING1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let R be non empty 1-sorted ;
let x be Element of SCM-Instr R;
given mk being Element of SCM-Instr-Loc , I being Element of Segm 8 such that A1: x = [I,<*mk*>] ;
func x jump_address -> Element of SCM-Instr-Loc means :Def9: :: SCMRING1:def 9
 ex f being FinSequence of SCM-Instr-Loc st
( f = x `2 & it = f /. 1 );
existence
ex b1 being Element of SCM-Instr-Loc ex f being FinSequence of SCM-Instr-Loc st
( f = x `2 & b1 = f /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Instr-Loc st ex f being FinSequence of SCM-Instr-Loc st
( f = x `2 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Instr-Loc st
( f = x `2 & b2 = f /. 1 ) holds
b1 = b2 ;
end;

:: deftheorem Def9 defines jump_address SCMRING1:def 9 :
for R being non empty 1-sorted
for x being Element of SCM-Instr R st ex mk being Element of SCM-Instr-Loc ex I being Element of Segm 8 st x = [I,<*mk*>] holds
for b3 being Element of SCM-Instr-Loc holds
( b3 = x jump_address iff ex f being FinSequence of SCM-Instr-Loc st
( f = x `2 & b3 = f /. 1 ) );

theorem :: SCMRING1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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-Instr-Loc st x = [I,<*mk*>] holds
x jump_address = mk
proof end;

definition
let S be non empty 1-sorted ;
let x be Element of SCM-Instr S;
given mk being Element of SCM-Instr-Loc , ml being Element of SCM-Data-Loc , I being Element of Segm 8 such that A1: x = [I,<*mk,ml*>] ;
func x cjump_address -> Element of SCM-Instr-Loc means :Def10: :: SCMRING1:def 10
 ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & it = <*mk,ml*> /. 1 );
existence
ex b1, mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b1 = <*mk,ml*> /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Instr-Loc st ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b1 = <*mk,ml*> /. 1 ) & ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b2 = <*mk,ml*> /. 1 ) holds
b1 = b2 ;
func x cond_address -> Element of SCM-Data-Loc means :Def11: :: SCMRING1:def 11
 ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & it = <*mk,ml*> /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b1 = <*mk,ml*> /. 2 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b1 = <*mk,ml*> /. 2 ) & ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b2 = <*mk,ml*> /. 2 ) holds
b1 = b2 ;
end;

:: deftheorem Def10 defines cjump_address SCMRING1:def 10 :
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of SCM-Instr-Loc 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-Instr-Loc holds
( b3 = x cjump_address iff ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b3 = <*mk,ml*> /. 1 ) );

:: deftheorem Def11 defines cond_address SCMRING1:def 11 :
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of SCM-Instr-Loc 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 mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b3 = <*mk,ml*> /. 2 ) );

theorem :: SCMRING1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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-Instr-Loc
for ml being Element of SCM-Data-Loc st x = [I,<*mk,ml*>] holds
( x cjump_address = mk & x cond_address = ml )
proof 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 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*>] ;
func x const_address -> Element of SCM-Data-Loc means :Def12: :: SCMRING1:def 12
 ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `2 & 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 `2 & b1 = f /. 1 )
proof 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 `2 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `2 & b2 = f /. 1 ) holds
b1 = b2 ;
func x const_value -> Element of S means :Def13: :: SCMRING1:def 13
 ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `2 & 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 `2 & b1 = f /. 2 )
proof 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 `2 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `2 & b2 = f /. 2 ) holds
b1 = b2 ;
end;

:: deftheorem Def12 defines const_address SCMRING1:def 12 :
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 `2 & b3 = f /. 1 ) );

:: deftheorem Def13 defines const_value SCMRING1:def 13 :
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 `2 & b3 = f /. 2 ) );

theorem :: SCMRING1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let R be good Ring;
let x be Element of SCM-Instr R;
let s be SCM-State of R;
func SCM-Exec-Res x,s -> SCM-State of R equals :: SCMRING1:def 14
 SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(Next (IC s)) if ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>]
SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(Next (IC s)) if ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>]
SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(Next (IC s)) if ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>]
SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(Next (IC s)) if ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>]
SCM-Chg s,(x jump_address ) if ex mk being Element of SCM-Instr-Loc st x = [6,<*mk*>]
SCM-Chg s,(IFEQ (s . (x cond_address )),(0. R),(x cjump_address ),(Next (IC s))) if ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>]
SCM-Chg (SCM-Chg s,(x const_address ),(x const_value )),(Next (IC s)) if ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,<*mk,r*>]
otherwise s;
coherence
( ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] implies SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(Next (IC s)) is SCM-State of R ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] implies SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(Next (IC s)) is SCM-State of R ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] implies SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(Next (IC s)) is SCM-State of R ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] implies SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(Next (IC s)) is SCM-State of R ) & ( ex mk being Element of SCM-Instr-Loc st x = [6,<*mk*>] implies SCM-Chg s,(x jump_address ) is SCM-State of R ) & ( ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] implies SCM-Chg s,(IFEQ (s . (x cond_address )),(0. R),(x cjump_address ),(Next (IC s))) is SCM-State of R ) & ( ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,<*mk,r*>] implies SCM-Chg (SCM-Chg s,(x const_address ),(x const_value )),(Next (IC s)) is SCM-State of R ) & ( ( for mk, ml being Element of SCM-Data-Loc holds not x = [1,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [2,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [3,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [4,<*mk,ml*>] ) & ( for mk being Element of SCM-Instr-Loc holds not x = [6,<*mk*>] ) & ( for mk being Element of SCM-Instr-Loc
for ml being Element of SCM-Data-Loc holds not x = [7,<*mk,ml*>] ) & ( for mk being Element of SCM-Data-Loc
for r being Element of R holds not x = [5,<*mk,r*>] ) implies s is SCM-State of R ) ) ;
consistency
for b1 being SCM-State of R holds
( ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(Next (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(Next (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(Next (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] & ex mk being Element of SCM-Instr-Loc st x = [6,<*mk*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(Next (IC s)) iff b1 = SCM-Chg s,(x jump_address ) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] & ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(Next (IC s)) iff b1 = SCM-Chg s,(IFEQ (s . (x cond_address )),(0. R),(x cjump_address ),(Next (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] & ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,<*mk,r*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x const_address ),(x const_value )),(Next (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(Next (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(Next (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] & ex mk being Element of SCM-Instr-Loc st x = [6,<*mk*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(Next (IC s)) iff b1 = SCM-Chg s,(x jump_address ) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] & ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(Next (IC s)) iff b1 = SCM-Chg s,(IFEQ (s . (x cond_address )),(0. R),(x cjump_address ),(Next (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] & ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,<*mk,r*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x const_address ),(x const_value )),(Next (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(Next (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] & ex mk being Element of SCM-Instr-Loc st x = [6,<*mk*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(Next (IC s)) iff b1 = SCM-Chg s,(x jump_address ) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] & ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(Next (IC s)) iff b1 = SCM-Chg s,(IFEQ (s . (x cond_address )),(0. R),(x cjump_address ),(Next (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] & ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,<*mk,r*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x const_address ),(x const_value )),(Next (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] & ex mk being Element of SCM-Instr-Loc st x = [6,<*mk*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(Next (IC s)) iff b1 = SCM-Chg s,(x jump_address ) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] & ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(Next (IC s)) iff b1 = SCM-Chg s,(IFEQ (s . (x cond_address )),(0. R),(x cjump_address ),(Next (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] & ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,<*mk,r*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x const_address ),(x const_value )),(Next (IC s)) ) ) & ( ex mk being Element of SCM-Instr-Loc st x = [6,<*mk*>] & ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] implies ( b1 = SCM-Chg s,(x jump_address ) iff b1 = SCM-Chg s,(IFEQ (s . (x cond_address )),(0. R),(x cjump_address ),(Next (IC s))) ) ) & ( ex mk being Element of SCM-Instr-Loc st x = [6,<*mk*>] & ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,<*mk,r*>] implies ( b1 = SCM-Chg s,(x jump_address ) iff b1 = SCM-Chg (SCM-Chg s,(x const_address ),(x const_value )),(Next (IC s)) ) ) & ( ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] & ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,<*mk,r*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (x cond_address )),(0. R),(x cjump_address ),(Next (IC s))) iff b1 = SCM-Chg (SCM-Chg s,(x const_address ),(x const_value )),(Next (IC s)) ) ) ) by ZFMISC_1:33;
end;

:: deftheorem defines SCM-Exec-Res SCMRING1:def 14 :
for R being good Ring
for x being Element of SCM-Instr R
for s being SCM-State of R holds
( ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(Next (IC s)) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(Next (IC s)) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(Next (IC s)) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(Next (IC s)) ) & ( ex mk being Element of SCM-Instr-Loc st x = [6,<*mk*>] implies SCM-Exec-Res x,s = SCM-Chg s,(x jump_address ) ) & ( ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] implies SCM-Exec-Res x,s = SCM-Chg s,(IFEQ (s . (x cond_address )),(0. R),(x cjump_address ),(Next (IC s))) ) & ( ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,<*mk,r*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(x const_address ),(x const_value )),(Next (IC s)) ) & ( ( for mk, ml being Element of SCM-Data-Loc holds not x = [1,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [2,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [3,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [4,<*mk,ml*>] ) & ( for mk being Element of SCM-Instr-Loc holds not x = [6,<*mk*>] ) & ( for mk being Element of SCM-Instr-Loc
for ml being Element of SCM-Data-Loc holds not x = [7,<*mk,ml*>] ) & ( for mk being Element of SCM-Data-Loc
for r being Element of R holds not x = [5,<*mk,r*>] ) implies SCM-Exec-Res x,s = s ) );

registration
let S be non empty 1-sorted ;
let f be Function of SCM-Instr S, Funcs (product (SCM-OK S)),(product (SCM-OK S));
let x be Element of SCM-Instr S;
cluster f . x -> Relation-like Function-like ;
coherence
( f . x is Function-like & f . x is Relation-like ) ;
end;

definition
let R be good Ring;
func SCM-Exec R -> Function of SCM-Instr R, Funcs (product (SCM-OK R)),(product (SCM-OK R)) means :: SCMRING1:def 15
for x being Element of SCM-Instr R
for y being SCM-State of R holds (it . x) . y = SCM-Exec-Res x,y;
existence
ex b1 being Function of SCM-Instr R, Funcs (product (SCM-OK R)),(product (SCM-OK R)) st
for x being Element of SCM-Instr R
for y being SCM-State of R holds (b1 . x) . y = SCM-Exec-Res x,y
proof end;
uniqueness
for b1, b2 being Function of SCM-Instr R, Funcs (product (SCM-OK R)),(product (SCM-OK R)) st ( for x being Element of SCM-Instr R
for y being SCM-State of R holds (b1 . x) . y = SCM-Exec-Res x,y ) & ( for x being Element of SCM-Instr R
for y being SCM-State of R holds (b2 . x) . y = SCM-Exec-Res x,y ) holds
b1 = b2
proof end;
end;

:: deftheorem defines SCM-Exec SCMRING1:def 15 :
for R being good Ring
for b2 being Function of SCM-Instr R, Funcs (product (SCM-OK R)),(product (SCM-OK R)) holds
( b2 = SCM-Exec R iff for x being Element of SCM-Instr R
for y being SCM-State of R holds (b2 . x) . y = SCM-Exec-Res x,y );