:: Composition of Machines, Instructions and Programs
:: by Andrzej Trybulec
::
:: Received May 20, 2010
:: Copyright (c) 2010 Association of Mizar Users


begin

definition
let N be set ;
attr c2 is strict ;
struct COM-Struct of N -> 1-sorted ;
aggr COM-Struct(# carrier, Instruction-Counter, Instructions, haltF, Object-Kind #) -> COM-Struct of N;
sel Instruction-Counter c2 -> Element of the carrier of c2;
sel Instructions c2 -> non empty set ;
sel haltF c2 -> Element of the Instructions of c2;
sel Object-Kind c2 -> Function of the carrier of c2,(N \/ {the Instructions of c2,NAT });
end;

definition
let N be set ;
func Trivial-COM N -> strict COM-Struct of N means :Def2: :: COMPOS_1:def 1
( the carrier of it = succ NAT & the Instruction-Counter of it = NAT & the Instructions of it = {[0 ,{} ,{} ]} & the haltF of it = [0 ,{} ,{} ] & the Object-Kind of it = (NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT ) );
existence
ex b1 being strict COM-Struct of N st
( the carrier of b1 = succ NAT & the Instruction-Counter of b1 = NAT & the Instructions of b1 = {[0 ,{} ,{} ]} & the haltF of b1 = [0 ,{} ,{} ] & the Object-Kind of b1 = (NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT ) )
proof end;
uniqueness
for b1, b2 being strict COM-Struct of N st the carrier of b1 = succ NAT & the Instruction-Counter of b1 = NAT & the Instructions of b1 = {[0 ,{} ,{} ]} & the haltF of b1 = [0 ,{} ,{} ] & the Object-Kind of b1 = (NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT ) & the carrier of b2 = succ NAT & the Instruction-Counter of b2 = NAT & the Instructions of b2 = {[0 ,{} ,{} ]} & the haltF of b2 = [0 ,{} ,{} ] & the Object-Kind of b2 = (NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT ) holds
b1 = b2 ;
end;

:: deftheorem Def2 defines Trivial-COM COMPOS_1:def 1 :
for N being set
for b2 being strict COM-Struct of N holds
( b2 = Trivial-COM N iff ( the carrier of b2 = succ NAT & the Instruction-Counter of b2 = NAT & the Instructions of b2 = {[0 ,{} ,{} ]} & the haltF of b2 = [0 ,{} ,{} ] & the Object-Kind of b2 = (NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT ) ) );

definition
let N be set ;
let S be COM-Struct of N;
attr S is stored-program means :Def3: :: COMPOS_1:def 2
 NAT c= the carrier of S;
end;

:: deftheorem Def3 defines stored-program COMPOS_1:def 2 :
for N being set
for S being COM-Struct of N holds
( S is stored-program iff NAT c= the carrier of S );

registration
let N be set ;
cluster Trivial-COM N -> non empty strict stored-program ;
coherence
( not Trivial-COM N is empty & Trivial-COM N is stored-program )
proof end;
end;

registration
let N be set ;
cluster non empty stored-program COM-Struct of N;
existence
ex b1 being COM-Struct of N st
( not b1 is empty & b1 is stored-program )
proof end;
end;

definition
let N be set ;
let S be non empty COM-Struct of N;
mode Object of S is Element of S;
end;

definition
let N be set ;
let S be COM-Struct of N;
mode Instruction of S is Element of the Instructions of S;
end;

definition
let N be set ;
let S be non empty COM-Struct of N;
func IC S -> Object of S equals :: COMPOS_1:def 3
the Instruction-Counter of S;
correctness
coherence
the Instruction-Counter of S is Object of S;
;
end;

:: deftheorem defines IC COMPOS_1:def 3 :
for N being set
for S being non empty COM-Struct of N holds IC S = the Instruction-Counter of S;

definition
let N be set ;
let S be non empty COM-Struct of N;
let o be Object of S;
func ObjectKind o -> Element of N \/ {the Instructions of S,NAT } equals :: COMPOS_1:def 4
the Object-Kind of S . o;
correctness
coherence
the Object-Kind of S . o is Element of N \/ {the Instructions of S,NAT };
;
end;

:: deftheorem defines ObjectKind COMPOS_1:def 4 :
for N being set
for S being non empty COM-Struct of N
for o being Object of S holds ObjectKind o = the Object-Kind of S . o;

definition
let N be set ;
let S be COM-Struct of N;
mode PartState of S is the carrier of S -defined the Object-Kind of S -compatible Function;
end;

definition
let N be set ;
let S be COM-Struct of N;
mode FinPartState of S is finite PartState of S;
end;

definition
let N be with_non-empty_elements set ;
let S be COM-Struct of N;
mode State of S is total PartState of S;
end;

definition
let N be set ;
let S be COM-Struct of N;
func halt S -> Instruction of S equals :: COMPOS_1:def 5
the haltF of S;
coherence
the haltF of S is Instruction of S ;
end;

:: deftheorem defines halt COMPOS_1:def 5 :
for N being set
for S being COM-Struct of N holds halt S = the haltF of S;

definition
let N be set ;
let IT be non empty COM-Struct of N;
attr IT is IC-Ins-separated means :Def11: :: COMPOS_1:def 6
 ObjectKind (IC IT) = NAT ;
end;

:: deftheorem Def11 defines IC-Ins-separated COMPOS_1:def 6 :
for N being set
for IT being non empty COM-Struct of N holds
( IT is IC-Ins-separated iff ObjectKind (IC IT) = NAT );

definition
let N be with_non-empty_elements set ;
let S be COM-Struct of N;
let I be NAT -defined the Instructions of S -valued Function;
attr I is halt-free means :: COMPOS_1:def 7
not halt S in rng I;
end;

:: deftheorem defines halt-free COMPOS_1:def 7 :
for N being with_non-empty_elements set
for S being COM-Struct of N
for I being NAT -defined the Instructions of b2 -valued Function holds
( I is halt-free iff not halt S in rng I );

definition
let N be set ;
let IT be non empty stored-program COM-Struct of N;
attr IT is definite means :Def14: :: COMPOS_1:def 8
for l being Element of NAT holds the Object-Kind of IT . l = the Instructions of IT;
end;

:: deftheorem Def14 defines definite COMPOS_1:def 8 :
for N being set
for IT being non empty stored-program COM-Struct of N holds
( IT is definite iff for l being Element of NAT holds the Object-Kind of IT . l = the Instructions of IT );

registration
let E be set ;
cluster Trivial-COM E -> strict IC-Ins-separated definite ;
coherence
( Trivial-COM E is IC-Ins-separated & Trivial-COM E is definite )
proof end;
end;

registration
let M be set ;
cluster non empty strict stored-program IC-Ins-separated definite COM-Struct of M;
existence
ex b1 being non empty stored-program COM-Struct of M st
( b1 is IC-Ins-separated & b1 is definite & b1 is strict )
proof end;
end;

registration
let N be with_non-empty_elements set ;
cluster non empty strict stored-program IC-Ins-separated definite COM-Struct of N;
existence
ex b1 being non empty stored-program COM-Struct of N st
( b1 is IC-Ins-separated & b1 is definite & b1 is strict )
proof end;
end;

definition
let N be with_non-empty_elements set ;
let S be non empty IC-Ins-separated COM-Struct of N;
let p be PartState of S;
func IC p -> Element of NAT equals :: COMPOS_1:def 9
p . (IC S);
coherence
p . (IC S) is Element of NAT
proof end;
end;

:: deftheorem defines IC COMPOS_1:def 9 :
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for p being PartState of S holds IC p = p . (IC S);

theorem :: COMPOS_1:1
for N being with_non-empty_elements set
for s1, s2 being State of (Trivial-COM N) st IC s1 = IC s2 holds
s1 = s2
proof end;

begin

definition
let N be with_non-empty_elements set ;
let S be non empty IC-Ins-separated COM-Struct of N;
let p be the Instructions of S -valued Function;
let s be State of S;
func CurInstr p,s -> Instruction of S equals :: COMPOS_1:def 10
p /. (IC s);
coherence
p /. (IC s) is Instruction of S ;
end;

:: deftheorem defines CurInstr COMPOS_1:def 10 :
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for p being the Instructions of b2 -valued Function
for s being State of S holds CurInstr p,s = p /. (IC s);

definition
let N be with_non-empty_elements set ;
let S be COM-Struct of N;
let s be PartState of S;
func ProgramPart s -> PartState of S equals :: COMPOS_1:def 11
s | NAT ;
coherence
s | NAT is PartState of S ;
end;

:: deftheorem defines ProgramPart COMPOS_1:def 11 :
for N being with_non-empty_elements set
for S being COM-Struct of N
for s being PartState of S holds ProgramPart s = s | NAT ;

registration
let N be with_non-empty_elements set ;
let S be COM-Struct of N;
let s be PartState of S;
cluster ProgramPart s -> NAT -defined ;
coherence
ProgramPart s is NAT -defined ;
end;

BWL: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite COM-Struct of N
for s being State of S
for i being natural number holds (ProgramPart s) . i = s . i
proof end;

BWL2: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite COM-Struct of N
for s being PartState of S
for i being natural number st i in dom s holds
(ProgramPart s) . i = s . i
proof end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N;
let s be PartState of S;
cluster ProgramPart s -> the Instructions of S -valued ;
coherence
ProgramPart s is the Instructions of S -valued
proof end;
end;

LmU: for N being with_non-empty_elements set
for S being non empty stored-program COM-Struct of N
for s being State of S holds dom (ProgramPart s) = NAT
proof end;

BWL1: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite COM-Struct of N
for s being State of S
for i being natural number holds (ProgramPart s) /. i = s . i
proof end;

definition
let N be set ;
let IT be COM-Struct of N;
attr IT is realistic means :Def21: :: COMPOS_1:def 12
not the Instruction-Counter of IT in NAT ;
end;

:: deftheorem Def21 defines realistic COMPOS_1:def 12 :
for N being set
for IT being COM-Struct of N holds
( IT is realistic iff not the Instruction-Counter of IT in NAT );

theorem :: COMPOS_1:2
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite COM-Struct of N
for s being State of S
for i being natural number holds (ProgramPart s) . i = s . i by BWL;

theorem :: COMPOS_1:3
for E being set
for S being non empty IC-Ins-separated COM-Struct of E st S is realistic holds
for l being Element of NAT holds not IC S = l by Def21;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program definite COM-Struct of N;
let s be State of S;
let l be Element of NAT ;
:: original: .
redefine func s . l -> Instruction of S;
coherence
s . l is Instruction of S
proof end;
end;

registration
let N be with_non-empty_elements set ;
let S be COM-Struct of N;
let p be FinPartState of S;
cluster ProgramPart p -> finite ;
coherence
ProgramPart p is finite ;
end;

registration
let N be with_non-empty_elements set ;
let S be COM-Struct of N;
let p be PartState of S;
cluster ProgramPart p -> NAT -defined ;
coherence
ProgramPart p is NAT -defined ;
end;

LmL: for N being with_non-empty_elements set
for S being stored-program COM-Struct of N
for s being State of S holds NAT c= dom s
proof end;

registration
let N be with_non-empty_elements set ;
let S be stored-program COM-Struct of N;
let s be State of S;
cluster ProgramPart s -> total ;
coherence
ProgramPart s is total
proof end;
end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N;
let P be the Instructions of S -valued ManySortedSet of NAT ;
let k be Nat;
:: original: .
redefine func P . k -> Instruction of S;
coherence
P . k is Instruction of S
proof end;
end;

L94: for N being with_non-empty_elements set
for S being non empty COM-Struct of N
for s being State of S holds IC S in dom s
proof end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty COM-Struct of N;
let o be Object of S;
cluster ObjectKind o -> non empty ;
coherence
not ObjectKind o is empty ;
end;

begin

definition
let N be set ;
let S be COM-Struct of N;
func FinPartSt S -> Subset of (sproduct the Object-Kind of S) equals :: COMPOS_1:def 13
{ p where p is Element of sproduct the Object-Kind of S : p is finite } ;
coherence
{ p where p is Element of sproduct the Object-Kind of S : p is finite } is Subset of (sproduct the Object-Kind of S)
proof end;
end;

:: deftheorem defines FinPartSt COMPOS_1:def 13 :
for N being set
for S being COM-Struct of N holds FinPartSt S = { p where p is Element of sproduct the Object-Kind of S : p is finite } ;

definition
let N be set ;
let S be non empty COM-Struct of N;
func Data-Locations S -> set equals :: COMPOS_1:def 14
the carrier of S \ ({(IC S)} \/ NAT );
coherence
the carrier of S \ ({(IC S)} \/ NAT ) is set ;
end;

:: deftheorem defines Data-Locations COMPOS_1:def 14 :
for N being set
for S being non empty COM-Struct of N holds Data-Locations S = the carrier of S \ ({(IC S)} \/ NAT );

theorem Th58: :: COMPOS_1:4
for N being non empty with_non-empty_elements set
for S being non empty COM-Struct of N
for A, B being set
for la, lb being Object of S st ObjectKind la = A & ObjectKind lb = B holds
for a being Element of A
for b being Element of B holds la,lb --> a,b is FinPartState of S
proof end;

theorem Th59: :: COMPOS_1:5
for N being non empty with_non-empty_elements set
for S being non empty COM-Struct of N
for A being set
for la being Object of S st the Object-Kind of S . la = A holds
for a being Element of A holds la .--> a is FinPartState of S
proof end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N;
let la be Object of S;
let a be Element of ObjectKind la;
:: original: .-->
redefine func la .--> a -> FinPartState of S;
coherence
la .--> a is FinPartState of S by Th59;
end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N;
let la, lb be Object of S;
let a be Element of ObjectKind la;
let b be Element of ObjectKind lb;
:: original: -->
redefine func la,lb --> a,b -> FinPartState of S;
coherence
la,lb --> a,b is FinPartState of S by Th58;
end;

registration
let E be set ;
cluster Trivial-COM E -> strict realistic ;
coherence
Trivial-COM E is realistic
proof end;
end;

registration
let E be set ;
cluster strict realistic COM-Struct of E;
existence
ex b1 being COM-Struct of E st
( b1 is realistic & b1 is strict )
proof end;
end;

registration
let M be set ;
cluster non empty strict stored-program IC-Ins-separated definite realistic COM-Struct of M;
existence
ex b1 being non empty stored-program COM-Struct of M st
( b1 is realistic & b1 is strict & b1 is IC-Ins-separated & b1 is definite )
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
cluster non empty strict stored-program IC-Ins-separated definite realistic COM-Struct of N;
existence
ex b1 being non empty stored-program IC-Ins-separated definite COM-Struct of N st
( b1 is realistic & b1 is strict )
proof end;
end;

registration
let N be set ;
let S be COM-Struct of N;
let f, g be PartState of S;
cluster f +* g -> the carrier of S -defined the Object-Kind of S -compatible Function;
coherence
for b1 being Function st b1 = f +* g holds
( b1 is the carrier of S -defined & b1 is the Object-Kind of S -compatible ) ;
end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated COM-Struct of N;
let l be Nat;
func Start-At l,S -> FinPartState of S equals :: COMPOS_1:def 15
(IC S) .--> l;
correctness
coherence
(IC S) .--> l is FinPartState of S;
proof end;
end;

:: deftheorem defines Start-At COMPOS_1:def 15 :
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for l being Nat holds Start-At l,S = (IC S) .--> l;

begin

theorem :: COMPOS_1:6
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for l being Nat
for I being Instruction of S
for p being PartState of S
for s being State of S st p = (IC S),l --> l,I & p c= s holds
CurInstr (ProgramPart s),s = I
proof end;

definition
let N be with_non-empty_elements set ;
let S be non empty IC-Ins-separated COM-Struct of N;
let l be Nat;
let p be PartState of S;
attr p is l -started means :Def41: :: COMPOS_1:def 16
( IC S in dom p & IC p = l );
end;

:: deftheorem Def41 defines -started COMPOS_1:def 16 :
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for l being Nat
for p being PartState of S holds
( p is l -started iff ( IC S in dom p & IC p = l ) );

begin

notation
let x be set ;
synonym InsCode x for x `1_3 ;
synonym JumpPart x for x `2_3 ;
synonym AddressPart x for x `3_3 ;
end;

definition
let N be set ;
let S be COM-Struct of N;
attr S is standard-ins means :Def32: :: COMPOS_1:def 17
 ex X being non empty set st the Instructions of S c= [:NAT ,(NAT * ),(X * ):];
end;

:: deftheorem Def32 defines standard-ins COMPOS_1:def 17 :
for N being set
for S being COM-Struct of N holds
( S is standard-ins iff ex X being non empty set st the Instructions of S c= [:NAT ,(NAT * ),(X * ):] );

registration
let N be set ;
cluster Trivial-COM N -> strict standard-ins ;
coherence
Trivial-COM N is standard-ins
proof end;
end;

registration
let N be set ;
cluster non empty stored-program standard-ins COM-Struct of N;
existence
ex b1 being COM-Struct of N st
( b1 is standard-ins & not b1 is empty & b1 is stored-program )
proof end;
end;

registration
let N be set ;
let S be standard-ins COM-Struct of N;
cluster the Instructions of S -> non empty Relation-like ;
coherence
the Instructions of S is Relation-like
proof end;
end;

registration
let N be set ;
let S be non empty standard-ins COM-Struct of N;
let x be Instruction of S;
cluster InsCode x -> natural ;
coherence
InsCode x is natural
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite standard-ins COM-Struct of N;
existence
ex b1 being non empty stored-program COM-Struct of N st
( b1 is IC-Ins-separated & b1 is definite & b1 is standard-ins )
proof end;
end;

registration
let N be set ;
let S be standard-ins COM-Struct of N;
cluster the Instructions of S -> non empty Relation-like ;
coherence
the Instructions of S is Relation-like ;
end;

definition
let N be set ;
let S be standard-ins COM-Struct of N;
func InsCodes S -> set equals :: COMPOS_1:def 18
 proj1 (proj1 the Instructions of S);
correctness
coherence
proj1 (proj1 the Instructions of S) is set ;
;
end;

:: deftheorem defines InsCodes COMPOS_1:def 18 :
for N being set
for S being standard-ins COM-Struct of N holds InsCodes S = proj1 (proj1 the Instructions of S);

registration
let N be set ;
let S be standard-ins COM-Struct of N;
cluster InsCodes S -> non empty ;
coherence
not InsCodes S is empty
proof end;
end;

definition
let N be set ;
let S be standard-ins COM-Struct of N;
mode InsType of S is Element of InsCodes S;
end;

definition
let N be set ;
let S be standard-ins COM-Struct of N;
let I be Element of the Instructions of S;
:: original: InsCode
redefine func InsCode I -> InsType of S;
coherence
InsCode I is InsType of S
proof end;
end;

begin

LMT: for N being with_non-empty_elements set
for S being COM-Struct of N
for p being FinPartState of S holds p in FinPartSt S
proof end;

registration
let N be with_non-empty_elements set ;
let S be COM-Struct of N;
cluster FinPartSt S -> non empty ;
coherence
not FinPartSt S is empty by LMT;
end;

registration
let N be set ;
let S be COM-Struct of N;
cluster Relation-like NAT -defined the carrier of S -defined the Instructions of S -valued Function-like the Object-Kind of S -compatible finite countable V114() set ;
existence
ex b1 being FinPartState of S st
( b1 is NAT -defined & b1 is the Instructions of S -valued )
proof end;
end;

registration
let N be set ;
let S be non empty stored-program definite COM-Struct of N;
cluster Relation-like NAT -defined the Instructions of S -valued Function-like -> the Object-Kind of S -compatible set ;
coherence
for b1 being Function st b1 is NAT -defined & b1 is the Instructions of S -valued holds
b1 is the Object-Kind of S -compatible
proof end;
end;

theorem :: COMPOS_1:7
for N being set
for S being standard-ins COM-Struct of N
for I, J being Instruction of S st InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J holds
I = J
proof end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated COM-Struct of N;
let l be Nat;
cluster Start-At l,S -> l -started ;
coherence
Start-At l,S is l -started
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated COM-Struct of N;
let l be Nat;
cluster Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V114() l -started set ;
existence
ex b1 being FinPartState of S st b1 is l -started
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be COM-Struct of N;
let s be State of S;
let p be PartState of S;
cluster s +* p -> total PartState of S;
coherence
for b1 being PartState of S st b1 = s +* p holds
b1 is total ;
cluster p +* s -> total PartState of S;
coherence
for b1 being PartState of S st b1 = p +* s holds
b1 is total ;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated COM-Struct of N;
let l be Nat;
let p be PartState of S;
let q be l -started PartState of S;
cluster p +* q -> l -started ;
coherence
p +* q is l -started
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated COM-Struct of N;
let l be Nat;
cluster non empty Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible total l -started set ;
existence
ex b1 being State of S st b1 is l -started
proof end;
end;

definition
let N be with_non-empty_elements set ;
let S be COM-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
let l be set ;
pred p halts_at l means :Def42: :: COMPOS_1:def 19
( l in dom p & p . l = halt S );
end;

:: deftheorem Def42 defines halts_at COMPOS_1:def 19 :
for N being with_non-empty_elements set
for S being COM-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for l being set holds
( p halts_at l iff ( l in dom p & p . l = halt S ) );

definition
let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated COM-Struct of N;
let l be Nat;
let s be State of S;
redefine attr s is l -started means :: COMPOS_1:def 20
 IC s = l;
compatibility
( s is l -started iff IC s = l )
proof end;
end;

:: deftheorem defines -started COMPOS_1:def 20 :
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for l being Nat
for s being State of S holds
( s is l -started iff IC s = l );

definition
let N be with_non-empty_elements set ;
let S be non empty COM-Struct of N;
let s be the Instructions of S -valued ManySortedSet of NAT ;
let l be Nat;
redefine pred s halts_at l means :Def45: :: COMPOS_1:def 21
s . l = halt S;
compatibility
( s halts_at l iff s . l = halt S )
proof end;
end;

:: deftheorem Def45 defines halts_at COMPOS_1:def 21 :
for N being with_non-empty_elements set
for S being non empty COM-Struct of N
for s being the Instructions of b2 -valued ManySortedSet of NAT
for l being Nat holds
( s halts_at l iff s . l = halt S );

theorem :: COMPOS_1:8
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite COM-Struct of N
for l being Nat
for p being b3 -started PartState of S
for s being PartState of S st p c= s holds
s is l -started
proof end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N;
let l be Element of NAT ;
let I be Element of the Instructions of S;
:: original: .-->
redefine func l .--> I -> NAT -defined FinPartState of ;
coherence
l .--> I is NAT -defined FinPartState of
proof end;
end;

theorem Th94: :: COMPOS_1:9
for N being with_non-empty_elements set
for S being non empty COM-Struct of N
for s being State of S holds IC S in dom s by L94;

theorem :: COMPOS_1:10
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for s being State of S holds Start-At (IC s),S = s | {(IC S)}
proof end;

definition
let N be set ;
let S be non empty COM-Struct of N;
let p be PartState of S;
func DataPart p -> PartState of S equals :: COMPOS_1:def 22
p | (Data-Locations S);
coherence
p | (Data-Locations S) is PartState of S ;
projectivity
for b1, b2 being PartState of S st b1 = b2 | (Data-Locations S) holds
b1 = b1 | (Data-Locations S) by RELAT_1:101;
end;

:: deftheorem defines DataPart COMPOS_1:def 22 :
for N being set
for S being non empty COM-Struct of N
for p being PartState of S holds DataPart p = p | (Data-Locations S);

registration
let N be set ;
let S be non empty COM-Struct of N;
let p be FinPartState of S;
cluster DataPart p -> finite ;
coherence
DataPart p is finite ;
end;

definition
let N be set ;
let S be non empty COM-Struct of N;
let IT be PartState of S;
attr IT is data-only means :Def50: :: COMPOS_1:def 23
 dom IT misses {(IC S)} \/ NAT ;
end;

:: deftheorem Def50 defines data-only COMPOS_1:def 23 :
for N being set
for S being non empty COM-Struct of N
for IT being PartState of S holds
( IT is data-only iff dom IT misses {(IC S)} \/ NAT );

registration
let N be set ;
let S be non empty COM-Struct of N;
cluster Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V114() data-only set ;
existence
ex b1 being FinPartState of S st b1 is data-only
proof end;
end;

theorem Th100: :: COMPOS_1:11
for N being set
for S being non empty COM-Struct of N
for p being PartState of S holds not IC S in dom (DataPart p)
proof end;

theorem Th101: :: COMPOS_1:12
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds not IC S in dom (ProgramPart p)
proof end;

theorem Th102: :: COMPOS_1:13
for N being set
for S being non empty COM-Struct of N
for p being PartState of S holds {(IC S)} misses dom (DataPart p) by Th100, ZFMISC_1:56;

theorem Th103: :: COMPOS_1:14
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds {(IC S)} misses dom (ProgramPart p) by Th101, ZFMISC_1:56;

theorem Th104: :: COMPOS_1:15
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for p, q being PartState of S holds dom (DataPart p) misses dom (ProgramPart q)
proof end;

theorem Th106: :: COMPOS_1:16
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for p being PartState of S
for l being Element of NAT st l in dom p holds
l in dom (ProgramPart p)
proof end;

theorem :: COMPOS_1:17
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for p being data-only PartState of S
for q being PartState of S holds
( p c= q iff p c= DataPart q )
proof end;

theorem Th108: :: COMPOS_1:18
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S st IC S in dom p holds
p = ((Start-At (IC p),S) +* (ProgramPart p)) +* (DataPart p)
proof end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated COM-Struct of N;
let IT be PartFunc of (FinPartSt S),(FinPartSt S);
attr IT is data-only means :: COMPOS_1:def 24
for p being PartState of S st p in dom IT holds
( p is data-only & ( for q being PartState of S st q = IT . p holds
q is data-only ) );
end;

:: deftheorem defines data-only COMPOS_1:def 24 :
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for IT being PartFunc of (FinPartSt S),(FinPartSt S) holds
( IT is data-only iff for p being PartState of S st p in dom IT holds
( p is data-only & ( for q being PartState of S st q = IT . p holds
q is data-only ) ) );

theorem :: COMPOS_1:19
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S st IC S in dom p holds
not p is NAT -defined
proof end;

theorem :: COMPOS_1:20
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S
for iloc, a being Element of NAT holds s . a = (s +* (Start-At iloc,S)) . a
proof end;

theorem :: COMPOS_1:21
for N being with_non-empty_elements set
for S being stored-program COM-Struct of N
for s being State of S holds NAT c= dom s by LmL;

theorem :: COMPOS_1:22
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated COM-Struct of N
for s being State of S holds IC s in dom s
proof end;

theorem :: COMPOS_1:23
for N being with_non-empty_elements set
for S being non empty stored-program COM-Struct of N
for s being State of S
for l being Element of NAT holds l in dom s
proof end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program definite COM-Struct of N;
let s be NAT -defined PartState of ;
let f be Function of the Instructions of S,the Instructions of S;
:: original: *
redefine func f * s -> NAT -defined PartState of ;
coherence
s * f is NAT -defined PartState of ;
end;

theorem :: COMPOS_1:24
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated realistic COM-Struct of N
for s1, s2 being State of S st s1,s2 equal_outside NAT holds
IC s1 = IC s2
proof end;

definition
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N;
let s be State of S;
let l be Element of NAT ;
let i be Instruction of S;
:: original: +*
redefine func s +* l,i -> State of S;
coherence
s +* l,i is State of S
proof end;
end;

theorem :: COMPOS_1:25
for N being non empty with_non-empty_elements set
for S being COM-Struct of N
for p being Element of FinPartSt S holds p is FinPartState of S
proof end;

theorem Th134: :: COMPOS_1:26
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated realistic COM-Struct of N
for l being Element of NAT holds dom (Start-At l,S) misses NAT
proof end;

theorem Th135: :: COMPOS_1:27
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated realistic COM-Struct of N
for l being Element of NAT holds ProgramPart (Start-At l,S) = {}
proof end;

registration
let N be set ;
let S be non empty COM-Struct of N;
let p be PartState of S;
cluster DataPart p -> data-only ;
coherence
DataPart p is data-only
proof end;
end;

theorem :: COMPOS_1:28
for N being with_non-empty_elements set
for S being non empty COM-Struct of N
for p being data-only PartState of S holds ProgramPart p = {}
proof end;

theorem :: COMPOS_1:29
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated realistic COM-Struct of N
for l, l1 being Element of NAT holds not l in dom (Start-At l1,S)
proof end;

theorem Th138: :: COMPOS_1:30
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for l being Element of NAT holds DataPart (Start-At l,S) = {}
proof end;

theorem Th139: :: COMPOS_1:31
for N being non empty with_non-empty_elements set
for S being non empty COM-Struct of N
for p being PartState of S holds
( p is data-only iff dom p c= Data-Locations S )
proof end;

theorem :: COMPOS_1:32
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S
for X being set st X c= NAT holds
rng (s | X) c= the Instructions of S
proof end;

theorem :: COMPOS_1:33
for N being non empty with_non-empty_elements set
for S being non empty COM-Struct of N
for p being PartState of S holds
( p is data-only iff DataPart p = p )
proof end;

theorem :: COMPOS_1:34
for N being with_non-empty_elements set
for S being non empty stored-program COM-Struct of N
for s being State of S holds dom (ProgramPart s) = NAT by LmU;

theorem :: COMPOS_1:35
for N being with_non-empty_elements set
for S being COM-Struct of N
for p being FinPartState of S holds p in FinPartSt S by LMT;

theorem :: COMPOS_1:36
for N being with_non-empty_elements set
for S being non empty stored-program definite COM-Struct of N
for f being NAT -defined the Instructions of b2 -valued Function holds f is PartState of S
proof end;

theorem :: COMPOS_1:37
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for n being Nat
for i being Instruction of S holds (IC S),n --> n,i is PartState of S
proof end;

theorem :: COMPOS_1:38
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite COM-Struct of N
for s being State of S
for i being natural number holds (ProgramPart s) /. i = s . i by BWL1;

theorem :: COMPOS_1:39
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite COM-Struct of N
for s1, s2 being State of S holds ProgramPart (s1 +* (DataPart s2)) = ProgramPart s1
proof end;

theorem Th155: :: COMPOS_1:40
for N being set
for S being non empty COM-Struct of N
for d being data-only PartState of S holds dom d misses NAT
proof end;

begin

theorem :: COMPOS_1:41
for N being non empty with_non-empty_elements set
for S being non empty stored-program definite COM-Struct of N
for I being Element of the Instructions of S
for s being State of S holds s +* (NAT --> I) is State of S
proof end;

registration
let N be set ;
let S be COM-Struct of N;
cluster empty Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible finite -> NAT -defined the Instructions of S -valued set ;
coherence
for b1 being FinPartState of S st b1 is empty holds
( b1 is the Instructions of S -valued & b1 is NAT -defined )
proof end;
end;

registration
let N be set ;
let S be COM-Struct of N;
cluster empty Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V114() set ;
existence
ex b1 being FinPartState of S st b1 is empty
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N;
cluster non empty trivial Relation-like NAT -defined the carrier of S -defined the Instructions of S -valued Function-like the Object-Kind of S -compatible finite countable V114() set ;
existence
ex b1 being FinPartState of S st
( not b1 is empty & b1 is trivial & b1 is NAT -defined & b1 is the Instructions of S -valued )
proof end;
end;

begin

begin

registration
let N be non empty with_non-empty_elements set ;
let T be non empty stored-program IC-Ins-separated definite COM-Struct of N;
let i be Element of the Instructions of T;
cluster <%i%> -> the carrier of T -defined ;
coherence
<%i%> is the carrier of T -defined
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N;
cluster non empty trivial Relation-like NAT -defined the carrier of S -defined the Instructions of S -valued Function-like the Object-Kind of S -compatible finite countable V114() initial set ;
existence
ex b1 being FinPartState of S st
( b1 is initial & not b1 is empty & b1 is trivial & b1 is NAT -defined & b1 is the Instructions of S -valued )
proof end;
end;

Lm7: now
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite COM-Struct of N holds
( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S & ( for l being Element of NAT st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds
l = LastLoc <%(halt S)%> ) )
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N; :: thesis: ( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S & ( for l being Element of NAT st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds
l = LastLoc <%(halt S)%> ) )
set F = <%(halt S)%>;
A1: dom <%(halt S)%> = {0 } by FUNCOP_1:19;
then A2: card (dom <%(halt S)%>) = 1 by CARD_1:50;
A3: LastLoc <%(halt S)%> = (card <%(halt S)%>) -' 1 by AFINSQ_1:74
.= (card (dom <%(halt S)%>)) -' 1
.= 0 by A2, XREAL_1:234 ;
hence <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S by FUNCOP_1:87; :: thesis: for l being Element of NAT st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds
l = LastLoc <%(halt S)%>
let l be Element of NAT ; :: thesis: ( <%(halt S)%> . l = halt S & l in dom <%(halt S)%> implies l = LastLoc <%(halt S)%> )
assume <%(halt S)%> . l = halt S ; :: thesis: ( l in dom <%(halt S)%> implies l = LastLoc <%(halt S)%> )
assume l in dom <%(halt S)%> ; :: thesis: l = LastLoc <%(halt S)%>
hence l = LastLoc <%(halt S)%> by A1, A3, TARSKI:def 1; :: thesis: verum
end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N;
let F be non empty NAT -defined FinPartState of ;
attr F is halt-ending means :Def22: :: COMPOS_1:def 25
F . (LastLoc F) = halt S;
attr F is unique-halt means :Def23: :: COMPOS_1:def 26
for f being Element of NAT st F . f = halt S & f in dom F holds
f = LastLoc F;
end;

:: deftheorem Def22 defines halt-ending COMPOS_1:def 25 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite COM-Struct of N
for F being non empty NAT -defined FinPartState of holds
( F is halt-ending iff F . (LastLoc F) = halt S );

:: deftheorem Def23 defines unique-halt COMPOS_1:def 26 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite COM-Struct of N
for F being non empty NAT -defined FinPartState of holds
( F is unique-halt iff for f being Element of NAT st F . f = halt S & f in dom F holds
f = LastLoc F );

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N;
cluster non empty trivial Relation-like NAT -defined the carrier of S -defined the Instructions of S -valued Function-like the Object-Kind of S -compatible T-Sequence-like finite countable V114() initial halt-ending unique-halt set ;
existence
ex b1 being non empty NAT -defined the Instructions of S -valued initial FinPartState of st
( b1 is halt-ending & b1 is unique-halt & b1 is trivial )
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N;
cluster non empty trivial Relation-like NAT -defined the carrier of S -defined the Instructions of S -valued Function-like the Object-Kind of S -compatible finite countable V114() initial set ;
existence
ex b1 being NAT -defined the Instructions of S -valued FinPartState of st
( b1 is trivial & b1 is initial & not b1 is empty )
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N;
cluster non empty trivial Relation-like NAT -defined the carrier of S -defined the Instructions of S -valued Function-like the Object-Kind of S -compatible T-Sequence-like finite countable V114() initial halt-ending unique-halt set ;
existence
ex b1 being non empty NAT -defined the Instructions of S -valued initial FinPartState of st
( b1 is halt-ending & b1 is unique-halt & b1 is trivial )
proof end;
end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N;
mode pre-Macro of S is non empty NAT -defined the Instructions of S -valued initial halt-ending unique-halt FinPartState of ;
end;

theorem :: COMPOS_1:42
for N being non empty with_non-empty_elements set
for i being Element of the Instructions of (Trivial-COM N) holds InsCode i = 0
proof end;

begin

theorem :: COMPOS_1:43
for k being natural number
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for l1, l2 being Element of NAT holds
( Start-At (l1 + k),S = Start-At (l2 + k),S iff Start-At l1,S = Start-At l2,S )
proof end;

theorem :: COMPOS_1:44
for k being natural number
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for l1, l2 being Element of NAT st Start-At l1,S = Start-At l2,S holds
Start-At (l1 -' k),S = Start-At (l2 -' k),S
proof end;

begin

definition
let l be Element of NAT ;
:: original: succ
redefine func succ l -> Element of NAT ;
coherence
succ l is Element of NAT ;
end;

registration
let N be set ;
let S be COM-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
let k be Element of NAT ;
cluster Shift p,k -> the Instructions of S -valued ;
coherence
Shift p,k is the Instructions of S -valued by RELAT_1:def 18;
end;

definition
let N be set ;
let S be COM-Struct of N;
mode preProgram of S is NAT -defined the Instructions of S -valued FinPartState of ;
end;

registration
let N be with_non-empty_elements set ;
let S be COM-Struct of N;
cluster empty Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V114() set ;
existence
ex b1 being FinPartState of S st b1 is empty
proof end;
end;

registration
let N be set ;
let S be COM-Struct of N;
cluster empty Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible finite -> NAT -defined set ;
coherence
for b1 being FinPartState of S st b1 is empty holds
b1 is NAT -defined ;
end;

registration
let N be set ;
let S be COM-Struct of N;
cluster Relation-like NAT -defined the carrier of S -defined the Instructions of S -valued Function-like the Object-Kind of S -compatible finite countable V114() initial set ;
existence
ex b1 being preProgram of S st b1 is initial
proof end;
end;

definition
let N be set ;
let S be COM-Struct of N;
mode Program of S is initial preProgram of S;
end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program definite COM-Struct of N;
func Stop S -> Program of S equals :: COMPOS_1:def 27
<%(halt S)%>;
coherence
<%(halt S)%> is Program of S
proof end;
end;

:: deftheorem defines Stop COMPOS_1:def 27 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program definite COM-Struct of N holds Stop S = <%(halt S)%>;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program definite COM-Struct of N;
cluster Stop S -> non empty ;
coherence
not Stop S is empty ;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program definite COM-Struct of N;
cluster non empty Relation-like NAT -defined the carrier of S -defined the Instructions of S -valued Function-like the Object-Kind of S -compatible T-Sequence-like finite countable V114() initial set ;
existence
not for b1 being Program of S holds b1 is empty
proof end;
end;

theorem :: COMPOS_1:45
for N being non empty with_non-empty_elements set
for S being non empty stored-program definite COM-Struct of N holds 0 in dom (Stop S)
proof end;

theorem :: COMPOS_1:46
for N being non empty with_non-empty_elements set
for S being non empty stored-program definite COM-Struct of N holds card (Stop S) = 1 by AFINSQ_1:36;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N;
let I be initial FinPartState of S;
cluster ProgramPart I -> initial Function;
coherence
for b1 being Function st b1 = ProgramPart I holds
b1 is initial
proof end;
end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated COM-Struct of N;
let p be PartState of S;
let k be Nat;
func IncrIC p,k -> PartState of S equals :: COMPOS_1:def 28
p +* (Start-At ((IC p) + k),S);
correctness
coherence
p +* (Start-At ((IC p) + k),S) is PartState of S;
;
end;

:: deftheorem defines IncrIC COMPOS_1:def 28 :
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for p being PartState of S
for k being Nat holds IncrIC p,k = p +* (Start-At ((IC p) + k),S);

registration
let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated COM-Struct of N;
let p be FinPartState of S;
let k be Nat;
cluster IncrIC p,k -> finite ;
coherence
IncrIC p,k is finite ;
end;

theorem :: COMPOS_1:47
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated realistic COM-Struct of N
for k being Element of NAT holds (Start-At k,S) | NAT = {}
proof end;

theorem :: COMPOS_1:48
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for p being FinPartState of S
for k being Element of NAT holds DataPart (IncrIC p,k) = DataPart p
proof end;

theorem Th13: :: COMPOS_1:49
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for s being State of S holds Data-Locations S c= dom s
proof end;

theorem :: COMPOS_1:50
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for s being State of S holds dom (DataPart s) = Data-Locations S
proof end;

theorem Th15: :: COMPOS_1:51
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N holds NAT misses Data-Locations S
proof end;

theorem Th17: :: COMPOS_1:52
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for l being Element of NAT holds IC S in dom (Start-At l,S)
proof end;

theorem Th18: :: COMPOS_1:53
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being FinPartState of S
for k being Element of NAT holds IC S in dom (IncrIC p,k)
proof end;

theorem Th19: :: COMPOS_1:54
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being FinPartState of S
for k being Element of NAT holds IC (IncrIC p,k) = (IC p) + k
proof end;

theorem :: COMPOS_1:55
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being FinPartState of S
for k being Element of NAT holds (IncrIC p,k) . (IC S) = (IC p) + k
proof end;

theorem Th21: :: COMPOS_1:56
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N holds not IC S in Data-Locations S
proof end;

theorem Th22: :: COMPOS_1:57
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for d being data-only FinPartState of S holds not IC S in dom d
proof end;

theorem Th23: :: COMPOS_1:58
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being FinPartState of S
for d being data-only FinPartState of S holds IC (p +* d) = IC p
proof end;

theorem Th24: :: COMPOS_1:59
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for l being Element of NAT
for d being data-only FinPartState of S holds d tolerates Start-At l,S
proof end;

theorem :: COMPOS_1:60
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being FinPartState of S
for k being Element of NAT
for d being data-only FinPartState of S holds IncrIC (p +* d),k = (IncrIC p,k) +* d
proof end;

theorem :: COMPOS_1:61
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for d being data-only FinPartState of S
for f being NAT -defined the Instructions of b2 -valued finite Function holds d tolerates f
proof end;

theorem :: COMPOS_1:62
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for k being Element of NAT
for d being data-only PartState of S holds ProgramPart (IncrIC d,k) = {}
proof end;

theorem :: COMPOS_1:63
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being FinPartState of S
for k being Element of NAT holds Start-At ((IC p) + k),S c= IncrIC p,k
proof end;

theorem :: COMPOS_1:64
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for l being Element of NAT holds IC (Start-At l,S) = l by FUNCOP_1:87;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N;
let p be PartState of S;
attr p is program-free means :Defx: :: COMPOS_1:def 29
p | NAT = {} ;
func NPP p -> PartState of S equals :: COMPOS_1:def 30
p \ (ProgramPart p);
coherence
p \ (ProgramPart p) is PartState of S
proof end;
end;

:: deftheorem Defx defines program-free COMPOS_1:def 29 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds
( p is program-free iff p | NAT = {} );

:: deftheorem defines NPP COMPOS_1:def 30 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds NPP p = p \ (ProgramPart p);

theorem Th40: :: COMPOS_1:65
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds NPP p = p | (the carrier of S \ NAT )
proof end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N;
let p be FinPartState of S;
cluster NPP p -> finite ;
coherence
NPP p is finite ;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N;
cluster Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible data-only -> program-free set ;
coherence
for b1 being PartState of S st b1 is data-only holds
b1 is program-free
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N;
cluster Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible program-free set ;
existence
ex b1 being PartState of S st b1 is program-free
proof end;
end;

theorem :: COMPOS_1:66
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S
for d being program-free PartState of S holds ProgramPart (p +* d) = ProgramPart p
proof end;

theorem :: COMPOS_1:67
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S
for d being data-only PartState of S holds NPP (p +* d) = (NPP p) +* d
proof end;

theorem Th43: :: COMPOS_1:68
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S holds s = (NPP s) \/ (ProgramPart s) by RELAT_1:88, XBOOLE_1:45;

theorem :: COMPOS_1:69
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S holds the carrier of S = (dom (NPP s)) \/ (dom (ProgramPart s))
proof end;

theorem Th45: :: COMPOS_1:70
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S st IC S in dom p holds
dom (NPP p) = {(IC S)} \/ (dom (DataPart p))
proof end;

theorem :: COMPOS_1:71
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S holds dom (NPP s) = {(IC S)} \/ (dom (DataPart s))
proof end;

theorem Th47: :: COMPOS_1:72
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S st IC S in dom p holds
IC (NPP p) = IC p
proof end;

theorem :: COMPOS_1:73
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds DataPart p = DataPart (NPP p)
proof end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N;
let p be program-free PartState of S;
let k be Element of NAT ;
cluster IncrIC p,k -> program-free ;
coherence
IncrIC p,k is program-free
proof end;
end;

theorem Th49: :: COMPOS_1:74
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S st IC S in dom p holds
NPP p = (DataPart p) +* (Start-At (IC p),S)
proof end;

theorem :: COMPOS_1:75
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for k being Element of NAT
for p being PartState of S st IC S in dom p holds
IncrIC (NPP p),k = (DataPart p) +* (Start-At ((IC p) + k),S)
proof end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N;
let p be PartState of S;
cluster NPP p -> program-free ;
coherence
NPP p is program-free
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N;
let s be State of S;
let k be Nat;
cluster IncrIC s,k -> total ;
coherence
IncrIC s,k is total ;
end;

begin

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N;
let p be PartState of S;
func Initialize p -> PartState of S equals :: COMPOS_1:def 31
p +* (Start-At 0 ,S);
coherence
p +* (Start-At 0 ,S) is PartState of S ;
projectivity
for b1, b2 being PartState of S st b1 = b2 +* (Start-At 0 ,S) holds
b1 = b1 +* (Start-At 0 ,S) by FUNCT_4:99;
end;

:: deftheorem defines Initialize COMPOS_1:def 31 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds Initialize p = p +* (Start-At 0 ,S);

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N;
let p be PartState of S;
cluster Initialize p -> 0 -started ;
coherence
Initialize p is 0 -started ;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N;
let p be FinPartState of S;
cluster Initialize p -> finite ;
coherence
Initialize p is finite ;
end;

theorem Th27: :: COMPOS_1:76
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds dom (Initialize p) = (dom p) \/ {(IC S)}
proof end;

theorem Th28: :: COMPOS_1:77
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S
for x being set holds
( not x in dom (Initialize p) or x in dom p or x = IC S )
proof end;