begin
definition
let N be
set ;
func Trivial-COM N -> strict COM-Struct of
N means :
Def2:
( the
carrier of
it = succ NAT & the
Instruction-Counter of
it = NAT & the
Instructions of
it = {[0,{},{}]} & the
haltF of
it = [0,{},{}] & the
Object-Kind of
it = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) );
existence
ex b1 being strict COM-Struct of N st
( the carrier of b1 = succ NAT & the Instruction-Counter of b1 = NAT & the Instructions of b1 = {[0,{},{}]} & the haltF of b1 = [0,{},{}] & the Object-Kind of b1 = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) )
uniqueness
for b1, b2 being strict COM-Struct of N st the carrier of b1 = succ NAT & the Instruction-Counter of b1 = NAT & the Instructions of b1 = {[0,{},{}]} & the haltF of b1 = [0,{},{}] & the Object-Kind of b1 = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) & the carrier of b2 = succ NAT & the Instruction-Counter of b2 = NAT & the Instructions of b2 = {[0,{},{}]} & the haltF of b2 = [0,{},{}] & the Object-Kind of b2 = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) holds
b1 = b2
;
end;
:: deftheorem Def2 defines Trivial-COM COMPOS_1:def 1 :
for N being set
for b2 being strict COM-Struct of N holds
( b2 = Trivial-COM N iff ( the carrier of b2 = succ NAT & the Instruction-Counter of b2 = NAT & the Instructions of b2 = {[0,{},{}]} & the haltF of b2 = [0,{},{}] & the Object-Kind of b2 = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) ) );
:: deftheorem Def3 defines stored-program COMPOS_1:def 2 :
for N being set
for S being COM-Struct of N holds
( S is stored-program iff NAT c= the carrier of S );
:: deftheorem defines IC COMPOS_1:def 3 :
for N being set
for S being non empty COM-Struct of N holds IC S = the Instruction-Counter of S;
:: 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;
:: 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;
:: deftheorem Def11 defines IC-Ins-separated COMPOS_1:def 6 :
for N being set
for IT being non empty COM-Struct of N holds
( IT is IC-Ins-separated iff ObjectKind (IC IT) = NAT );
:: 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 b2 -compatible Function holds
( I is halt-free iff not halt S in rng I );
:: 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 );
:: deftheorem defines IC COMPOS_1:def 9 :
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for p being PartState of S holds IC p = p . (IC S);
theorem
begin
:: 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 b2 -valued Function
for s being State of S holds CurInstr (p,s) = p /. (IC s);
:: deftheorem defines ProgramPart COMPOS_1:def 11 :
for N being with_non-empty_elements set
for S being COM-Struct of N
for s being PartState of S holds ProgramPart s = s | NAT;
BWL:
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
BWL2:
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 PartState of S
for i being natural number st i in dom s holds
(ProgramPart s) . i = s . i
LmU:
for N being with_non-empty_elements set
for S being non empty stored-program COM-Struct of N
for s being State of S holds dom (ProgramPart s) = NAT
BWL1:
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite COM-Struct of N
for s being State of S
for i being natural number holds (ProgramPart s) /. i = s . i
:: deftheorem Def21 defines realistic COMPOS_1:def 12 :
for N being set
for IT being COM-Struct of N holds
( IT is realistic iff not the Instruction-Counter of IT in NAT );
theorem
theorem Th3:
LmL:
for N being with_non-empty_elements set
for S being stored-program COM-Struct of N
for s being State of S holds NAT c= dom s
L94:
for N being with_non-empty_elements set
for S being non empty COM-Struct of N
for s being State of S holds IC S in dom s
begin
:: 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 } ;
:: deftheorem defines Data-Locations COMPOS_1:def 14 :
for N being set
for S being non empty COM-Struct of N holds Data-Locations S = the carrier of S \ ({(IC S)} \/ NAT);
theorem Th4:
theorem Th5:
:: deftheorem defines Start-At COMPOS_1:def 15 :
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for l being Nat holds Start-At (l,S) = (IC S) .--> l;
begin
theorem
:: deftheorem Def41 defines -started COMPOS_1:def 16 :
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated COM-Struct of N
for l being Nat
for p being PartState of S holds
( p is l -started iff ( IC S in dom p & IC p = l ) );
begin
:: 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 *):] );
:: 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);
begin
LMT:
for N being with_non-empty_elements set
for S being COM-Struct of N
for p being FinPartState of S holds p in FinPartSt S
theorem Th7:
:: deftheorem Def42 defines halts_at COMPOS_1:def 19 :
for N being with_non-empty_elements set
for S being COM-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for l being set holds
( p halts_at l iff ( l in dom p & p . l = halt S ) );
:: 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 );
:: 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 b2 -valued ManySortedSet of NAT
for l being Nat holds
( s halts_at l iff s . l = halt S );
theorem
theorem Th9:
theorem
:: 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);
:: deftheorem Def50 defines data-only COMPOS_1:def 23 :
for N being set
for S being non empty COM-Struct of N
for IT being PartState of S holds
( IT is data-only iff dom IT misses {(IC S)} \/ NAT );
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem
theorem Th18:
:: 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
theorem
theorem
theorem
theorem Th23:
theorem
theorem
theorem Th26:
theorem Th135:
theorem
theorem
theorem Th30:
theorem Th31:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th155:
begin
theorem
begin
:: 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 );
theorem
begin
theorem
theorem
begin
:: 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)%>;
theorem
theorem Th46:
:: deftheorem defines IncrIC 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 IncrIC (p,k) = p +* (Start-At (((IC p) + k),S));
theorem
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem
theorem Th56:
theorem Th22:
theorem Th58:
theorem Th24:
theorem Th60:
theorem
theorem
theorem
theorem
:: deftheorem Def29 defines program-free COMPOS_1:def 29 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds
( p is program-free iff p | NAT = {} );
:: deftheorem defines NPP COMPOS_1:def 30 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds NPP p = p \ (ProgramPart p);
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th43:
theorem
theorem Th45:
theorem
theorem Th72:
theorem Th73:
theorem Th74:
theorem
begin
:: 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));
theorem Th27:
theorem
theorem Th78:
theorem
theorem
theorem
theorem
theorem
theorem
begin
Lm1:
for k being natural number holds - 1 < k
;
Lm2:
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
begin
:: 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 } ;
:: deftheorem Def4 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:
:: 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 } ;
:: deftheorem Def11 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 Dfs 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:
Lm3:
for N being non empty with_non-empty_elements set
for I being Instruction of (Trivial-COM N) holds JumpPart I = 0
Lm4:
for N being non empty with_non-empty_elements set
for T being InsType of (Trivial-COM N) holds JumpParts T = {0}
theorem
:: 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 );
theorem Th25:
theorem Th89:
Lm6:
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
theorem Th27:
begin
:: 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 b5 being Instruction of S holds
( b5 = IncAddr (I,k) iff ( InsCode b5 = InsCode I & AddressPart b5 = AddressPart I & JumpPart b5 = k + (JumpPart I) ) );
theorem Th28:
theorem Th29:
:: 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 );
theorem
theorem
theorem Th34:
theorem Th35:
theorem Th37:
:: deftheorem Def15 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 b2 -valued finite Function
for k being natural number
for b5 being FinPartState of S holds
( b5 = IncAddr (p,k) iff ( dom b5 = dom p & ( for m being natural number st m in dom p holds
b5 . m = IncAddr ((p /. m),k) ) ) );
theorem Th38:
theorem
:: 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 b2 -valued finite Function
for k being Element of NAT holds Reloc (p,k) = IncAddr ((Shift (p,k)),k);
theorem Th100:
theorem Th101:
:: 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 b2 -valued FinPartState of holds F ';' G = (CutLastLoc F) +* (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)));
theorem Th102:
theorem
theorem Th104:
theorem Th55:
theorem
theorem Th57:
theorem Th108:
theorem Th5:
theorem Th110:
theorem
theorem
theorem
theorem
begin
:: 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) = (IncrIC ((NPP p),k)) +* (Reloc ((ProgramPart p),k));
theorem
theorem Th69:
theorem Th70:
theorem
theorem Th119:
theorem Th73:
theorem Th75:
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem Th32:
theorem
theorem Th54:
theorem Th56:
theorem
theorem
:: 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);
theorem
theorem
begin
:: 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));
theorem
theorem Th137:
theorem
theorem Th47:
begin
theorem Th64:
theorem Th65:
theorem Th66:
theorem
begin
theorem
theorem
theorem
theorem Th147:
theorem
begin
theorem
theorem
theorem
theorem Th152: