:: AMISTD_1 semantic presentation
theorem Th1: :: AMISTD_1:1
theorem Th2: :: AMISTD_1:2
theorem Th3: :: AMISTD_1:3
theorem Th4: :: AMISTD_1:4
canceled;
theorem Th5: :: AMISTD_1:5
theorem Th6: :: AMISTD_1:6
theorem Th7: :: AMISTD_1:7
theorem Th8: :: AMISTD_1:8
theorem Th9: :: AMISTD_1:9
theorem Th10: :: AMISTD_1:10
theorem Th11: :: AMISTD_1:11
Lemma10:
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b1
for b3 being Instruction-Location of b2
for b4 being Element of the Instructions of b2
for b5 being FinPartState of b2 st b5 = b3 .--> b4 holds
b5 is autonomic
theorem Th12: :: AMISTD_1:12
theorem Th13: :: AMISTD_1:13
:: deftheorem Def1 AMISTD_1:def 1 :
canceled;
:: deftheorem Def2 AMISTD_1:def 2 :
canceled;
:: deftheorem Def3 defines jump-only AMISTD_1:def 3 :
:: deftheorem Def4 defines jump-only AMISTD_1:def 4 :
:: deftheorem Def5 defines NIC AMISTD_1:def 5 :
E12:
now
let c1 be
with_non-empty_elements set ;
let c2 be non
empty non
void IC-Ins-separated definite realistic AMI-Struct of
c1;
let c3 be
Element of the
Instructions of
c2;
let c4 be
Instruction-Location of
c2;
let c5 be
State of
c2;
let c6 be
FinPartState of
c2;
assume E13:
c6 = (IC c2),
c4 --> c4,
c3
;
set c7 =
c5 +* c6;
E14:
IC c2 <> c4
by AMI_1:48;
E15:
dom c6 = {(IC c2),c4}
by E13, FUNCT_4:65;
then E16:
IC c2 in dom c6
by TARSKI:def 2;
E17:
IC (c5 +* c6) =
(c5 +* c6) . (IC c2)
.=
c6 . (IC c2)
by E16, FUNCT_4:14
.=
c4
by E13, E14, FUNCT_4:66
;
c4 in dom c6
by E15, TARSKI:def 2;
then (c5 +* c6) . c4 =
c6 . c4
by FUNCT_4:14
.=
c3
by E13, E14, FUNCT_4:66
;
hence
IC (Following (c5 +* c6)) in NIC c3,
c4
by E17;
end;
:: deftheorem Def6 defines JUMP AMISTD_1:def 6 :
:: deftheorem Def7 defines SUCC AMISTD_1:def 7 :
theorem Th14: :: AMISTD_1:14
theorem Th15: :: AMISTD_1:15
:: deftheorem Def8 defines <= AMISTD_1:def 8 :
theorem Th16: :: AMISTD_1:16
:: deftheorem Def9 defines InsLoc-antisymmetric AMISTD_1:def 9 :
:: deftheorem Def10 defines standard AMISTD_1:def 10 :
theorem Th17: :: AMISTD_1:17
theorem Th18: :: AMISTD_1:18
theorem Th19: :: AMISTD_1:19
Lemma20:
for b1, b2 being set holds dom ((NAT --> b1) +* (NAT .--> b2)) = NAT \/ {NAT }
set c1 = {[1,0],[0,0]};
definition
let c2 be
with_non-empty_elements set ;
func STC c1 -> strict AMI-Struct of
a1 means :
Def11:
:: AMISTD_1:def 11
( the
carrier of
a2 = NAT \/ {NAT } & the
Instruction-Counter of
a2 = NAT & the
Instruction-Locations of
a2 = NAT & the
Instruction-Codes of
a2 = {0,1} & the
Instructions of
a2 = {[0,0],[1,0]} & the
Object-Kind of
a2 = (NAT --> {[1,0],[0,0]}) +* (NAT .--> NAT ) & ex
b1 being
Function of
product the
Object-Kind of
a2,
product the
Object-Kind of
a2 st
( ( for
b2 being
Element of
product the
Object-Kind of
a2 holds
b1 . b2 = b2 +* (NAT .--> (succ (b2 . NAT ))) ) & the
Execution of
a2 = ([1,0] .--> b1) +* ([0,0] .--> (id (product the Object-Kind of a2))) ) );
existence
ex b1 being strict AMI-Struct of c2 st
( the carrier of b1 = NAT \/ {NAT } & the Instruction-Counter of b1 = NAT & the Instruction-Locations of b1 = NAT & the Instruction-Codes of b1 = {0,1} & the Instructions of b1 = {[0,0],[1,0]} & the Object-Kind of b1 = (NAT --> {[1,0],[0,0]}) +* (NAT .--> NAT ) & ex b2 being Function of product the Object-Kind of b1, product the Object-Kind of b1 st
( ( for b3 being Element of product the Object-Kind of b1 holds b2 . b3 = b3 +* (NAT .--> (succ (b3 . NAT ))) ) & the Execution of b1 = ([1,0] .--> b2) +* ([0,0] .--> (id (product the Object-Kind of b1))) ) )
uniqueness
for b1, b2 being strict AMI-Struct of c2 st the carrier of b1 = NAT \/ {NAT } & the Instruction-Counter of b1 = NAT & the Instruction-Locations of b1 = NAT & the Instruction-Codes of b1 = {0,1} & the Instructions of b1 = {[0,0],[1,0]} & the Object-Kind of b1 = (NAT --> {[1,0],[0,0]}) +* (NAT .--> NAT ) & ex b3 being Function of product the Object-Kind of b1, product the Object-Kind of b1 st
( ( for b4 being Element of product the Object-Kind of b1 holds b3 . b4 = b4 +* (NAT .--> (succ (b4 . NAT ))) ) & the Execution of b1 = ([1,0] .--> b3) +* ([0,0] .--> (id (product the Object-Kind of b1))) ) & the carrier of b2 = NAT \/ {NAT } & the Instruction-Counter of b2 = NAT & the Instruction-Locations of b2 = NAT & the Instruction-Codes of b2 = {0,1} & the Instructions of b2 = {[0,0],[1,0]} & the Object-Kind of b2 = (NAT --> {[1,0],[0,0]}) +* (NAT .--> NAT ) & ex b3 being Function of product the Object-Kind of b2, product the Object-Kind of b2 st
( ( for b4 being Element of product the Object-Kind of b2 holds b3 . b4 = b4 +* (NAT .--> (succ (b4 . NAT ))) ) & the Execution of b2 = ([1,0] .--> b3) +* ([0,0] .--> (id (product the Object-Kind of b2))) ) holds
b1 = b2
end;
:: deftheorem Def11 defines STC AMISTD_1:def 11 :
for
b1 being
with_non-empty_elements set for
b2 being
strict AMI-Struct of
b1 holds
(
b2 = STC b1 iff ( the
carrier of
b2 = NAT \/ {NAT } & the
Instruction-Counter of
b2 = NAT & the
Instruction-Locations of
b2 = NAT & the
Instruction-Codes of
b2 = {0,1} & the
Instructions of
b2 = {[0,0],[1,0]} & the
Object-Kind of
b2 = (NAT --> {[1,0],[0,0]}) +* (NAT .--> NAT ) & ex
b3 being
Function of
product the
Object-Kind of
b2,
product the
Object-Kind of
b2 st
( ( for
b4 being
Element of
product the
Object-Kind of
b2 holds
b3 . b4 = b4 +* (NAT .--> (succ (b4 . NAT ))) ) & the
Execution of
b2 = ([1,0] .--> b3) +* ([0,0] .--> (id (product the Object-Kind of b2))) ) ) );
Lemma22:
for b1 being with_non-empty_elements set
for b2 being Instruction of (STC b1)
for b3 being State of (STC b1) st InsCode b2 = 1 holds
(Exec b2,b3) . (IC (STC b1)) = succ (IC b3)
theorem Th20: :: AMISTD_1:20
theorem Th21: :: AMISTD_1:21
theorem Th22: :: AMISTD_1:22
theorem Th23: :: AMISTD_1:23
Lemma26:
for b1 being natural number
for b2 being with_non-empty_elements set
for b3 being Instruction-Location of (STC b2)
for b4 being Element of the Instructions of (STC b2) st b3 = b1 & InsCode b4 = 1 holds
NIC b4,b3 = {(b1 + 1)}
Lemma27:
for b1 being with_non-empty_elements set
for b2 being Element of the Instructions of (STC b1) holds JUMP b2 is empty
theorem Th24: :: AMISTD_1:24
definition
let c2 be
with_non-empty_elements set ;
let c3 be non
empty non
void IC-Ins-separated definite standard AMI-Struct of
c2;
let c4 be
natural number ;
func il. c2,
c3 -> Instruction-Location of
a2 means :
Def12:
:: AMISTD_1:def 12
ex
b1 being
Function of
NAT ,the
Instruction-Locations of
a2 st
(
b1 is
bijective & ( for
b2,
b3 being
Nat holds
(
b2 <= b3 iff
b1 . b2 <= b1 . b3 ) ) &
a4 = b1 . a3 );
existence
ex b1 being Instruction-Location of c3ex b2 being Function of NAT ,the Instruction-Locations of c3 st
( b2 is bijective & ( for b3, b4 being Nat holds
( b3 <= b4 iff b2 . b3 <= b2 . b4 ) ) & b1 = b2 . c4 )
uniqueness
for b1, b2 being Instruction-Location of c3 st ex b3 being Function of NAT ,the Instruction-Locations of c3 st
( b3 is bijective & ( for b4, b5 being Nat holds
( b4 <= b5 iff b3 . b4 <= b3 . b5 ) ) & b1 = b3 . c4 ) & ex b3 being Function of NAT ,the Instruction-Locations of c3 st
( b3 is bijective & ( for b4, b5 being Nat holds
( b4 <= b5 iff b3 . b4 <= b3 . b5 ) ) & b2 = b3 . c4 ) holds
b1 = b2
by Th17;
end;
:: deftheorem Def12 defines il. AMISTD_1:def 12 :
theorem Th25: :: AMISTD_1:25
theorem Th26: :: AMISTD_1:26
:: deftheorem Def13 defines locnum AMISTD_1:def 13 :
theorem Th27: :: AMISTD_1:27
theorem Th28: :: AMISTD_1:28
theorem Th29: :: AMISTD_1:29
theorem Th30: :: AMISTD_1:30
:: deftheorem Def14 defines + AMISTD_1:def 14 :
theorem Th31: :: AMISTD_1:31
theorem Th32: :: AMISTD_1:32
theorem Th33: :: AMISTD_1:33
:: deftheorem Def15 defines NextLoc AMISTD_1:def 15 :
theorem Th34: :: AMISTD_1:34
theorem Th35: :: AMISTD_1:35
theorem Th36: :: AMISTD_1:36
theorem Th37: :: AMISTD_1:37
theorem Th38: :: AMISTD_1:38
theorem Th39: :: AMISTD_1:39
theorem Th40: :: AMISTD_1:40
:: deftheorem Def16 defines sequential AMISTD_1:def 16 :
theorem Th41: :: AMISTD_1:41
theorem Th42: :: AMISTD_1:42
theorem Th43: :: AMISTD_1:43
:: deftheorem Def17 defines closed AMISTD_1:def 17 :
:: deftheorem Def18 defines really-closed AMISTD_1:def 18 :
:: deftheorem Def19 defines para-closed AMISTD_1:def 19 :
theorem Th44: :: AMISTD_1:44
theorem Th45: :: AMISTD_1:45
theorem Th46: :: AMISTD_1:46
:: deftheorem Def20 defines lower AMISTD_1:def 20 :
theorem Th47: :: AMISTD_1:47
theorem Th48: :: AMISTD_1:48
theorem Th49: :: AMISTD_1:49
theorem Th50: :: AMISTD_1:50
:: deftheorem Def21 defines LastLoc AMISTD_1:def 21 :
theorem Th51: :: AMISTD_1:51
theorem Th52: :: AMISTD_1:52
theorem Th53: :: AMISTD_1:53
theorem Th54: :: AMISTD_1:54
theorem Th55: :: AMISTD_1:55
E54:
now
let c2 be
with_non-empty_elements set ;
let c3 be non
empty non
void halting IC-Ins-separated definite standard AMI-Struct of
c2;
set c4 =
(il. c3,0) .--> (halt c3);
E55:
dom ((il. c3,0) .--> (halt c3)) = {(il. c3,0)}
by CQC_LANG:5;
then E56:
card (dom ((il. c3,0) .--> (halt c3))) = 1
by CARD_1:79;
(il. c3,0) .--> (halt c3) is
lower FinPartState of
c3
by Th48;
then E57:
LastLoc ((il. c3,0) .--> (halt c3)) =
il. c3,
((card ((il. c3,0) .--> (halt c3))) -' 1)
by Th55
.=
il. c3,
((card (dom ((il. c3,0) .--> (halt c3)))) -' 1)
by PRE_CIRC:21
.=
il. c3,0
by E56, BINARITH:51
;
hence
((il. c3,0) .--> (halt c3)) . (LastLoc ((il. c3,0) .--> (halt c3))) = halt c3
by CQC_LANG:6;
let c5 be
Instruction-Location of
c3;
assume
((il. c3,0) .--> (halt c3)) . c5 = halt c3
;
assume
c5 in dom ((il. c3,0) .--> (halt c3))
;
hence
c5 = LastLoc ((il. c3,0) .--> (halt c3))
by E55, E57, TARSKI:def 1;
end;
:: deftheorem Def22 defines halt-ending AMISTD_1:def 22 :
:: deftheorem Def23 defines unique-halt AMISTD_1:def 23 :