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

begin

definition

let N be set ;
attr c₂ is strict ;
struct COM-Struct of N -> ZeroStr ;
aggr COM-Struct(# carrier, ZeroF, Instructions, haltF, Object-Kind #) -> COM-Struct of N;
sel Instructions c₂ -> non empty set ;
sel haltF c₂ -> Element of the Instructions of c₂;
sel Object-Kind c₂ -> Function of the carrier of c₂,(N \/ { the Instructions of c₂,NAT});

end;

definition

let N be set ;
func Trivial-COM N -> strict COM-Struct of N means :Def1: :: COMPOS_1:def 1
( the carrier of it = succ NAT & the ZeroF of it = NAT & the Instructions of it = {[0,{},{}]} & the haltF of it = [0,{},{}] & the Object-Kind of it = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) );
existence
ex b₁ being strict COM-Struct of N st
( the carrier of b₁ = succ NAT & the ZeroF of b₁ = NAT & the Instructions of b₁ = {[0,{},{}]} & the haltF of b₁ = [0,{},{}] & the Object-Kind of b₁ = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) )

proof end;

uniqueness
for b₁, b₂ being strict COM-Struct of N st the carrier of b₁ = succ NAT & the ZeroF of b₁ = NAT & the Instructions of b₁ = {[0,{},{}]} & the haltF of b₁ = [0,{},{}] & the Object-Kind of b₁ = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) & the carrier of b₂ = succ NAT & the ZeroF of b₂ = NAT & the Instructions of b₂ = {[0,{},{}]} & the haltF of b₂ = [0,{},{}] & the Object-Kind of b₂ = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) holds
b₁ = b₂ ;

end;

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

definition

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

end;

:: deftheorem Def2 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 b₁ being COM-Struct of N st
( not b₁ is empty & b₁ 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;

notation

let N be set ;
let S be non empty COM-Struct of N;
synonym IC S for 0. N;

end;

definition

canceled;
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 COMPOS_1:def 3 :
canceled;

:: 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 :Def6: :: COMPOS_1:def 6
ObjectKind (IC ) = NAT ;

end;

:: deftheorem Def6 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 ) = NAT );

definition

let N be with_non-empty_elements set ;
let S be COM-Struct of N;
let I be the Object-Kind of S -compatible Function;
attr I is halt-free means :Def7: :: COMPOS_1:def 7
not halt S in rng I;

end;

:: deftheorem Def7 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 the Object-Kind of b₂ -compatible 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 :Def8: :: COMPOS_1:def 8
for l being Element of NAT holds the Object-Kind of IT . l = the Instructions of IT;

end;

:: deftheorem Def8 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 b₁ being non empty stored-program COM-Struct of M st
( b₁ is IC-Ins-separated & b₁ is definite & b₁ is strict )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty strict stored-program IC-Ins-separated definite COM-Struct of N;
existence
ex b₁ being non empty stored-program COM-Struct of N st
( b₁ is IC-Ins-separated & b₁ is definite & b₁ 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 );
coherence
p . (IC ) 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 );

theorem :: COMPOS_1:1

for N being non empty 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 non empty 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 non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for p being the Instructions of b₂ -valued Function
for s being State of S holds CurInstr (p,s) = p /. (IC s);

definition

let N be 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 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;

Lm1: 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;

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;

Lm2: 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;

Lm3: 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 :Def12: :: COMPOS_1:def 12
not the ZeroF of IT in NAT ;

end;

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

theorem :: COMPOS_1:2

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 Lm1;

theorem :: COMPOS_1:3

for A being set
for S being non empty IC-Ins-separated COM-Struct of A st S is realistic holds
for l being Element of NAT holds not IC = l by Def12;

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;

Lm4: 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;

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 )} \/ NAT);
coherence
the carrier of S \ ({(IC )} \/ 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 )} \/ NAT);

definition

let N be set ;
let S be non empty COM-Struct of N;
:: original: Data-Locations
redefine func Data-Locations S -> Subset of S;
coherence
Data-Locations S is Subset of S ;

end;

theorem Th4: :: 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 Th5: :: 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 Th5;

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 Th4;

end;

registration

let A be set ;
cluster Trivial-COM A -> strict realistic ;
coherence
Trivial-COM A is realistic

proof end;

end;

registration

let A be set ;
cluster strict realistic COM-Struct of A;
existence
ex b₁ being COM-Struct of A st
( b₁ is realistic & b₁ is strict )

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 b₁ being non empty stored-program IC-Ins-separated definite COM-Struct of N st
( b₁ is realistic & b₁ 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 b₁ being Function st b₁ = f +* g holds
( b₁ is the carrier of S -defined & b₁ 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 ) .--> l;
correctness
coherence
(IC ) .--> 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 ) .--> 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 Element of NAT
for I being Instruction of S
for P being NAT -defined the Instructions of b₂ -valued Function st l .--> I c= P holds
for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,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 :Def16: :: COMPOS_1:def 16
( IC in dom p & IC p = l );

end;

:: deftheorem Def16 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 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 :Def17: :: COMPOS_1:def 17
ex X being non empty set st the Instructions of S c= [:NAT,(NAT *),(X *):];

end;

:: deftheorem Def17 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 b₁ being COM-Struct of N st
( b₁ is standard-ins & not b₁ is empty & b₁ 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 b₁ being non empty stored-program COM-Struct of N st
( b₁ is IC-Ins-separated & b₁ is definite & b₁ 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

Lm5: 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 Lm5;

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 b₁ being FinPartState of S st
( b₁ is NAT -defined & b₁ 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 b₁ being Function st b₁ is NAT -defined & b₁ is the Instructions of S -valued holds
b₁ is the Object-Kind of S -compatible

proof end;

end;

theorem Th7: :: 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 b₁ being FinPartState of S st b₁ 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 b₁ being PartState of S st b₁ = s +* p holds
b₁ is total ;
cluster p +* s -> total PartState of S;
coherence
for b₁ being PartState of S st b₁ = p +* s holds
b₁ 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 b₁ being State of S st b₁ 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 :Def19: :: COMPOS_1:def 19
( l in dom p & p . l = halt S );

end;

:: deftheorem Def19 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 b₂ -valued Function
for l being set holds
( p halts_at l iff ( l in dom p & p . l = halt S ) );

Lm6: 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 in dom s

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 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 :: COMPOS_1:def 21
s . l = halt S;
compatibility
( s halts_at l iff s . l = halt S )

proof end;

end;

:: deftheorem 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 b₂ -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 b₃ -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 ;

end;

theorem :: 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 in dom s by Lm6;

theorem Th10: :: COMPOS_1:10

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 Start-At ((IC s),S) = s | {(IC )}

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 b₁, b₂ being PartState of S st b₁ = b₂ | (Data-Locations S) holds
b₁ = b₁ | (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 :Def23: :: COMPOS_1:def 23
dom IT misses {(IC )} \/ NAT;

end;

:: deftheorem Def23 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 )} \/ 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 b₁ being FinPartState of S st b₁ is data-only

proof end;

end;

theorem Th11: :: 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 in dom (DataPart p)

proof end;

theorem Th12: :: 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 in dom (ProgramPart p)

proof end;

theorem :: COMPOS_1:13

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

theorem :: 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 )} misses dom (ProgramPart p) by Th12, ZFMISC_1:56;

theorem Th15: :: COMPOS_1:15

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, q being PartState of S holds dom (DataPart p) misses dom (ProgramPart q)

proof end;

theorem Th16: :: COMPOS_1:16

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 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 stored-program IC-Ins-separated definite realistic 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 Th18: :: 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 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 stored-program IC-Ins-separated definite realistic 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 stored-program IC-Ins-separated definite realistic 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 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 Lm4;

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 Th23: :: 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

canceled;

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 Th26: :: 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 Th27: :: 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 Th30: :: 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 Th31: :: 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 Lm2;

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 Lm5;

theorem :: COMPOS_1:36

canceled;

theorem :: COMPOS_1:37

canceled;

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 Lm3;

theorem :: COMPOS_1:39

canceled;

theorem Th40: :: 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;

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 b₁ being FinPartState of S st b₁ is empty holds
( b₁ is the Instructions of S -valued & b₁ 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 b₁ being FinPartState of S st b₁ 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 b₁ being FinPartState of S st
( not b₁ is empty & b₁ is trivial & b₁ is NAT -defined & b₁ is the Instructions of S -valued )

proof end;

end;

begin

notation

let N be set ;
let S be COM-Struct of N;
let i be Instruction of S;
synonym Load i for <%N%>;

end;

registration

let N be set ;
let S be non empty stored-program definite COM-Struct of N;
let ins be Element of the Instructions of S;
cluster Load -> the carrier of S -defined ;
coherence
Load is the carrier of S -defined ;

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 b₁ being FinPartState of S st
( b₁ is initial & not b₁ is empty & b₁ is trivial & b₁ is NAT -defined & b₁ 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
.= 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 :Def25: :: COMPOS_1:def 25
F . (LastLoc F) = halt S;
attr F is unique-halt means :Def26: :: 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 Def25 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 Def26 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 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 b₁ being non empty NAT -defined the Instructions of S -valued initial FinPartState of st
( b₁ is halt-ending & b₁ is unique-halt & b₁ 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 b₁ being NAT -defined the Instructions of S -valued FinPartState of st
( b₁ is trivial & b₁ is initial & not b₁ 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 b₁ being non empty NAT -defined the Instructions of S -valued initial FinPartState of st
( b₁ is halt-ending & b₁ is unique-halt & b₁ 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 realistic 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:41

canceled;

theorem :: COMPOS_1:42

for N being non empty with_non-empty_elements set
for ins being Element of the Instructions of (Trivial-COM N) holds InsCode ins = 0

proof end;

begin

theorem :: COMPOS_1:43

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 natural number
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 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 natural number
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 ;

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 b₁ being FinPartState of S st b₁ 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 b₁ being FinPartState of S st b₁ is empty holds
b₁ is NAT -defined ;

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 -> preProgram of S equals :: COMPOS_1:def 27
<%(halt S)%>;
coherence
<%(halt S)%> is preProgram of S ;

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 initial ;
coherence
( Stop S is initial & 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 finite countable V114() initial set ;
existence
ex b₁ being preProgram of S st
( b₁ is initial & not b₁ is empty )

proof end;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program definite COM-Struct of N;
mode Program of S is non empty initial preProgram of S;

end;

theorem :: COMPOS_1:45

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 0 in dom (Stop S)

proof end;

theorem Th46: :: COMPOS_1:46

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 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 realistic COM-Struct of N;
let I be initial FinPartState of S;
cluster ProgramPart I -> initial Function;
coherence
for b₁ being Function st b₁ = ProgramPart I holds
b₁ is initial

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 realistic COM-Struct of N;
let p be PartState of S;
let k be Nat;
func IncIC (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 IncIC COMPOS_1:def 28 :
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 k being Nat holds IncIC (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 stored-program IC-Ins-separated definite realistic COM-Struct of N;
let p be FinPartState of S;
let k be Nat;
cluster IncIC (p,k) -> finite ;
coherence
IncIC (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 Th48: :: COMPOS_1:48

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 DataPart (IncIC (p,k)) = DataPart p

proof end;

theorem Th49: :: COMPOS_1:49

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 Data-Locations S c= dom s

proof end;

theorem Th50: :: COMPOS_1:50

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 (DataPart s) = Data-Locations S

proof end;

theorem Th51: :: COMPOS_1:51

for N being non empty with_non-empty_elements set
for S being non empty COM-Struct of N holds NAT misses Data-Locations S

proof end;

theorem Th52: :: 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 Nat holds IC in dom (Start-At (l,S))

proof end;

theorem Th53: :: 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 k being natural number
for p being PartState of S holds IC in dom (IncIC (p,k))

proof end;

theorem Th54: :: 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 PartState of S
for k being Nat holds IC (IncIC (p,k)) = (IC p) + k

proof end;

theorem :: COMPOS_1:55

canceled;

theorem Th56: :: 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 in Data-Locations S

proof end;

theorem Th57: :: 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 PartState of S holds not IC in dom d

proof end;

theorem Th58: :: 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 PartState of S
for d being data-only FinPartState of S holds IC (p +* d) = IC p

proof end;

theorem Th59: :: COMPOS_1:59

for N being non empty with_non-empty_elements set
for l being Element of NAT
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 d tolerates Start-At (l,S)

proof end;

theorem Th60: :: 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 natural number
for d being data-only FinPartState of S holds IncIC ((p +* d),k) = (IncIC (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 b₂ -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 natural number
for d being data-only PartState of S holds ProgramPart (IncIC (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= IncIC (p,k)

proof end;

theorem :: COMPOS_1:64

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

definition

let N be set ;
let S be COM-Struct of N;
let p be PartState of S;
attr p is program-free means :Def29: :: 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 ;

end;

:: deftheorem Def29 defines program-free COMPOS_1:def 29 :
for N being set
for S being 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 set
for S being COM-Struct of N
for p being PartState of S holds NPP p = p \ (ProgramPart p);

theorem Th65: :: COMPOS_1:65

for N being non empty with_non-empty_elements set
for S being 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 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 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 b₁ being PartState of S st b₁ is data-only holds
b₁ is program-free

proof end;

end;

registration

let N be non empty with_non-empty_elements 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() program-free set ;
existence
ex b₁ being FinPartState of S st b₁ is program-free

proof end;

end;

theorem Th66: :: 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;

Lm40: for N being non empty with_non-empty_elements set
for S being non empty COM-Struct of N
for p being program-free PartState of S holds dom p misses NAT

proof end;

theorem Th67: :: 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 program-free PartState of S holds NPP (p +* d) = (NPP p) +* d

proof end;

theorem Th68: :: 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 Th70: :: 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 in dom p holds
dom (NPP p) = {(IC )} \/ (dom (DataPart p))

proof end;

theorem Th71: :: 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 )} \/ (dom (DataPart s))

proof end;

theorem Th72: :: 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 in dom p holds
IC (NPP p) = IC p

proof end;

theorem Th73: :: 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 IncIC (p,k) -> program-free ;
coherence
IncIC (p,k) is program-free

proof end;

end;

theorem Th74: :: 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 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 natural number
for p being PartState of S st IC in dom p holds
IncIC ((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 IncIC (s,k) -> total ;
coherence
IncIC (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 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 b₁, b₂ being PartState of S st b₁ = b₂ +* (Start-At (0,S)) holds
b₁ = b₁ +* (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 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 Th76: :: COMPOS_1:76

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 p being PartState of S holds dom (Initialize p) = (dom p) \/ {(IC )}

proof end;

theorem :: 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 FinPartState of S
for x being set holds
( not x in dom (Initialize p) or x in dom p or x = IC )

proof end;

theorem :: COMPOS_1:78

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 0 -started PartState of S holds Initialize p = 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 k be natural number ;
let p be k -started PartState of S;
let I be NAT -defined Function;
cluster p +* I -> k -started PartState of S;
coherence
for b₁ being PartState of S st b₁ = p +* I holds
b₁ is k -started

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 realistic COM-Struct of N;
let p be PartState of S;
let f be NAT -defined the Instructions of S -valued Function;
:: original: +*
redefine func p +* f -> PartState of S;
coherence
p +* f is PartState of S ;

end;

theorem :: COMPOS_1:79

canceled;

theorem Th80: :: COMPOS_1:80

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 (Initialize p) = DataPart p

proof end;

Lm221: 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, q being PartState of S holds NPP (p +* q) = (NPP p) +* (NPP q)

proof end;

theorem :: COMPOS_1:81

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 s1, s2 being State of S st NPP s1 = NPP s2 holds
NPP (Initialize s1) = NPP (Initialize s2)

proof end;

theorem :: COMPOS_1:82

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 f being NAT -defined the Instructions of b₂ -valued Function holds DataPart (p +* f) = DataPart p

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N;
let p be PartState of S;
cluster p | NAT -> the Instructions of S -valued ;
coherence
p | NAT is the Instructions of S -valued

proof end;

end;

theorem :: COMPOS_1:83

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 f being NAT -defined the Instructions of b₂ -valued Function holds Initialize (p +* f) = (Initialize p) +* f

proof end;

theorem :: COMPOS_1:84

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 st IC s = 0 holds
Initialize s = s

proof end;

begin

Lm8: for k being natural number holds - 1 < k
;

Lm9: for k being natural number
for a, b, c being Element of NAT st 1 <= a & 2 <= b & not k < a - 1 & not ( a <= k & k <= (a + b) - 3 ) & not k = (a + b) - 2 & not (a + b) - 2 < k holds
k = a - 1

proof end;

begin

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 i1, i2 be Element of NAT ;
let I1, I2 be Element of the Instructions of S;
:: original: -->
redefine func (i1,i2) --> (I1,I2) -> FinPartState of S;
coherence
(i1,i2) --> (I1,I2) is FinPartState of S ;

end;

definition

let N be set ;
let S be standard-ins COM-Struct of N;
let T be InsType of S;
func JumpParts T -> set equals :: COMPOS_1:def 32
{ (JumpPart I) where I is Instruction of S : InsCode I = T } ;
coherence
{ (JumpPart I) where I is Instruction of S : InsCode I = T } is set ;

end;

:: deftheorem defines JumpParts COMPOS_1:def 32 :
for N being set
for S being standard-ins COM-Struct of N
for T being InsType of S holds JumpParts T = { (JumpPart I) where I is Instruction of S : InsCode I = T } ;

registration

let N be set ;
let S be standard-ins COM-Struct of N;
let I be Element of the Instructions of S;
cluster AddressPart I -> Relation-like Function-like ;
coherence
( AddressPart I is Function-like & AddressPart I is Relation-like )

proof end;

cluster JumpPart I -> Relation-like Function-like ;
coherence
( JumpPart I is Function-like & JumpPart I is Relation-like )

proof end;

end;

registration

let N be set ;
let S be standard-ins COM-Struct of N;
let I be Element of the Instructions of S;
cluster AddressPart I -> FinSequence-like ;
coherence
AddressPart I is FinSequence-like

proof end;

cluster JumpPart I -> FinSequence-like ;
coherence
JumpPart I is FinSequence-like

proof end;

end;

definition

let N be set ;
let S be standard-ins COM-Struct of N;
attr S is homogeneous means :Def33: :: COMPOS_1:def 33
for I, J being Instruction of S st InsCode I = InsCode J holds
dom (JumpPart I) = dom (JumpPart J);

end;

:: deftheorem Def33 defines homogeneous COMPOS_1:def 33 :
for N being set
for S being standard-ins COM-Struct of N holds
( S is homogeneous iff for I, J being Instruction of S st InsCode I = InsCode J holds
dom (JumpPart I) = dom (JumpPart J) );

theorem Th85: :: COMPOS_1:85

for N being non empty with_non-empty_elements set
for I being Instruction of (Trivial-COM N) holds JumpPart I = 0

proof end;

definition

let N be set ;
let S be standard-ins COM-Struct of N;
let T be InsType of S;
func AddressParts T -> set equals :: COMPOS_1:def 34
{ (AddressPart I) where I is Instruction of S : InsCode I = T } ;
coherence
{ (AddressPart I) where I is Instruction of S : InsCode I = T } is set ;

end;

:: deftheorem defines AddressParts COMPOS_1:def 34 :
for N being set
for S being standard-ins COM-Struct of N
for T being InsType of S holds AddressParts T = { (AddressPart I) where I is Instruction of S : InsCode I = T } ;

registration

let N be set ;
let S be standard-ins COM-Struct of N;
let T be InsType of S;
cluster AddressParts T -> functional ;
coherence
AddressParts T is functional

proof end;

cluster JumpParts T -> non empty functional ;
coherence
( not JumpParts T is empty & JumpParts T is functional )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite -> non empty stored-program IC-Ins-separated definite COM-Struct of N;
coherence
for b₁ being non empty stored-program IC-Ins-separated definite COM-Struct of N holds verum ;

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 b₁ being non empty stored-program IC-Ins-separated definite COM-Struct of N st b₁ is standard-ins

proof end;

end;

definition

let N be set ;
let S be standard-ins COM-Struct of N;
attr S is regular means :Def35: :: COMPOS_1:def 35
for I being Instruction of S
for k being set st k in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . k = NAT ;
attr S is J/A-independent means :Def36: :: COMPOS_1:def 36
for T being InsType of S
for f1, f2 being Function
for p being set st f1 in JumpParts T & f2 in product (product" (JumpParts T)) & [T,f1,p] in the Instructions of S holds
[T,f2,p] in the Instructions of S;

end;

:: deftheorem Def35 defines regular COMPOS_1:def 35 :
for N being set
for S being standard-ins COM-Struct of N holds
( S is regular iff for I being Instruction of S
for k being set st k in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . k = NAT );

:: deftheorem Def36 defines J/A-independent COMPOS_1:def 36 :
for N being set
for S being standard-ins COM-Struct of N holds
( S is J/A-independent iff for T being InsType of S
for f1, f2 being Function
for p being set st f1 in JumpParts T & f2 in product (product" (JumpParts T)) & [T,f1,p] in the Instructions of S holds
[T,f2,p] in the Instructions of S );

theorem Th86: :: COMPOS_1:86

for N being non empty with_non-empty_elements set
for T being InsType of (Trivial-COM N) holds JumpParts T = {0}

proof end;

Lm10: for N being non empty with_non-empty_elements set
for I being Instruction of (Trivial-COM N) holds JumpPart I = 0

proof end;

Lm11: for N being non empty with_non-empty_elements set
for T being InsType of (Trivial-COM N) holds JumpParts T = {0}

proof end;

registration

let N be non empty with_non-empty_elements set ;
cluster Trivial-COM N -> strict homogeneous regular J/A-independent ;
coherence
( Trivial-COM N is homogeneous & Trivial-COM N is regular & Trivial-COM N is J/A-independent )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite standard-ins COM-Struct of N st
( b₁ is regular & b₁ is J/A-independent & b₁ is homogeneous & b₁ is realistic )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be standard-ins homogeneous regular COM-Struct of N;
let T be InsType of S;
cluster JumpParts T -> with_common_domain ;
coherence
JumpParts T is with_common_domain

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be standard-ins homogeneous regular COM-Struct of N;
let I be Instruction of S;
cluster JumpPart I -> NAT -valued Function;
coherence
for b₁ being Function st b₁ = JumpPart I holds
b₁ is NAT -valued

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be standard-ins homogeneous regular J/A-independent COM-Struct of N;
let T be InsType of S;
cluster JumpParts T -> product-like ;
coherence
JumpParts T is product-like

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster Trivial-COM N -> strict regular J/A-independent ;
coherence
( Trivial-COM N is regular & Trivial-COM N is J/A-independent ) ;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster standard-ins regular J/A-independent COM-Struct of N;
existence
ex b₁ being standard-ins COM-Struct of N st
( b₁ is regular & b₁ is J/A-independent )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be standard-ins homogeneous COM-Struct of N;
let T be InsType of S;
cluster JumpParts T -> with_common_domain ;
coherence
JumpParts T is with_common_domain

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program standard-ins regular J/A-independent COM-Struct of N;
existence
ex b₁ being non empty stored-program standard-ins COM-Struct of N st
( b₁ is regular & b₁ is J/A-independent )

proof end;

end;

theorem :: COMPOS_1:87

for N being non empty with_non-empty_elements set
for S being non empty stored-program standard-ins homogeneous regular COM-Struct of N
for I being Instruction of S
for x being set st x in dom (JumpPart I) holds
(JumpPart I) . x is Element of NAT

proof end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic standard-ins COM-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite standard-ins COM-Struct of N st b₁ is realistic

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 trivial Relation-like NAT -defined the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V114() set ;
existence
ex b₁ being FinPartState of S st
( not b₁ is trivial & b₁ is NAT -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 Function-like the Object-Kind of S -compatible finite -> non empty NAT -defined unique-halt set ;
coherence
for b₁ being non empty NAT -defined FinPartState of st b₁ is trivial holds
b₁ is unique-halt

proof end;

end;

definition

let N be set ;
let S be standard-ins COM-Struct of N;
let I be Instruction of S;
attr I is ins-loc-free means :Def37: :: COMPOS_1:def 37
JumpPart I is empty ;

end;

:: deftheorem Def37 defines ins-loc-free COMPOS_1:def 37 :
for N being set
for S being standard-ins COM-Struct of N
for I being Instruction of S holds
( I is ins-loc-free iff JumpPart I is empty );

Lm12: 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
( dom (Stop S) = {0} & 0 in dom (Stop S) )
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N; :: thesis: ( dom (Stop S) = {0} & 0 in dom (Stop S) )
thus dom (Stop S) = {0} by FUNCOP_1:19; :: thesis: 0 in dom (Stop S)
hence 0 in dom (Stop S) by TARSKI:def 1; :: thesis: verum

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 Stop S -> non empty trivial initial ;
coherence
( Stop S is initial & not Stop S is empty & Stop S is NAT -defined & Stop S is the Instructions of S -valued & Stop S is trivial ) ;

end;

theorem Th88: :: COMPOS_1:88

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 holds card (Stop S) = 1

proof end;

theorem Th89: :: COMPOS_1:89

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 F being pre-Macro of S st card F = 1 holds
F = Stop S

proof end;

Lm13: 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 holds (card (Stop S)) -' 1 = 0

proof end;

theorem Th90: :: COMPOS_1:90

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 holds LastLoc (Stop S) = 0

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;
cluster Stop S -> halt-ending unique-halt ;
coherence
( Stop S is halt-ending & Stop S is unique-halt )

proof end;

end;

begin

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N;
let I be Element of the Instructions of S;
cluster JumpPart I -> natural-valued Function;
coherence
for b₁ being Function st b₁ = JumpPart I holds
b₁ is natural-valued ;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N;
let I be Element of the Instructions of S;
let k be natural number ;
func IncAddr (I,k) -> Instruction of S means :Def38: :: COMPOS_1:def 38
( InsCode it = InsCode I & AddressPart it = AddressPart I & JumpPart it = k + (JumpPart I) );
existence
ex b₁ being Instruction of S st
( InsCode b₁ = InsCode I & AddressPart b₁ = AddressPart I & JumpPart b₁ = k + (JumpPart I) )

proof end;

uniqueness
for b₁, b₂ being Instruction of S st InsCode b₁ = InsCode I & AddressPart b₁ = AddressPart I & JumpPart b₁ = k + (JumpPart I) & InsCode b₂ = InsCode I & AddressPart b₂ = AddressPart I & JumpPart b₂ = k + (JumpPart I) holds
b₁ = b₂ by Th7;

end;

:: deftheorem Def38 defines IncAddr COMPOS_1:def 38 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for I being Element of the Instructions of S
for k being natural number
for b₅ being Instruction of S holds
( b₅ = IncAddr (I,k) iff ( InsCode b₅ = InsCode I & AddressPart b₅ = AddressPart I & JumpPart b₅ = k + (JumpPart I) ) );

theorem Th91: :: COMPOS_1:91

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for I being Element of the Instructions of S holds IncAddr (I,0) = I

proof end;

theorem Th92: :: COMPOS_1:92

for N being non empty with_non-empty_elements set
for k being natural number
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for I being Instruction of S st I is ins-loc-free holds
IncAddr (I,k) = I

proof end;

definition

let N be set ;
let S be standard-ins COM-Struct of N;
attr S is proper-halt means :Def39: :: COMPOS_1:def 39
halt S is ins-loc-free ;

end;

:: deftheorem Def39 defines proper-halt COMPOS_1:def 39 :
for N being set
for S being standard-ins COM-Struct of N holds
( S is proper-halt iff halt S is ins-loc-free );

registration

let N be set ;
cluster Trivial-COM N -> strict proper-halt ;
coherence
Trivial-COM N is proper-halt

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N;
existence
ex b₁ being non empty stored-program standard-ins COM-Struct of N st
( b₁ is proper-halt & b₁ is regular & b₁ is homogeneous & b₁ is J/A-independent & b₁ is realistic & b₁ is IC-Ins-separated & b₁ is definite )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be standard-ins proper-halt COM-Struct of N;
cluster halt S -> ins-loc-free ;
coherence
halt S is ins-loc-free by Def39;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be standard-ins proper-halt COM-Struct of N;
cluster ins-loc-free Element of the Instructions of S;
existence
ex b₁ being Instruction of S st b₁ is ins-loc-free

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be standard-ins proper-halt COM-Struct of N;
let I be ins-loc-free Instruction of S;
cluster JumpPart I -> empty ;
coherence
JumpPart I is empty by Def37;

end;

theorem :: COMPOS_1:93

for N being non empty with_non-empty_elements set
for k being natural number
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N holds IncAddr ((halt S),k) = halt S by Th92;

theorem :: COMPOS_1:94

for N being non empty with_non-empty_elements set
for k being natural number
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for I being Instruction of S holds JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))

proof end;

theorem Th95: :: COMPOS_1:95

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for I, J being Instruction of S st ex k being natural number st IncAddr (I,k) = IncAddr (J,k) holds
I = J

proof end;

theorem Th96: :: COMPOS_1:96

for N being non empty with_non-empty_elements set
for k being natural number
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N
for I being Instruction of S st IncAddr (I,k) = halt S holds
I = halt S

proof end;

theorem Th97: :: COMPOS_1:97

for N being non empty with_non-empty_elements set
for k, m being natural number
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for I being Instruction of S holds IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N;
let p be NAT -defined the Instructions of S -valued finite Function;
let k be natural number ;
A1: dom p c= NAT by RELAT_1:def 18;
func IncAddr (p,k) -> FinPartState of S means :Def40: :: COMPOS_1:def 40
( dom it = dom p & ( for m being natural number st m in dom p holds
it . m = IncAddr ((p /. m),k) ) );
existence
ex b₁ being FinPartState of S st
( dom b₁ = dom p & ( for m being natural number st m in dom p holds
b₁ . m = IncAddr ((p /. m),k) ) )

proof end;

uniqueness
for b₁, b₂ being FinPartState of S st dom b₁ = dom p & ( for m being natural number st m in dom p holds
b₁ . m = IncAddr ((p /. m),k) ) & dom b₂ = dom p & ( for m being natural number st m in dom p holds
b₂ . m = IncAddr ((p /. m),k) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def40 defines IncAddr COMPOS_1:def 40 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for p being NAT -defined the Instructions of b₂ -valued finite Function
for k being natural number
for b₅ being FinPartState of S holds
( b₅ = IncAddr (p,k) iff ( dom b₅ = dom p & ( for m being natural number st m in dom p holds
b₅ . m = IncAddr ((p /. m),k) ) ) );

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N;
let F be NAT -defined the Instructions of S -valued finite Function;
let k be natural number ;
cluster IncAddr (F,k) -> NAT -defined the Instructions of S -valued ;
coherence
( IncAddr (F,k) is NAT -defined & IncAddr (F,k) is the Instructions of S -valued )

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 standard-ins regular J/A-independent COM-Struct of N;
cluster empty Relation-like NAT -defined the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V114() set ;
existence
ex b₁ being FinPartState of S st
( b₁ is empty & b₁ is NAT -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 standard-ins homogeneous regular J/A-independent COM-Struct of N;
let F be empty NAT -defined the Instructions of S -valued FinPartState of ;
let k be natural number ;
cluster IncAddr (F,k) -> empty ;
coherence
IncAddr (F,k) 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 standard-ins homogeneous regular J/A-independent COM-Struct of N;
let F be non empty NAT -defined the Instructions of S -valued FinPartState of ;
let k be natural number ;
cluster IncAddr (F,k) -> non empty ;
coherence
not IncAddr (F,k) 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 standard-ins homogeneous regular J/A-independent COM-Struct of N;
let F be NAT -defined the Instructions of S -valued initial FinPartState of ;
let k be natural number ;
cluster IncAddr (F,k) -> initial ;
coherence
IncAddr (F,k) is initial

proof end;

end;

theorem Th98: :: COMPOS_1:98

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for F being NAT -defined the Instructions of b₂ -valued FinPartState of holds IncAddr (F,0) = F

proof end;

theorem Th99: :: COMPOS_1:99

for N being non empty with_non-empty_elements set
for k, m being natural number
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for F being NAT -defined the Instructions of b₄ -valued finite Function holds IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N;
let p be NAT -defined the Instructions of S -valued finite Function;
let k be Element of NAT ;
func Reloc (p,k) -> NAT -defined the Instructions of S -valued finite Function equals :: COMPOS_1:def 41
IncAddr ((Shift (p,k)),k);
coherence
IncAddr ((Shift (p,k)),k) is NAT -defined the Instructions of S -valued finite Function ;

end;

:: deftheorem defines Reloc COMPOS_1:def 41 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for p being NAT -defined the Instructions of b₂ -valued finite Function
for k being Element of NAT holds Reloc (p,k) = IncAddr ((Shift (p,k)),k);

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite standard-ins regular J/A-independent COM-Struct of N st
( b₁ is homogeneous & b₁ is realistic )

proof end;

end;

theorem Th100: :: COMPOS_1:100

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for F being non empty NAT -defined initial FinPartState of
for G being non empty NAT -defined the Instructions of b₂ -valued FinPartState of holds dom (CutLastLoc F) misses dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)))

proof end;

theorem Th101: :: COMPOS_1:101

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 F being non empty NAT -defined initial unique-halt FinPartState of
for I being Element of NAT st I in dom (CutLastLoc F) holds
(CutLastLoc F) . I <> halt 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 standard-ins homogeneous regular J/A-independent COM-Struct of N;
let F, G be non empty NAT -defined the Instructions of S -valued FinPartState of ;
func F ';' G -> NAT -defined the Instructions of S -valued FinPartState of equals :: COMPOS_1:def 42
(CutLastLoc F) +* (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)));
coherence
(CutLastLoc F) +* (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1))) is NAT -defined the Instructions of S -valued FinPartState of ;

end;

:: deftheorem defines ';' COMPOS_1:def 42 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for F, G being non empty NAT -defined the Instructions of b₂ -valued FinPartState of holds F ';' G = (CutLastLoc F) +* (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)));

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N;
let F, G be non empty NAT -defined the Instructions of S -valued FinPartState of ;
cluster F ';' G -> non empty NAT -defined the Instructions of S -valued ;
coherence
( not F ';' G is empty & F ';' G is the Instructions of S -valued & F ';' G is NAT -defined ) ;

end;

theorem Th102: :: COMPOS_1:102

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for F being non empty NAT -defined the Instructions of b₂ -valued initial FinPartState of
for G being non empty NAT -defined the Instructions of b₂ -valued FinPartState of holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )

proof end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N;
let F, G be non empty NAT -defined the Instructions of S -valued initial FinPartState of ;
cluster F ';' G -> NAT -defined the Instructions of S -valued initial ;
coherence
F ';' G is initial

proof end;

end;

theorem :: COMPOS_1:103

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for F, G being non empty NAT -defined the Instructions of b₂ -valued initial FinPartState of holds dom F c= dom (F ';' G)

proof end;

theorem Th104: :: COMPOS_1:104

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for F, G being non empty NAT -defined the Instructions of b₂ -valued initial FinPartState of holds CutLastLoc F c= CutLastLoc (F ';' G)

proof end;

theorem Th105: :: COMPOS_1:105

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for F, G being non empty NAT -defined the Instructions of b₂ -valued initial FinPartState of holds (F ';' G) . (LastLoc F) = (IncAddr (G,((card F) -' 1))) . 0

proof end;

theorem :: COMPOS_1:106

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for F, G being non empty NAT -defined the Instructions of b₂ -valued initial FinPartState of
for f being Element of NAT st f < (card F) - 1 holds
(IncAddr (F,((card F) -' 1))) . f = (IncAddr ((F ';' G),((card F) -' 1))) . f

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 standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N;
let F be non empty NAT -defined the Instructions of S -valued initial FinPartState of ;
let G be non empty NAT -defined the Instructions of S -valued initial halt-ending FinPartState of ;
cluster F ';' G -> NAT -defined the Instructions of S -valued halt-ending ;
coherence
F ';' G is halt-ending

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 standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N;
let F, G be non empty NAT -defined the Instructions of S -valued initial halt-ending unique-halt FinPartState of ;
cluster F ';' G -> NAT -defined the Instructions of S -valued unique-halt ;
coherence
F ';' G is unique-halt

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 realistic standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N;
let F, G be pre-Macro of S;
:: original: ';'
redefine func F ';' G -> pre-Macro of S;
coherence
F ';' G is pre-Macro of S ;

end;

theorem Th107: :: COMPOS_1:107

for N being non empty with_non-empty_elements set
for k being natural number
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N holds IncAddr ((Stop S),k) = Stop S

proof end;

theorem Th108: :: COMPOS_1:108

for N being non empty with_non-empty_elements set
for k being Element of NAT
for S being non empty stored-program IC-Ins-separated definite COM-Struct of N holds Shift ((Stop S),k) = k .--> (halt S)

proof end;

theorem Th109: :: COMPOS_1:109

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N
for F being pre-Macro of S holds F ';' (Stop S) = F

proof end;

theorem Th110: :: COMPOS_1:110

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for F being pre-Macro of S holds (Stop S) ';' F = F

proof end;

theorem :: COMPOS_1:111

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N
for F, G, H being pre-Macro of S holds (F ';' G) ';' H = F ';' (G ';' H)

proof end;

theorem :: COMPOS_1:112

for N being non empty with_non-empty_elements set
for S being non empty stored-program standard-ins homogeneous regular COM-Struct of N
for I being Instruction of S
for x being set st x in dom (JumpPart I) holds
(JumpPart I) . x in (product" (JumpParts (InsCode I))) . x

proof end;

theorem :: COMPOS_1:113

for N being non empty with_non-empty_elements set
for I being Instruction of (Trivial-COM N) holds JumpPart I = 0 by Lm10;

theorem :: COMPOS_1:114

for N being non empty with_non-empty_elements set
for T being InsType of (Trivial-COM N) holds JumpParts T = {0} by Lm11;

begin

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N;
let k be Element of NAT ;
let p be FinPartState of S;
func Relocated (p,k) -> FinPartState of S equals :: COMPOS_1:def 43
(IncIC ((NPP p),k)) +* (Reloc ((ProgramPart p),k));
coherence
(IncIC ((NPP p),k)) +* (Reloc ((ProgramPart p),k)) is FinPartState of S ;

end;

:: deftheorem defines Relocated COMPOS_1:def 43 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for k being Element of NAT
for p being FinPartState of S holds Relocated (p,k) = (IncIC ((NPP p),k)) +* (Reloc ((ProgramPart p),k));

theorem Th115: :: COMPOS_1:115

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for g being FinPartState of S
for k being Element of NAT holds DataPart (Relocated (g,k)) = DataPart g

proof end;

theorem Th116: :: COMPOS_1:116

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for g being FinPartState of S
for k being Element of NAT holds ProgramPart (Relocated (g,k)) = Reloc ((ProgramPart g),k)

proof end;

theorem Th117: :: COMPOS_1:117

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for k being Element of NAT
for p being NAT -defined the Instructions of b₂ -valued finite Function holds dom (Reloc (p,k)) = { (j + k) where j is Element of NAT : j in dom p }

proof end;

theorem :: COMPOS_1:118

canceled;

theorem Th119: :: COMPOS_1:119

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for g being FinPartState of S
for k being Element of NAT holds IC in dom (Relocated (g,k))

proof end;

theorem Th120: :: COMPOS_1:120

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for g being FinPartState of S
for k being Element of NAT st IC in dom g holds
IC (Relocated (g,k)) = (IC g) + k

proof end;

theorem Th121: :: COMPOS_1:121

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for i, j being Element of NAT
for p being NAT -defined the Instructions of b₂ -valued finite Function holds Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i)

proof end;

theorem :: COMPOS_1:122

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for il being Element of NAT
for g being NAT -defined the Instructions of b₂ -valued finite Function
for k being Element of NAT
for I being Instruction of S st il in dom g & I = g . il holds
IncAddr (I,k) = (Reloc (g,k)) . (il + k)

proof end;

theorem :: COMPOS_1:123

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for g being FinPartState of S
for k being Element of NAT st IC in dom g holds
Start-At (((IC g) + k),S) c= Relocated (g,k)

proof end;

theorem :: COMPOS_1:124

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for g being FinPartState of S
for k being Element of NAT
for q being data-only FinPartState of S holds Relocated ((g +* q),k) = (Relocated (g,k)) +* q

proof end;

begin

definition

let N be set ;
let S be non empty stored-program definite COM-Struct of N;
let i be Instruction of S;
:: original: Load
redefine func Load i -> preProgram of S;
coherence
Load is preProgram of S ;

end;

theorem :: COMPOS_1:125

canceled;

theorem :: COMPOS_1:126

canceled;

theorem :: COMPOS_1:127

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 s1, s2 being State of S holds
( ( for l being Element of NAT holds s1 . l = s2 . l ) iff s1 | NAT = s2 | NAT )

proof end;

theorem :: COMPOS_1:128

canceled;

theorem :: COMPOS_1:129

canceled;

theorem Th130: :: COMPOS_1:130

for N being non empty with_non-empty_elements set
for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for I being NAT -defined Function holds dom I misses dom (Start-At (n,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 I be Program of S;
func stop I -> Program of S equals :: COMPOS_1:def 44
I ^ (Stop S);
coherence
I ^ (Stop S) is Program of S ;

end;

:: deftheorem defines stop COMPOS_1:def 44 :
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 Program of S holds stop I = I ^ (Stop 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 s be State of S;
cluster Initialize s -> total ;
coherence
Initialize s is total ;

end;

theorem :: COMPOS_1:131

canceled;

theorem :: COMPOS_1:132

canceled;

theorem :: COMPOS_1:133

canceled;

theorem :: COMPOS_1:134

canceled;

theorem :: COMPOS_1:135

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 I being Program of S holds 0 in dom (stop I)

proof end;

begin

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program definite COM-Struct of N;
let i be Instruction of S;
func Macro i -> Program of S equals :: COMPOS_1:def 45
(0,1) --> (i,(halt S));
coherence
(0,1) --> (i,(halt S)) is Program of S

proof end;

correctness
;

end;

:: deftheorem defines Macro COMPOS_1:def 45 :
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 Instruction of S holds Macro i = (0,1) --> (i,(halt 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 i be Instruction of S;
cluster Macro i -> ;
coherence
not Macro i is empty ;

end;

theorem :: COMPOS_1:136

canceled;

theorem Th137: :: COMPOS_1:137

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 (DataPart p) misses NAT

proof end;

theorem :: COMPOS_1:138

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 s1, s2 being State of S st NPP s1 = NPP s2 holds
DataPart s1 = DataPart s2

proof end;

theorem Th139: :: COMPOS_1:139

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 I being NAT -defined Function holds not IC in dom I

proof end;

begin

theorem Th140: :: COMPOS_1:140

for N being non empty with_non-empty_elements set
for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for I being Program of S holds dom I misses dom (Start-At (n,S))

proof end;

theorem Th141: :: COMPOS_1:141

for N being non empty with_non-empty_elements set
for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds IC in dom (p +* (Start-At (n,S)))

proof end;

theorem Th142: :: COMPOS_1:142

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 n being Nat holds IC (p +* (Start-At (n,S))) = n

proof end;

theorem :: COMPOS_1:143

for N being non empty with_non-empty_elements set
for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S
for p being PartState of S st p +* (Start-At (n,S)) c= s holds
IC s = n

proof end;

begin

theorem :: COMPOS_1:144

for N being non empty with_non-empty_elements set
for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for I being Program of S holds (I +* (Start-At (n,S))) | NAT = I

proof end;

theorem :: COMPOS_1:145

for N being non empty with_non-empty_elements set
for x being set
for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for I being Program of S st x in dom I holds
I . x = (I +* (Start-At (n,S))) . x

proof end;

theorem :: COMPOS_1:146

canceled;

theorem Th147: :: COMPOS_1:147

for N being non empty with_non-empty_elements set
for x being set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for i being Instruction of S holds
( x in dom (Macro i) iff ( x = 0 or x = 1 ) )

proof end;

theorem :: COMPOS_1:148

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 i being Instruction of S holds
( (Macro i) . 0 = i & (Macro i) . 1 = halt S & (Initialize (Macro i)) . 0 = i )

proof end;

begin

theorem :: COMPOS_1:149

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 i being Instruction of S holds dom (Macro i) = {0,1}

proof end;

theorem :: COMPOS_1:150

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 i being Instruction of S holds card (Macro i) = 2

proof 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 Stop S -> non halt-free ;
coherence
not Stop S is halt-free

proof end;

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 non halt-free set ;
existence
ex b₁ being Program of S st
( not b₁ is halt-free & b₁ is finite )

proof end;

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 Relation-like NAT -defined the Instructions of S -valued Function-like -> the Object-Kind of S -compatible set ;
coherence
for b₁ being Function st b₁ is NAT -defined & b₁ is the Instructions of S -valued holds
b₁ is the Object-Kind of S -compatible ;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program definite COM-Struct of N;
let p be PartState of S;
let q be NAT -defined the Instructions of S -valued non halt-free Function;
cluster ProgramPart (p +* q) -> non halt-free ;
coherence
not ProgramPart (p +* q) is halt-free

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program definite COM-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
let q be NAT -defined the Instructions of S -valued non halt-free Function;
cluster p +* q -> non halt-free ;
coherence
not p +* q is halt-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 standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N;
let p be NAT -defined the Instructions of S -valued finite non halt-free Function;
let k be Element of NAT ;
cluster Reloc (p,k) -> NAT -defined the Instructions of S -valued finite non halt-free ;
coherence
not Reloc (p,k) is halt-free

proof end;

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 non halt-free set ;
existence
not for b₁ being Program of S holds b₁ is halt-free

proof end;

end;

theorem Th151: :: COMPOS_1:151

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 p being PartState of S holds
( p is l -started iff Start-At (l,S) c= 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;
cluster Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V114() non program-free set ;
existence
not for b₁ being FinPartState of S holds b₁ 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 p be non program-free PartState of S;
let f be Function;
cluster p +* f -> non program-free PartState of S;
coherence
for b₁ being PartState of S st b₁ = p +* f holds
not b₁ is program-free

proof end;

cluster f +* p -> non program-free PartState of S;
coherence
for b₁ being PartState of S st b₁ = f +* p holds
not b₁ is program-free

proof end;

end;

theorem Th152: :: COMPOS_1:152

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 program-free PartState of S
for k being Element of NAT holds ProgramPart (IncIC (p,k)) = {} by Def29;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N;
let p be non program-free FinPartState of S;
let k be Element of NAT ;
cluster Relocated (p,k) -> non program-free ;
coherence
not Relocated (p,k) 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 k be Element of NAT ;
let p be k -started PartState of S;
let d be data-only PartState of S;
cluster p +* d -> k -started ;
coherence
p +* d is k -started

proof end;

end;

theorem Th153: :: COMPOS_1:153

for N being non empty with_non-empty_elements set
for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for p, q being NAT -defined the Instructions of b₃ -valued finite Function holds IncAddr ((p +* q),n) = (IncAddr (p,n)) +* (IncAddr (q,n))

proof end;

theorem :: COMPOS_1:154

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for p, q being NAT -defined the Instructions of b₂ -valued finite Function
for k being Element of NAT holds Reloc ((p +* q),k) = (Reloc (p,k)) +* (Reloc (q,k))

proof end;

theorem :: COMPOS_1:155

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for p being NAT -defined the Instructions of b₂ -valued finite Function
for m, n being Element of NAT holds Reloc ((Reloc (p,m)),n) = Reloc (p,(m + n))

proof end;

theorem :: COMPOS_1:156

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for P, Q being NAT -defined the Instructions of b₂ -valued finite Function
for k being Element of NAT st P c= Q holds
Reloc (P,k) c= Reloc (Q,k)

proof end;

theorem :: COMPOS_1:157

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for P being preProgram of S holds Reloc (P,0) = P

proof end;

theorem :: COMPOS_1:158

for N being non empty with_non-empty_elements set
for il being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for k being Element of NAT
for P being preProgram of S holds
( il in dom P iff il + k in dom (Reloc (P,k)) )

proof end;

theorem :: COMPOS_1:159

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for i being Element of NAT
for p being NAT -defined the Instructions of b₂ -valued finite Function holds Shift ((IncAddr (p,i)),i) = Reloc (p,i) by Th121;

theorem Th160: :: COMPOS_1:160

for N being set
for S being non empty stored-program COM-Struct of N holds the carrier of S = ({(IC )} \/ (Data-Locations S)) \/ NAT

proof end;

Lm168: 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, q being PartState of S holds DataPart p misses ProgramPart q

proof end;

Lm169: 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 c= NPP p

proof end;

LmXX: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for k being Element of NAT
for p being FinPartState of S st IC in dom p holds
NPP (Relocated (p,k)) = IncIC ((NPP p),k)

proof end;

Lm179: 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 in dom p holds
IC in dom (NPP p)

proof end;

theorem :: COMPOS_1:161

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for k being Element of NAT
for p being FinPartState of S
for s1, s2 being State of S st p c= s1 & Relocated (p,k) c= s2 holds
p c= s1 +* (DataPart s2)

proof end;

theorem :: COMPOS_1:162

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 i, j being Nat holds IncIC ((IncIC (p,i)),j) = IncIC (p,(i + j))

proof end;

theorem :: COMPOS_1:163

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 j, k being Nat holds IncIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j + k),S))

proof end;

theorem Th164: :: COMPOS_1:164

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 Start-At ((IC s),S) c= s

proof end;

theorem :: COMPOS_1:165

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 +* (Start-At ((IC s),S)) = s

proof end;

theorem :: COMPOS_1:166

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 k being Nat holds (IC (IncIC (s,k))) -' k = IC s

proof end;

theorem :: COMPOS_1:167

for n being Element of NAT
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N
for i being Instruction of S
for f being Function of the Instructions of S, the Instructions of S st f = (id the Instructions of S) +* ((halt S) .--> i) holds
for s being NAT -defined the Instructions of b₃ -valued finite Function holds IncAddr ((f * s),n) = ((id the Instructions of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))

proof end;

theorem Th168: :: COMPOS_1:168

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, q being PartState of S holds DataPart p misses ProgramPart q

proof end;

theorem Th169: :: COMPOS_1:169

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 c= NPP p

proof end;

theorem Th170: :: COMPOS_1:170

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, q being PartState of S st p c= q holds
NPP p c= NPP q

proof end;

theorem Th171: :: COMPOS_1:171

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 (NPP p) c= {(IC )} \/ (dom (DataPart p))

proof end;

theorem :: COMPOS_1:172

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 s = ({(IC )} \/ (Data-Locations S)) \/ NAT

proof end;

theorem :: COMPOS_1:173

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for I, J being Program of S holds dom I misses dom (Reloc ((ProgramPart J),(card I)))

proof end;

theorem :: COMPOS_1:174

for N being non empty with_non-empty_elements set
for m being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for I being preProgram of S holds card (Reloc ((ProgramPart I),m)) = card I

proof end;

LmAA: 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 NPP s = s | ((Data-Locations S) \/ {(IC )})

proof end;

theorem :: COMPOS_1:175

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 s1, s2 being State of S holds
( NPP s1 = NPP s2 iff s1 | ((Data-Locations S) \/ {(IC )}) = s2 | ((Data-Locations S) \/ {(IC )}) )

proof end;

theorem :: COMPOS_1:176

for N being non empty with_non-empty_elements set
for S being non empty COM-Struct of N
for p being data-only PartState of S holds NPP p = p

proof end;

theorem :: COMPOS_1:177

canceled;

theorem :: COMPOS_1:178

canceled;

theorem Th179: :: COMPOS_1:179

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 in dom p holds
IC in dom (NPP p)

proof end;

theorem :: COMPOS_1:180

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for p being FinPartState of S
for k being Element of NAT holds NPP (Relocated (p,k)) = IncIC ((NPP p),k)

proof end;

theorem :: COMPOS_1:181

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for p being PartState of S st IC in dom p holds
NPP p = (Start-At ((IC p),S)) +* (DataPart p)

proof end;

theorem :: COMPOS_1:182

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for p being PartState of S holds (dom (NPP p)) /\ (Data-Locations S) = dom (DataPart p)

proof end;

theorem :: COMPOS_1:183

canceled;

theorem Th184: :: COMPOS_1:184

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 = (ProgramPart p) +* (NPP p)

proof end;

theorem :: COMPOS_1:185

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for s being State of S holds Data-Locations S c= dom (NPP 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 realistic COM-Struct of N;
let p be PartState of S;
let k be Nat;
func DecIC (p,k) -> PartState of S equals :: COMPOS_1:def 46
p +* (Start-At (((IC p) -' k),S));
correctness
coherence
p +* (Start-At (((IC p) -' k),S)) is PartState of S;
;

end;

:: deftheorem defines DecIC COMPOS_1:def 46 :
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 k being Nat holds DecIC (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 stored-program IC-Ins-separated definite realistic COM-Struct of N;
let p be FinPartState of S;
let k be Nat;
cluster DecIC (p,k) -> finite ;
coherence
DecIC (p,k) is finite ;

end;

theorem :: COMPOS_1:186

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 DataPart (DecIC (p,k)) = DataPart p

proof end;

theorem Th187: :: COMPOS_1:187

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 k being Nat holds IC in dom (DecIC (p,k))

proof end;

theorem Th188: :: COMPOS_1:188

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 k being Nat holds IC (DecIC (p,k)) = (IC p) -' k

proof end;

theorem :: COMPOS_1:189

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 FinPartState of S
for k being Nat holds DecIC ((p +* d),k) = (DecIC (p,k)) +* d

proof end;

theorem :: COMPOS_1:190

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 PartState of S
for k being Nat holds ProgramPart (DecIC (d,k)) = {}

proof end;

theorem :: COMPOS_1:191

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= DecIC (p,k)

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 DecIC (p,k) -> program-free ;
coherence
DecIC (p,k) is program-free

proof end;

end;

theorem :: COMPOS_1:192

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 k being Nat st IC in dom p holds
DecIC ((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 s be State of S;
let k be Nat;
cluster DecIC (s,k) -> total ;
coherence
DecIC (s,k) is total ;

end;

theorem :: COMPOS_1:193

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 program-free PartState of S
for k being Element of NAT holds ProgramPart (DecIC (p,k)) = {} by Def29;

theorem :: COMPOS_1:194

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 i, j being Nat holds DecIC ((DecIC (p,i)),j) = DecIC (p,(i + j))

proof end;

theorem :: COMPOS_1:195

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 j, k being Nat holds DecIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j -' k),S))

proof end;

theorem :: COMPOS_1:196

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 k being Nat st k <= IC s holds
(IC (DecIC (s,k))) + k = IC s

proof end;

theorem :: COMPOS_1:197

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, q being PartState of S
for k being Nat st IC in dom q holds
IncIC ((p +* q),k) = p +* (IncIC (q,k))

proof end;

theorem Th198: :: COMPOS_1:198

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, q being PartState of S
for k being Nat st IC in dom q holds
DecIC ((p +* q),k) = p +* (DecIC (q,k))

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 l be Nat;
let p be l -started PartState of S;
cluster NPP p -> l -started ;
coherence
NPP p is l -started

proof end;

end;

theorem Th199: :: COMPOS_1:199

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 k, l being Nat holds (p +* (Start-At (k,S))) +* (Start-At (l,S)) = p +* (Start-At (l,S))

proof end;

theorem Th200: :: COMPOS_1:200

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 in dom p holds
p +* (Start-At ((IC p),S)) = p

proof end;

theorem Th201: :: COMPOS_1:201

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 k being Nat st IC in dom p holds
DecIC ((IncIC (p,k)),k) = p

proof end;

theorem :: COMPOS_1:202

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, q being PartState of S
for k being Nat st IC in dom q holds
DecIC ((p +* (IncIC (q,k))),k) = p +* q

proof end;

theorem :: COMPOS_1:203

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for k being Element of NAT
for p being FinPartState of S
for s1, s2 being State of S st NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
NPP p c= s1 +* (DataPart s2)

proof end;

theorem :: COMPOS_1:204

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 k being Nat holds
( Start-At (k,S) c= p iff Start-At (k,S) c= NPP p )

proof end;

theorem :: COMPOS_1:205

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for k being Element of NAT
for p being FinPartState of S st IC in dom p holds
NPP (Relocated (p,k)) = IncIC ((NPP p),k)

proof end;

theorem Th206: :: COMPOS_1:206

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 ProgramPart (Initialize p) = ProgramPart p

proof end;

theorem :: COMPOS_1:207

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for p being FinPartState of S holds NPP (Initialize p) = Initialize (NPP p)

proof end;

theorem Th208: :: COMPOS_1:208

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 I being NAT -defined PartState of holds NPP 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 realistic COM-Struct of N;
let I be NAT -defined PartState of ;
cluster NPP I -> empty ;
coherence
NPP I is empty by Th208;

end;

theorem Th209: :: COMPOS_1:209

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 I being NAT -defined PartState of holds DataPart I = 0

proof end;

theorem Th210: :: COMPOS_1:210

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 I being NAT -defined PartState of holds NPP (Initialize I) = Start-At (0,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 program-free PartState of S;
cluster Initialize p -> program-free ;
coherence
Initialize p is program-free

proof end;

end;

theorem :: COMPOS_1:211

for N being non empty with_non-empty_elements set
for S being non empty COM-Struct of N
for d being program-free PartState of S holds dom d misses NAT by Lm40;

theorem Th212: :: COMPOS_1:212

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 program-free PartState of S holds NPP p = p

proof end;

theorem :: COMPOS_1:213

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for k being Element of NAT
for p being FinPartState of S st IC in dom p holds
for s1, s2 being State of S st NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
NPP p c= s1 +* (DataPart s2)

proof end;

theorem :: COMPOS_1:214

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 NAT -defined the Instructions of b₂ -valued non halt-free Function
for d being program-free FinPartState of S holds ProgramPart (d +* p) = p

proof end;

theorem :: COMPOS_1:215

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 NAT -defined the Instructions of b₂ -valued Function
for p being PartState of S holds NPP (p +* P) = NPP p

proof end;

theorem :: COMPOS_1:216

for N being non empty with_non-empty_elements set
for l being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S st Start-At (l,S) c= p holds
Start-At (l,S) c= NPP p

proof end;

theorem :: COMPOS_1:217

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, q being PartState of S st DataPart p c= q holds
DataPart p c= NPP q

proof end;

theorem :: COMPOS_1:218

for N being non empty with_non-empty_elements set
for x being set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N st x in Data-Locations S holds
for p being PartState of S holds p . x = (NPP p) . x

proof end;

theorem :: COMPOS_1:219

for N being non empty with_non-empty_elements set
for x being set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N st x in Data-Locations S holds
for p being PartState of S st x in dom p holds
x in dom (NPP p)

proof end;

theorem :: COMPOS_1:220

for N being non empty with_non-empty_elements set
for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S
for p being PartState of S st NPP (p +* (Start-At (n,S))) c= s holds
IC s = n

proof end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated realistic COM-Struct of N;
let k be Element of NAT ;
cluster Start-At (k,S) -> program-free ;
coherence
Start-At (k,S) is program-free

proof end;

end;

theorem Th221: :: COMPOS_1:221

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, q being PartState of S holds NPP (p +* q) = (NPP p) +* (NPP q) by Lm221;

theorem :: COMPOS_1:222

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 Start-At (0,S) c= p holds
IC p = 0

proof end;

theorem :: COMPOS_1:223

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 p being PartState of S st Initialize p c= s holds
IC s = 0

proof end;

theorem :: COMPOS_1:224

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 NAT -defined the Instructions of b₂ -valued Function
for p being PartState of S holds NPP (P +* p) = NPP p

proof end;

theorem Th225: :: COMPOS_1:225

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 in dom (Initialize p)

proof end;

theorem :: COMPOS_1:226

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, q being PartState of S holds IC in dom (p +* (Initialize q))

proof end;

theorem :: COMPOS_1:227

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 I being NAT -defined PartState of holds NPP (Initialize I) c= Initialize p

proof end;

theorem :: COMPOS_1:228

for N being non empty with_non-empty_elements set
for l being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S st Start-At (l,S) c= p holds
IC p = l

proof end;

theorem :: COMPOS_1:229

for N being non empty with_non-empty_elements set
for l being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S holds NPP (DecIC (s,l)) = DecIC ((NPP s),l)

proof end;

theorem :: COMPOS_1:230

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 NPP s1 = NPP s2 holds
IC s1 = IC s2

proof end;

theorem :: COMPOS_1:231

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 NPP s = s | ((Data-Locations S) \/ {(IC )}) by LmAA;

theorem Th232: :: COMPOS_1:232

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 NPP s = s | ((dom s) \ NAT)

proof end;

theorem :: COMPOS_1:233

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 s1, s2 being State of S holds
( NPP s1 = NPP s2 iff s1 | ((dom s1) \ NAT) = s2 | ((dom s2) \ NAT) )

proof end;

theorem :: COMPOS_1:234

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 k being Element of NAT
for x being Instruction of S holds NPP (s +* (k,x)) = NPP s

proof end;

theorem :: COMPOS_1:235

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 s1, s2 being State of S st NPP s1 = NPP s2 holds
NPP (s1 +* p) = NPP (s2 +* p)

proof end;

theorem :: COMPOS_1:236

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 p being NAT -defined PartState of holds NPP s = NPP (s +* p)

proof end;

theorem :: COMPOS_1:237

canceled;

theorem :: COMPOS_1:238

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 s1, s2 being State of S
for p being PartState of S st NPP s1 = NPP s2 & dom p = NAT holds
s1 +* p = s2 +* p

proof end;

theorem :: COMPOS_1:239

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 s1, s2 being State of S st ProgramPart s1 = ProgramPart s2 & NPP s1 = NPP s2 holds
s1 = s2

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 l be Element of NAT ;
let s be State of S;
cluster s +* ((IC ),l) -> the Object-Kind of S -compatible ;
coherence
s +* ((IC ),l) is the Object-Kind of S -compatible

proof end;

end;

theorem :: COMPOS_1:240

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 IC (NPP s) = IC s

proof end;

theorem :: COMPOS_1:241

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 p being PartState of S holds (NPP s) | (dom (DataPart p)) = s | (dom (DataPart p))

proof end;

theorem :: COMPOS_1:242

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 (NPP s) | {(IC )} = s | {(IC )}

proof end;