:: On the Composition of Macro Instructions of Standard Computers
:: by Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000 Association of Mizar Users
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
theorem :: AMISTD_2:1
canceled;
theorem :: AMISTD_2:2
canceled;
theorem :: AMISTD_2:3
canceled;
theorem :: AMISTD_2:4
canceled;
theorem :: AMISTD_2:5
canceled;
theorem :: AMISTD_2:6
canceled;
theorem :: AMISTD_2:7
canceled;
theorem :: AMISTD_2:8
canceled;
theorem :: AMISTD_2:9
canceled;
theorem :: AMISTD_2:10
canceled;
theorem :: AMISTD_2:11
theorem Th12: :: AMISTD_2:12
:: deftheorem AMISTD_2:def 1 :
canceled;
:: deftheorem AMISTD_2:def 2 :
canceled;
theorem Th13: :: AMISTD_2:13
theorem Th14: :: AMISTD_2:14
theorem Th15: :: AMISTD_2:15
:: deftheorem defines AddressPart AMISTD_2:def 3 :
theorem Th16: :: AMISTD_2:16
:: deftheorem Def4 defines homogeneous AMISTD_2:def 4 :
theorem Th17: :: AMISTD_2:17
:: 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: :: AMISTD_2:18
:: deftheorem AMISTD_2:def 10 :
canceled;
:: deftheorem Def11 defines regular AMISTD_2:def 11 :
theorem Th19: :: AMISTD_2:19
Lm3:
for N being with_non-empty_elements set
for IL being non empty set
for I being Instruction of (Trivial-AMI IL,N) holds AddressPart I = 0
Lm4:
for N being with_non-empty_elements set
for IL being non empty set
for T being InsType of (Trivial-AMI IL,N) holds AddressParts T = {0 }
theorem Th20: :: AMISTD_2:20
theorem Th21: :: AMISTD_2:21
:: deftheorem Def12 defines ins-loc-free AMISTD_2:def 12 :
theorem :: AMISTD_2:22
theorem Th23: :: AMISTD_2:23
theorem Th24: :: AMISTD_2:24
:: deftheorem defines Stop AMISTD_2:def 13 :
theorem Th25: :: AMISTD_2:25
theorem Th26: :: AMISTD_2:26
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 NAT ,N holds (card (Stop S)) -' 1 = 0
theorem Th27: :: AMISTD_2:27
:: deftheorem Def14 defines IncAddr AMISTD_2:def 14 :
theorem Th28: :: AMISTD_2:28
theorem Th29: :: AMISTD_2:29
theorem :: AMISTD_2:30
theorem Th31: :: AMISTD_2:31
theorem Th32: :: AMISTD_2:32
theorem Th33: :: AMISTD_2:33
theorem Th34: :: AMISTD_2:34
theorem Th35: :: AMISTD_2:35
theorem :: AMISTD_2:36
theorem Th37: :: AMISTD_2:37
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
NAT ,
N;
let p be
programmed FinPartState of
S;
let k be
natural number ;
A1:
dom p c= NAT
by AMI_1:def 40;
func IncAddr p,
k -> FinPartState of
S means :
Def15:
:: AMISTD_2:def 15
(
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: :: AMISTD_2:38
theorem :: AMISTD_2:39
definition
let N be
with_non-empty_elements set ;
let S be non
empty stored-program IC-Ins-separated definite standard AMI-Struct of
NAT ,
N;
let p be
FinPartState of
S;
let k be
natural number ;
func Shift p,
k -> FinPartState of
S means :
Def16:
:: AMISTD_2:def 16
(
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: :: AMISTD_2:40
theorem Th41: :: AMISTD_2:41
theorem :: AMISTD_2:42
theorem Th43: :: AMISTD_2:43
:: 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: :: AMISTD_2:44
theorem Th45: :: AMISTD_2:45
theorem Th46: :: AMISTD_2:46
:: deftheorem defines CutLastLoc AMISTD_2:def 21 :
theorem Th47: :: AMISTD_2:47
theorem Th48: :: AMISTD_2:48
theorem Th49: :: AMISTD_2:49
theorem Th50: :: AMISTD_2:50
theorem Th51: :: AMISTD_2:51
:: deftheorem defines ';' AMISTD_2:def 22 :
theorem Th52: :: AMISTD_2:52
theorem Th53: :: AMISTD_2:53
theorem Th54: :: AMISTD_2:54
theorem Th55: :: AMISTD_2:55
theorem :: AMISTD_2:56
theorem Th57: :: AMISTD_2:57
theorem Th58: :: AMISTD_2:58
theorem Th59: :: AMISTD_2:59
theorem Th60: :: AMISTD_2:60
theorem :: AMISTD_2:61
theorem :: AMISTD_2:62
theorem :: AMISTD_2:63
theorem :: AMISTD_2:64
theorem Th65: :: AMISTD_2:65
theorem :: AMISTD_2:66
Lm4:
for a, b, c being set st a c= c & b c= c \ a holds
c = (a \/ (c \ (a \/ b))) \/ b
Lm5:
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N holds IL c= the carrier of S \ {(IC S)}
theorem :: AMISTD_2:67
:: deftheorem defines Relocated AMISTD_2:def 23 :
theorem :: AMISTD_2:68
theorem Th48: :: AMISTD_2:69
theorem Th49: :: AMISTD_2:70
theorem :: AMISTD_2:71
theorem Th51: :: AMISTD_2:72
theorem Th52: :: AMISTD_2:73
theorem Th53: :: AMISTD_2:74
theorem Th54: :: AMISTD_2:75
theorem :: AMISTD_2:76
theorem :: AMISTD_2:77
Lm2:
for a, b, c being set holds not c in a \ ({c} \/ b)
theorem :: AMISTD_2:78