:: AMI_3 semantic presentation
definition
func SCM -> strict AMI-Struct of
{INT } equals :: AMI_3:def 1
AMI-Struct(#
NAT ,0,
SCM-Instr-Loc ,
(Segm 9),
SCM-Instr ,
SCM-OK ,
SCM-Exec #);
coherence
AMI-Struct(# NAT ,0,SCM-Instr-Loc ,(Segm 9),SCM-Instr ,SCM-OK ,SCM-Exec #) is strict AMI-Struct of {INT }
;
end;
:: deftheorem Def1 defines SCM AMI_3:def 1 :
theorem Th1: :: AMI_3:1
theorem Th2: :: AMI_3:2
:: deftheorem Def2 defines Data-Location AMI_3:def 2 :
definition
let c1,
c2 be
Data-Location ;
func c1 := c2 -> Instruction of
SCM equals :: AMI_3:def 3
[1,<*a1,a2*>];
correctness
coherence
[1,<*c1,c2*>] is Instruction of SCM ;
func AddTo c1,
c2 -> Instruction of
SCM equals :: AMI_3:def 4
[2,<*a1,a2*>];
correctness
coherence
[2,<*c1,c2*>] is Instruction of SCM ;
func SubFrom c1,
c2 -> Instruction of
SCM equals :: AMI_3:def 5
[3,<*a1,a2*>];
correctness
coherence
[3,<*c1,c2*>] is Instruction of SCM ;
func MultBy c1,
c2 -> Instruction of
SCM equals :: AMI_3:def 6
[4,<*a1,a2*>];
correctness
coherence
[4,<*c1,c2*>] is Instruction of SCM ;
func Divide c1,
c2 -> Instruction of
SCM equals :: AMI_3:def 7
[5,<*a1,a2*>];
correctness
coherence
[5,<*c1,c2*>] is Instruction of SCM ;
end;
:: deftheorem Def3 defines := AMI_3:def 3 :
:: deftheorem Def4 defines AddTo AMI_3:def 4 :
:: deftheorem Def5 defines SubFrom AMI_3:def 5 :
:: deftheorem Def6 defines MultBy AMI_3:def 6 :
:: deftheorem Def7 defines Divide AMI_3:def 7 :
definition
let c1 be
Instruction-Location of
SCM ;
func goto c1 -> Instruction of
SCM equals :: AMI_3:def 8
[6,<*a1*>];
correctness
coherence
[6,<*c1*>] is Instruction of SCM ;
by AMI_2:3;
let c2 be
Data-Location ;
func c2 =0_goto c1 -> Instruction of
SCM equals :: AMI_3:def 9
[7,<*a1,a2*>];
correctness
coherence
[7,<*c1,c2*>] is Instruction of SCM ;
func c2 >0_goto c1 -> Instruction of
SCM equals :: AMI_3:def 10
[8,<*a1,a2*>];
correctness
coherence
[8,<*c1,c2*>] is Instruction of SCM ;
end;
:: deftheorem Def8 defines goto AMI_3:def 8 :
:: deftheorem Def9 defines =0_goto AMI_3:def 9 :
:: deftheorem Def10 defines >0_goto AMI_3:def 10 :
theorem Th3: :: AMI_3:3
canceled;
theorem Th4: :: AMI_3:4
theorem Th5: :: AMI_3:5
:: deftheorem Def11 defines Next AMI_3:def 11 :
theorem Th6: :: AMI_3:6
theorem Th7: :: AMI_3:7
theorem Th8: :: AMI_3:8
theorem Th9: :: AMI_3:9
theorem Th10: :: AMI_3:10
theorem Th11: :: AMI_3:11
theorem Th12: :: AMI_3:12
theorem Th13: :: AMI_3:13
theorem Th14: :: AMI_3:14
theorem Th15: :: AMI_3:15
Lemma15:
for b1 being Instruction of SCM st ex b2 being State of SCM st (Exec b1,b2) . (IC SCM ) = Next (IC b2) holds
not b1 is halting
Lemma16:
for b1 being Instruction of SCM st b1 = [0,{} ] holds
b1 is halting
Lemma17:
for b1, b2 being Data-Location holds not b1 := b2 is halting
Lemma18:
for b1, b2 being Data-Location holds not AddTo b1,b2 is halting
Lemma19:
for b1, b2 being Data-Location holds not SubFrom b1,b2 is halting
Lemma20:
for b1, b2 being Data-Location holds not MultBy b1,b2 is halting
Lemma21:
for b1, b2 being Data-Location holds not Divide b1,b2 is halting
Lemma22:
for b1 being Instruction-Location of SCM holds not goto b1 is halting
Lemma23:
for b1 being Data-Location
for b2 being Instruction-Location of SCM holds not b1 =0_goto b2 is halting
Lemma24:
for b1 being Data-Location
for b2 being Instruction-Location of SCM holds not b1 >0_goto b2 is halting
Lemma25:
for b1 being set holds
( b1 is Instruction of SCM iff ( b1 = [0,{} ] or ex b2, b3 being Data-Location st b1 = b2 := b3 or ex b2, b3 being Data-Location st b1 = AddTo b2,b3 or ex b2, b3 being Data-Location st b1 = SubFrom b2,b3 or ex b2, b3 being Data-Location st b1 = MultBy b2,b3 or ex b2, b3 being Data-Location st b1 = Divide b2,b3 or ex b2 being Instruction-Location of SCM st b1 = goto b2 or ex b2 being Data-Location ex b3 being Instruction-Location of SCM st b1 = b2 =0_goto b3 or ex b2 being Data-Location ex b3 being Instruction-Location of SCM st b1 = b2 >0_goto b3 ) )
Lemma26:
for b1 being Instruction of SCM st b1 is halting holds
b1 = halt SCM
Lemma27:
halt SCM = [0,{} ]
theorem Th16: :: AMI_3:16
canceled;
theorem Th17: :: AMI_3:17
canceled;
theorem Th18: :: AMI_3:18
theorem Th19: :: AMI_3:19
Lemma30:
for b1, b2 being Function
for b3, b4 being set st b1 | b3 = b2 | b3 & b1 | b4 = b2 | b4 holds
b1 | (b3 \/ b4) = b2 | (b3 \/ b4)
by RELAT_1:185;
Lemma31:
for b1 being Function
for b2 being set st b2 in dom b1 holds
b1 | {b2} = {[b2,(b1 . b2)]}
by GRFUNC_1:89;
Lemma32:
for b1 being Function
for b2 being set st b2 misses dom b1 holds
b1 | b2 = {}
by RELAT_1:95;
theorem Th20: :: AMI_3:20
canceled;
theorem Th21: :: AMI_3:21
canceled;
theorem Th22: :: AMI_3:22
canceled;
theorem Th23: :: AMI_3:23
canceled;
theorem Th24: :: AMI_3:24
theorem Th25: :: AMI_3:25
theorem Th26: :: AMI_3:26
theorem Th27: :: AMI_3:27
theorem Th28: :: AMI_3:28
canceled;
theorem Th29: :: AMI_3:29
theorem Th30: :: AMI_3:30
canceled;
theorem Th31: :: AMI_3:31
theorem Th32: :: AMI_3:32
theorem Th33: :: AMI_3:33
scheme :: AMI_3:sch 2
s2{
F1()
-> non
empty with_non-empty_elements set ,
F2()
-> AMI-Struct of
F1(),
P1[
set ,
set ],
F3()
-> PartFunc of
FinPartSt F2(),
FinPartSt F2(),
F4()
-> PartFunc of
FinPartSt F2(),
FinPartSt F2() } :
provided
E39:
for
b1,
b2 being
FinPartState of
F2() holds
(
[b1,b2] in F3() iff
P1[
b1,
b2] )
and E40:
for
b1,
b2 being
FinPartState of
F2() holds
(
[b1,b2] in F4() iff
P1[
b1,
b2] )
:: deftheorem Def12 defines Start-At AMI_3:def 12 :
theorem Th34: :: AMI_3:34
:: deftheorem Def13 defines programmed AMI_3:def 13 :
theorem Th35: :: AMI_3:35
theorem Th36: :: AMI_3:36
theorem Th37: :: AMI_3:37
theorem Th38: :: AMI_3:38
:: deftheorem Def14 defines starts_at AMI_3:def 14 :
:: deftheorem Def15 defines halts_at AMI_3:def 15 :
theorem Th39: :: AMI_3:39
:: deftheorem Def16 defines IC AMI_3:def 16 :
:: deftheorem Def17 defines starts_at AMI_3:def 17 :
:: deftheorem Def18 defines halts_at AMI_3:def 18 :
theorem Th40: :: AMI_3:40
theorem Th41: :: AMI_3:41
theorem Th42: :: AMI_3:42
theorem Th43: :: AMI_3:43
theorem Th44: :: AMI_3:44
theorem Th45: :: AMI_3:45
theorem Th46: :: AMI_3:46
theorem Th47: :: AMI_3:47
theorem Th48: :: AMI_3:48
theorem Th49: :: AMI_3:49
theorem Th50: :: AMI_3:50
Lemma49:
for b1 being State of SCM
for b2 being Instruction of SCM
for b3 being Instruction-Location of SCM holds (Exec b2,b1) . b3 = b1 . b3
theorem Th51: :: AMI_3:51
:: deftheorem Def19 defines dl. AMI_3:def 19 :
:: deftheorem Def20 defines il. AMI_3:def 20 :
theorem Th52: :: AMI_3:52
theorem Th53: :: AMI_3:53
theorem Th54: :: AMI_3:54
theorem Th55: :: AMI_3:55
theorem Th56: :: AMI_3:56
theorem Th57: :: AMI_3:57
theorem Th58: :: AMI_3:58
theorem Th59: :: AMI_3:59
theorem Th60: :: AMI_3:60
theorem Th61: :: AMI_3:61
theorem Th62: :: AMI_3:62
theorem Th63: :: AMI_3:63
theorem Th64: :: AMI_3:64
theorem Th65: :: AMI_3:65
theorem Th66: :: AMI_3:66
theorem Th67: :: AMI_3:67
theorem Th68: :: AMI_3:68
theorem Th69: :: AMI_3:69
for
b1 being
set holds
(
b1 is
Instruction of
SCM iff (
b1 = [0,{} ] or ex
b2,
b3 being
Data-Location st
b1 = b2 := b3 or ex
b2,
b3 being
Data-Location st
b1 = AddTo b2,
b3 or ex
b2,
b3 being
Data-Location st
b1 = SubFrom b2,
b3 or ex
b2,
b3 being
Data-Location st
b1 = MultBy b2,
b3 or ex
b2,
b3 being
Data-Location st
b1 = Divide b2,
b3 or ex
b2 being
Instruction-Location of
SCM st
b1 = goto b2 or ex
b2 being
Data-Location ex
b3 being
Instruction-Location of
SCM st
b1 = b2 =0_goto b3 or ex
b2 being
Data-Location ex
b3 being
Instruction-Location of
SCM st
b1 = b2 >0_goto b3 ) )
by Lemma25;
theorem Th70: :: AMI_3:70
theorem Th71: :: AMI_3:71