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
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
:: deftheorem AMISTD_2:def 1 :
canceled;
:: deftheorem AMISTD_2:def 2 :
canceled;
theorem Th13:
theorem Th14:
theorem Th15:
:: deftheorem defines AddressPart AMISTD_2:def 3 :
:: deftheorem Def4 defines homogeneous AMISTD_2:def 4 :
theorem
canceled;
theorem Th17:
:: deftheorem defines AddressParts AMISTD_2:def 5 :
:: deftheorem Def6 defines with_explicit_jumps AMISTD_2:def 6 :
:: deftheorem Def7 defines without_implicit_jumps AMISTD_2:def 7 :
:: deftheorem Def8 defines with_explicit_jumps AMISTD_2:def 8 :
:: deftheorem Def9 defines without_implicit_jumps AMISTD_2:def 9 :
theorem Th18:
:: deftheorem AMISTD_2:def 10 :
canceled;
:: deftheorem Def11 defines regular AMISTD_2:def 11 :
theorem Th19:
Lm3:
for N being with_non-empty_elements set
for I being Instruction of (Trivial-AMI N) holds AddressPart I = 0
Lm4:
for N being with_non-empty_elements set
for T being InsType of (Trivial-AMI N) holds AddressParts T = {0 }
theorem Th20:
theorem Th21:
:: deftheorem Def12 defines ins-loc-free AMISTD_2:def 12 :
theorem
theorem Th23:
theorem Th24:
:: deftheorem defines Stop AMISTD_2:def 13 :
theorem Th25:
theorem Th26:
Lm6:
for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of N holds (card (Stop S)) -' 1 = 0
theorem Th27:
begin
:: deftheorem Def14 defines IncAddr AMISTD_2:def 14 :
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem Th37:
definition
let N be
with_non-empty_elements set ;
let S be non
empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of
N;
let p be
NAT -defined FinPartState of
S;
let k be
natural number ;
A1:
dom p c= NAT
by RELAT_1:def 18;
func IncAddr p,
k -> FinPartState of
S means :
Def15:
(
dom it = dom p & ( for
m being
natural number st
il. S,
m in dom p holds
it . (il. S,m) = IncAddr (pi p,(il. S,m)),
k ) );
existence
ex b1 being FinPartState of S st
( dom b1 = dom p & ( for m being natural number st il. S,m in dom p holds
b1 . (il. S,m) = IncAddr (pi p,(il. S,m)),k ) )
uniqueness
for b1, b2 being FinPartState of S st dom b1 = dom p & ( for m being natural number st il. S,m in dom p holds
b1 . (il. S,m) = IncAddr (pi p,(il. S,m)),k ) & dom b2 = dom p & ( for m being natural number st il. S,m in dom p holds
b2 . (il. S,m) = IncAddr (pi p,(il. S,m)),k ) holds
b1 = b2
end;
:: deftheorem Def15 defines IncAddr AMISTD_2:def 15 :
theorem Th38:
theorem
definition
let N be
with_non-empty_elements set ;
let S be non
empty stored-program IC-Ins-separated definite standard AMI-Struct of
N;
let p be
FinPartState of
S;
let k be
natural number ;
func Shift p,
k -> FinPartState of
S means :
Def16:
(
dom it = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } & ( for
m being
Element of
NAT st
il. S,
m in dom p holds
it . (il. S,(m + k)) = p . (il. S,m) ) );
existence
ex b1 being FinPartState of S st
( dom b1 = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } & ( for m being Element of NAT st il. S,m in dom p holds
b1 . (il. S,(m + k)) = p . (il. S,m) ) )
uniqueness
for b1, b2 being FinPartState of S st dom b1 = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } & ( for m being Element of NAT st il. S,m in dom p holds
b1 . (il. S,(m + k)) = p . (il. S,m) ) & dom b2 = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } & ( for m being Element of NAT st il. S,m in dom p holds
b2 . (il. S,(m + k)) = p . (il. S,m) ) holds
b1 = b2
end;
:: deftheorem Def16 defines Shift AMISTD_2:def 16 :
theorem Th40:
theorem Th41:
theorem
theorem Th43:
:: deftheorem Def17 defines IC-good AMISTD_2:def 17 :
:: deftheorem Def18 defines IC-good AMISTD_2:def 18 :
:: deftheorem Def19 defines Exec-preserving AMISTD_2:def 19 :
:: deftheorem Def20 defines Exec-preserving AMISTD_2:def 20 :
theorem Th44:
theorem Th45:
theorem Th46:
:: deftheorem defines CutLastLoc AMISTD_2:def 21 :
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
:: deftheorem defines ';' AMISTD_2:def 22 :
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem
theorem
theorem
theorem
begin
theorem Th65:
theorem
Lm7:
for a, b, c being set st a c= c & b c= c \ a holds
c = (a \/ (c \ (a \/ b))) \/ b
Lm8:
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N holds NAT c= the carrier of S \ {(IC S)}
theorem
:: deftheorem defines Relocated AMISTD_2:def 23 :
theorem
theorem Th69:
theorem Th70:
theorem
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem
theorem
Lm10:
for a, b, c being set holds not c in a \ ({c} \/ b)
theorem