Copyright (c) 2001 Association of Mizar Users
environ
vocabulary AMI_3, AMI_1, BOOLE, CAT_1, FUNCT_1, RELAT_1, FUNCT_4, GOBOARD5,
FRECHET, AMISTD_1, REALSET1, FUNCOP_1, AMISTD_2, CARD_5, NET_1, AMI_5,
AMI_2, INT_1, FINSEQ_1, ARYTM_1, SQUARE_1, ARYTM_3, NAT_1, AMI_7;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, REALSET1,
NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, FINSEQ_1, FUNCOP_1, CQC_LANG,
INT_1, NAT_1, FUNCT_4, STRUCT_0, AMI_1, AMI_2, AMI_3, AMI_5, FUNCT_7,
AMISTD_1, AMISTD_2;
constructors DOMAIN_1, FUNCT_7, NAT_1, AMI_5, SQUARE_1, AMISTD_2, REALSET1,
PRE_CIRC;
clusters AMI_1, XREAL_0, INT_1, AMISTD_1, SCMRING1, AMI_6, AMISTD_2, RELSET_1,
FUNCOP_1, WAYBEL12, SCMRING3, SQUARE_1, XBOOLE_0, FRAENKEL;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI, AMI_1, AMISTD_1, AMISTD_2, XBOOLE_0;
theorems AMI_1, AMI_2, AMI_3, AMI_5, BVFUNC14, ENUMSET1, FUNCT_7, NAT_1,
REAL_1, TARSKI, SCMFSA9A, YELLOW14, AMISTD_1, FUNCT_2, SUBSET_1, AMI_6,
INT_1, SQUARE_1, FUNCOP_1, FUNCT_4, CQC_LANG, ZFMISC_1, PRE_FF, YELLOW_8,
CARD_3, FUNCT_1, YELLOW15, XBOOLE_0, XBOOLE_1, XCMPLX_1;
schemes SUBSET_1;
begin :: Preliminaries
reserve N for with_non-empty_elements set;
theorem Th1:
for x, y, z being set st x <> y & x <> z holds {x, y, z} \ {x} = {y, z}
proof
let x, y, z be set such that
A1: x <> y & x <> z;
hereby
let a be set;
assume a in {x, y, z} \ {x};
then a in {x, y, z} & not a in {x} by XBOOLE_0:def 4;
then (a = x or a = y or a = z) & a <> x by ENUMSET1:13,TARSKI:def 1;
hence a in {y, z} by TARSKI:def 2;
end;
let a be set;
assume a in {y, z};
then a = y or a = z by TARSKI:def 2;
then a in {x, y, z} & not a in {x} by A1,ENUMSET1:14,TARSKI:def 1;
hence a in {x, y, z} \ {x} by XBOOLE_0:def 4;
end;
theorem Th2:
for A being non empty non void AMI-Struct over N,
s being State of A,
o being Object of A holds
s.o in ObjectKind o
proof
let A be non empty non void AMI-Struct over N,
s be State of A,
o be Object of A;
A1: ObjectKind o = (the Object-Kind of A).o by AMI_1:def 6;
dom the Object-Kind of A = the carrier of A by FUNCT_2:def 1;
hence s.o in ObjectKind o by A1,CARD_3:18;
end;
theorem
for A being realistic IC-Ins-separated definite
(non empty non void AMI-Struct over N),
s being State of A,
f being Instruction-Location of A,
w being Element of ObjectKind IC A
holds (s+*(IC A,w)).f = s.f
proof
let A be realistic IC-Ins-separated definite
(non empty non void AMI-Struct over N),
s be State of A,
f be Instruction-Location of A,
w be Element of ObjectKind IC A;
f <> IC A by AMI_1:48;
hence (s+*(IC A,w)).f = s.f by FUNCT_7:34;
end;
definition
let N be with_non-empty_elements set,
A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
s be State of A,
o be Object of A,
a be Element of ObjectKind o;
redefine func s+*(o,a) -> State of A;
coherence
proof
dom s = the carrier of A by AMI_3:36;
then s+*(o,a) = s+*(o .--> a) by FUNCT_7:def 3;
hence thesis;
end;
end;
theorem Th4:
for A being steady-programmed IC-Ins-separated definite
(non empty non void AMI-Struct over N),
s being State of A,
o being Object of A,
f being Instruction-Location of A,
I being Instruction of A,
w being Element of ObjectKind o
st f <> o
holds Exec(I,s).f = Exec(I,s+*(o,w)).f
proof
let A be steady-programmed IC-Ins-separated definite
(non empty non void AMI-Struct over N),
s be State of A,
o be Object of A,
f be Instruction-Location of A,
I being Instruction of A,
w be Element of ObjectKind o such that
A1: f <> o;
thus Exec(I,s).f = s.f by AMI_1:def 13
.= s+*(o,w).f by A1,FUNCT_7:34
.= Exec(I,s+*(o,w)).f by AMI_1:def 13;
end;
theorem Th5:
for A being IC-Ins-separated definite (non empty non void AMI-Struct over N),
s being State of A,
o being Object of A,
w being Element of ObjectKind o
st o <> IC A
holds IC s = IC (s+*(o,w))
proof
let A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
s be State of A,
o be Object of A,
w be Element of ObjectKind o such that
A1: o <> IC A;
thus IC s = s.IC A by AMI_1:def 15
.= (s+*(o,w)).IC A by A1,FUNCT_7:34
.= IC (s+*(o,w)) by AMI_1:def 15;
end;
theorem Th6:
for A being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I being Instruction of A,
s being State of A,
o being Object of A,
w being Element of ObjectKind o
st I is sequential & o <> IC A
holds IC Exec(I,s) = IC Exec(I,s+*(o,w))
proof
let A be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I be Instruction of A,
s be State of A,
o be Object of A,
w be Element of ObjectKind o such that
A1: for s being State of A holds Exec(I,s).IC A = NextLoc IC s and
A2: o <> IC A;
thus IC Exec(I,s) = Exec(I,s).IC A by AMI_1:def 15
.= NextLoc IC s by A1
.= NextLoc IC (s+*(o,w)) by A2,Th5
.= Exec(I,s+*(o,w)).IC A by A1
.= IC Exec(I,s+*(o,w)) by AMI_1:def 15;
end;
theorem Th7:
for A being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I being Instruction of A,
s being State of A,
o being Object of A,
w being Element of ObjectKind o
st I is sequential & o <> IC A
holds IC Exec(I,s+*(o,w)) = IC (Exec(I,s) +* (o,w))
proof
let A be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I be Instruction of A,
s be State of A,
o be Object of A,
w be Element of ObjectKind o such that
A1: I is sequential and
A2: o <> IC A;
thus IC Exec(I,s+*(o,w)) = IC Exec(I,s) by A1,A2,Th6
.= Exec(I,s).IC A by AMI_1:def 15
.= (Exec(I,s) +* (o,w)).IC A by A2,FUNCT_7:34
.= IC (Exec(I,s) +* (o,w)) by AMI_1:def 15;
end;
theorem Th8:
for A being standard steady-programmed
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I being Instruction of A,
s being State of A,
o being Object of A,
w being Element of ObjectKind o,
i being Instruction-Location of A
holds Exec(I,s+*(o,w)).i = (Exec(I,s) +* (o,w)).i
proof
let A be standard steady-programmed
(IC-Ins-separated definite (non empty non void AMI-Struct over N)),
I be Instruction of A,
s be State of A,
o be Object of A,
w be Element of ObjectKind o,
i be Instruction-Location of A;
A1: Exec(I,s+*(o,w)).i = (s+*(o,w)).i by AMI_1:def 13;
A2: dom s = the carrier of A by AMI_3:36;
A3: dom Exec(I,s) = the carrier of A by AMI_3:36;
per cases;
suppose
A4: i = o;
hence Exec(I,s+*(o,w)).i = w by A1,A2,FUNCT_7:33
.= (Exec(I,s) +* (o,w)).i by A3,A4,FUNCT_7:33;
suppose
A5: i <> o;
hence Exec(I,s+*(o,w)).i = s.i by A1,FUNCT_7:34
.= Exec(I,s).i by AMI_1:def 13
.= (Exec(I,s) +* (o,w)).i by A5,FUNCT_7:34;
end;
begin :: Input and Output of Instructions
definition
let N be set,
A be AMI-Struct over N;
attr A is with_non_trivial_Instructions means
:Def1:
the Instructions of A is non trivial;
end;
definition
let N be set,
A be non empty AMI-Struct over N;
attr A is with_non_trivial_ObjectKinds means
:Def2:
for o being Object of A holds ObjectKind o is non trivial;
end;
definition
let N be with_non-empty_elements set;
cluster STC N -> with_non_trivial_ObjectKinds;
coherence
proof
let o be Object of STC N;
A1: the carrier of STC N = NAT \/ {NAT} by AMISTD_1:def 11;
A2: the Object-Kind of STC N =
(NAT --> {[1,0],[0,0]}) +* ({NAT} --> NAT) by AMISTD_1:def 11;
A3: ObjectKind o = (the Object-Kind of STC N).o by AMI_1:def 6;
A4: dom ({NAT} --> NAT) = {NAT} by FUNCOP_1:19;
per cases by A1,XBOOLE_0:def 2;
suppose
A5: o in NAT;
then o <> NAT;
then not o in dom ({NAT} --> NAT) by A4,TARSKI:def 1;
then A6: ObjectKind o = (NAT --> {[1,0],[0,0]}).o by A2,A3,FUNCT_4:12
.= {[1,0],[0,0]} by A5,FUNCOP_1:13;
A7: [1,0] <> [0,0] by ZFMISC_1:33;
[1,0] in {[1,0],[0,0]} & [0,0] in {[1,0],[0,0]} by TARSKI:def 2;
hence ObjectKind o is non trivial by A6,A7,YELLOW_8:def 1;
suppose
A8: o in {NAT};
then ObjectKind o = ({NAT} --> NAT).o by A2,A3,A4,FUNCT_4:14
.= NAT by A8,FUNCOP_1:13;
hence ObjectKind o is non trivial;
end;
end;
definition
let N be with_non-empty_elements set;
cluster halting realistic steady-programmed programmable
with_explicit_jumps without_implicit_jumps
IC-good Exec-preserving
with_non_trivial_ObjectKinds with_non_trivial_Instructions
(regular standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)));
existence
proof
take STC N;
STC N is with_non_trivial_Instructions
proof
A1: the Instructions of STC N = {[0,0],[1,0]} by AMISTD_1:def 11;
A2: [1,0] <> [0,0] by ZFMISC_1:33;
[1,0] in {[1,0],[0,0]} & [0,0] in {[1,0],[0,0]} by TARSKI:def 2;
hence the Instructions of STC N is non trivial by A1,A2,YELLOW_8:def 1;
end;
hence thesis;
end;
end;
definition
let N be with_non-empty_elements set;
cluster with_non_trivial_ObjectKinds -> with_non_trivial_Instructions
(definite (non empty non void AMI-Struct over N));
coherence
proof
let A be definite (non empty non void AMI-Struct over N);
assume
A1: for o being Object of A holds ObjectKind o is non trivial;
consider l being Instruction-Location of A;
ObjectKind l = the Instructions of A by AMI_1:def 14;
hence the Instructions of A is non trivial by A1;
end;
end;
definition
let N be with_non-empty_elements set;
cluster with_non_trivial_ObjectKinds ->
with-non-trivial-Instruction-Locations
(IC-Ins-separated (non empty AMI-Struct over N));
coherence
proof
let A be IC-Ins-separated (non empty AMI-Struct over N);
assume
A1: for o being Object of A holds ObjectKind o is non trivial;
ObjectKind IC A = the Instruction-Locations of A by AMI_1:def 11;
hence the Instruction-Locations of A is non trivial by A1;
end;
end;
definition
let N be with_non-empty_elements set,
A be with_non_trivial_ObjectKinds (non empty AMI-Struct over N),
o be Object of A;
cluster ObjectKind o -> non trivial;
coherence by Def2;
end;
definition
let N be with_non-empty_elements set,
A be with_non_trivial_Instructions AMI-Struct over N;
cluster the Instructions of A -> non trivial;
coherence by Def1;
end;
definition
let N be with_non-empty_elements set,
A be with-non-trivial-Instruction-Locations
IC-Ins-separated (non empty AMI-Struct over N);
cluster ObjectKind IC A -> non trivial;
coherence by AMI_1:def 11;
end;
definition
let N be with_non-empty_elements set,
A be non empty non void AMI-Struct over N,
I be Instruction of A;
func Output I -> Subset of A means
:Def3:
for o being Object of A holds o in it iff
ex s being State of A st s.o <> Exec(I,s).o;
existence
proof
defpred P[set] means ex s being State of A st s.$1 <> Exec(I,s).$1;
consider X being Subset of A such that
A1: for x being set holds x in X iff x in the carrier of A & P[x]
from Subset_Ex;
take X;
thus thesis by A1;
end;
uniqueness proof
defpred P[set] means ex s being State of A st s.$1 <> Exec(I,s).$1;
thus for a, b being Subset of A st
(for o being Object of A holds o in a iff P[o]) &
(for o being Object of A holds o in b iff P[o]) holds a = b
from Subset_Eq;
end;
end;
definition
let N be with_non-empty_elements set,
A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of A;
func Out_\_Inp I -> Subset of A means
:Def4:
for o being Object of A holds o in it iff
for s being State of A, a being Element of ObjectKind o
holds Exec(I,s) = Exec(I,s+*(o,a));
existence
proof
defpred P[set] means
ex l being Object of A st l = $1 &
for s being State of A, a being Element of ObjectKind l
holds Exec(I,s) = Exec(I,s+*(l,a));
consider X being Subset of A such that
A1: for x being set holds x in X iff x in the carrier of A & P[x]
from Subset_Ex;
take X;
let l be Object of A;
hereby
assume l in X;
then P[l] by A1;
hence for s being State of A, a being Element of ObjectKind l
holds Exec(I,s) = Exec(I,s+*(l,a));
end;
thus thesis by A1;
end;
uniqueness proof
defpred P[Object of A] means
for s being State of A, a being Element of ObjectKind $1
holds Exec(I,s) = Exec(I,s+*($1,a));
thus for a, b being Subset of A st
(for o being Object of A holds o in a iff P[o]) &
(for o being Object of A holds o in b iff P[o]) holds a = b
from Subset_Eq;
end;
func Out_U_Inp I -> Subset of A means
:Def5:
for o being Object of A holds o in it iff
ex s being State of A, a being Element of ObjectKind o
st Exec(I,s+*(o,a)) <> Exec(I,s) +* (o,a);
existence
proof
defpred P[set] means
ex l being Object of A st l = $1 &
ex s being State of A, a being Element of ObjectKind l
st Exec(I,s+*(l,a)) <> Exec(I,s) +* (l,a);
consider X being Subset of A such that
A2: for x being set holds x in X iff x in the carrier of A & P[x]
from Subset_Ex;
take X;
let l be Object of A;
hereby
assume l in X;
then P[l] by A2;
hence ex s being State of A, a being Element of ObjectKind l
st Exec(I,s+*(l,a)) <> Exec(I,s) +* (l,a);
end;
thus thesis by A2;
end;
uniqueness proof
defpred P[Object of A] means
ex s being State of A, a being Element of ObjectKind $1
st Exec(I,s+*($1,a)) <> Exec(I,s) +* ($1,a);
thus for a, b being Subset of A st
(for o being Object of A holds o in a iff P[o]) &
(for o being Object of A holds o in b iff P[o]) holds a = b
from Subset_Eq;
end;
end;
definition
let N be with_non-empty_elements set,
A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of A;
func Input I -> Subset of A equals
:Def6:
Out_U_Inp I \ Out_\_Inp I;
coherence;
end;
theorem Th9:
for A being IC-Ins-separated definite (non empty non void AMI-Struct over N),
I being Instruction of A holds
Out_\_Inp I misses Input I
proof
let A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of A;
Out_\_Inp I misses Out_U_Inp I \ Out_\_Inp I by XBOOLE_1:85;
hence thesis by Def6;
end;
theorem Th10:
for A being with_non_trivial_ObjectKinds IC-Ins-separated definite
(non empty non void AMI-Struct over N),
I being Instruction of A holds
Out_\_Inp I c= Output I
proof
let A be with_non_trivial_ObjectKinds IC-Ins-separated definite
(non empty non void AMI-Struct over N),
I be Instruction of A;
for o being Object of A holds o in Out_\_Inp I implies o in Output I
proof
let o be Object of A;
assume
A1: not thesis;
consider s being State of A, a being Element of ObjectKind o;
consider w being set such that
A2: w in ObjectKind o & w <> a by YELLOW15:4;
reconsider w as Element of ObjectKind o by A2;
set t = s +* (o,w);
A3: dom s = the carrier of A by AMI_3:36;
A4: dom t = the carrier of A by AMI_3:36;
A5: Exec(I,t).o = t.o by A1,Def3
.= w by A3,FUNCT_7:33;
Exec(I,t+*(o,a)).o = (t+*(o,a)).o by A1,Def3
.= a by A4,FUNCT_7:33;
hence contradiction by A1,A2,A5,Def4;
end;
hence thesis by SUBSET_1:7;
end;
theorem Th11:
for A being IC-Ins-separated definite (non empty non void AMI-Struct over N),
I being Instruction of A holds
Output I c= Out_U_Inp I
proof
let A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of A;
for o being Object of A holds o in Output I implies o in Out_U_Inp I
proof
let o be Object of A;
assume
A1: not thesis;
for s being State of A holds s.o = Exec(I,s).o
proof
let s be State of A;
reconsider so = s.o as Element of ObjectKind o by Th2;
A2: Exec(I,s+*(o,so)) = Exec(I,s) +* (o,so) by A1,Def5;
dom Exec(I,s) = the carrier of A by AMI_3:36;
hence s.o = (Exec(I,s) +* (o,so)).o by FUNCT_7:33
.= Exec(I,s).o by A2,FUNCT_7:37;
end;
hence contradiction by A1,Def3;
end;
hence thesis by SUBSET_1:7;
end;
theorem Th12:
for A being IC-Ins-separated definite (non empty non void AMI-Struct over N),
I being Instruction of A holds
Input I c= Out_U_Inp I
proof
let A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of A;
Input I = Out_U_Inp I \ Out_\_Inp I by Def6;
hence thesis by XBOOLE_1:36;
end;
theorem
for A being with_non_trivial_ObjectKinds IC-Ins-separated definite
(non empty non void AMI-Struct over N),
I being Instruction of A holds
Out_\_Inp I = Output I \ Input I
proof
let A be with_non_trivial_ObjectKinds IC-Ins-separated definite
(non empty non void AMI-Struct over N),
I be Instruction of A;
for o being Object of A holds o in Out_\_Inp I iff o in Output I \ Input
I
proof
let o be Object of A;
hereby assume
A1: o in Out_\_Inp I;
A2: Out_\_Inp I c= Output I by Th10;
Out_\_Inp I misses Input I by Th9;
then not o in Input I by A1,XBOOLE_0:3;
hence o in Output I \ Input I by A1,A2,XBOOLE_0:def 4;
end;
assume
A3: o in Output I \ Input I;
then not o in Input I by XBOOLE_0:def 4;
then A4: not o in Out_U_Inp I \ Out_\_Inp I by Def6;
per cases by A4,XBOOLE_0:def 4;
suppose
A5: not o in Out_U_Inp I;
Output I c= Out_U_Inp I by Th11;
then not o in Output I by A5;
hence thesis by A3,XBOOLE_0:def 4;
suppose o in Out_\_Inp I;
hence thesis;
end;
hence thesis by SUBSET_1:8;
end;
theorem
for A being with_non_trivial_ObjectKinds IC-Ins-separated definite
(non empty non void AMI-Struct over N),
I being Instruction of A holds
Out_U_Inp I = Output I \/ Input I
proof
let A be with_non_trivial_ObjectKinds IC-Ins-separated definite
(non empty non void AMI-Struct over N),
I be Instruction of A;
for o being Object of A st o in Out_U_Inp I holds o in Output I \/ Input
I
proof
let o be Object of A such that
A1: o in Out_U_Inp I;
o in Input I or o in Output I
proof
assume
A2: not o in Input I;
A3: Input I = Out_U_Inp I \ Out_\_Inp I by Def6;
per cases by A2,A3,XBOOLE_0:def 4;
suppose not o in Out_U_Inp I;
hence thesis by A1;
suppose
A4: o in Out_\_Inp I;
Out_\_Inp I c= Output I by Th10;
hence thesis by A4;
end;
hence o in Output I \/ Input I by XBOOLE_0:def 2;
end;
hence Out_U_Inp I c= Output I \/ Input I by SUBSET_1:7;
Output I c= Out_U_Inp I & Input I c= Out_U_Inp I by Th11,Th12;
hence thesis by XBOOLE_1:8;
end;
theorem Th15:
for A being IC-Ins-separated definite (non empty non void AMI-Struct over N),
I being Instruction of A,
o being Object of A st ObjectKind o is trivial
holds not o in Out_U_Inp I
proof
let A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of A,
o be Object of A such that
A1: ObjectKind o is trivial;
assume o in Out_U_Inp I;
then consider s being State of A,
a being Element of ObjectKind o such that
A2: Exec(I,s+*(o,a)) <> Exec(I,s) +* (o,a) by Def5;
s.o is Element of ObjectKind o by Th2;
then s.o = a by A1,YELLOW_8:def 1;
then A3: Exec(I,s+*(o,a)) = Exec(I,s) by FUNCT_7:37;
A4: dom (Exec(I,s) +* (o,a)) = the carrier of A by AMI_3:36;
A5: dom Exec(I,s) = the carrier of A by AMI_3:36;
for x being set st x in the carrier of A holds
(Exec(I,s) +* (o,a)).x = Exec(I,s).x
proof
let x be set such that x in the carrier of A;
per cases;
suppose
A6: x = o;
A7: Exec(I,s).o is Element of ObjectKind o by Th2;
thus (Exec(I,s) +* (o,a)).x = a by A5,A6,FUNCT_7:33
.= Exec(I,s).x by A1,A6,A7,YELLOW_8:def 1;
suppose x <> o;
hence (Exec(I,s) +* (o,a)).x = Exec(I,s).x by FUNCT_7:34;
end;
hence contradiction by A2,A3,A4,A5,FUNCT_1:9;
end;
theorem
for A being IC-Ins-separated definite (non empty non void AMI-Struct over N)
,
I being Instruction of A,
o being Object of A st ObjectKind o is trivial
holds not o in Input I
proof
let A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of A,
o be Object of A;
assume
A1: ObjectKind o is trivial;
Input I c= Out_U_Inp I by Th12;
hence thesis by A1,Th15;
end;
theorem
for A being IC-Ins-separated definite (non empty non void AMI-Struct over N)
,
I being Instruction of A,
o being Object of A st ObjectKind o is trivial
holds not o in Output I
proof
let A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of A,
o be Object of A;
assume
A1: ObjectKind o is trivial;
Output I c= Out_U_Inp I by Th11;
hence thesis by A1,Th15;
end;
theorem Th18:
for A being IC-Ins-separated definite (non empty non void AMI-Struct over N),
I being Instruction of A holds
I is halting iff Output I is empty
proof
let A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of A;
thus I is halting implies Output I is empty
proof
assume
A1: for s being State of A holds Exec(I,s) = s;
assume not thesis;
then consider o being Object of A such that
A2: o in Output I by SUBSET_1:10;
ex s being State of A st s.o <> Exec(I,s).o by A2,Def3;
hence thesis by A1;
end;
assume
A3: Output I is empty;
let s be State of A;
A4: dom s = the carrier of A by AMI_3:36;
A5: dom Exec(I,s) = the carrier of A by AMI_3:36;
assume Exec(I,s) <> s;
then ex x being set st x in the carrier of A & Exec(I,s).x <> s.x
by A4,A5,FUNCT_1:9;
hence contradiction by A3,Def3;
end;
theorem Th19:
for A being with_non_trivial_ObjectKinds IC-Ins-separated definite
(non empty non void AMI-Struct over N),
I being Instruction of A st I is halting
holds Out_\_Inp I is empty
proof
let A be with_non_trivial_ObjectKinds IC-Ins-separated definite
(non empty non void AMI-Struct over N),
I be Instruction of A such that
A1: I is halting;
Out_\_Inp I c= Output I by Th10;
then Out_\_Inp I c= {} by A1,Th18;
hence thesis by XBOOLE_1:3;
end;
theorem Th20:
for A being IC-Ins-separated definite (non empty non void AMI-Struct over N),
I being Instruction of A st I is halting
holds Out_U_Inp I is empty
proof
let A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of A such that
A1: for s being State of A holds Exec(I,s) = s;
assume not thesis;
then consider o being Object of A such that
A2: o in Out_U_Inp I by SUBSET_1:10;
consider s being State of A,
a being Element of ObjectKind o such that
A3: Exec(I,s+*(o,a)) <> Exec(I,s) +* (o,a) by A2,Def5;
Exec(I,s+*(o,a)) = s+*(o,a) by A1
.= Exec(I,s) +* (o,a) by A1;
hence thesis by A3;
end;
theorem Th21:
for A being IC-Ins-separated definite (non empty non void AMI-Struct over N),
I being Instruction of A st I is halting
holds Input I is empty
proof
let A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of A such that
A1: I is halting;
Input I = Out_U_Inp I \ Out_\_Inp I by Def6
.= {} \ Out_\_Inp I by A1,Th20
.= {};
hence thesis;
end;
definition
let N be with_non-empty_elements set,
A be halting IC-Ins-separated definite
(non empty non void AMI-Struct over N),
I be halting Instruction of A;
cluster Input I -> empty;
coherence by Th21;
cluster Output I -> empty;
coherence by Th18;
cluster Out_U_Inp I -> empty;
coherence by Th20;
end;
definition
let N be with_non-empty_elements set,
A be halting with_non_trivial_ObjectKinds IC-Ins-separated definite
(non empty non void AMI-Struct over N),
I be halting Instruction of A;
cluster Out_\_Inp I -> empty;
coherence by Th19;
end;
theorem Th22:
for A being with_non_trivial_Instructions steady-programmed IC-Ins-separated
definite (non empty non void AMI-Struct over N),
f being Instruction-Location of A,
I being Instruction of A
holds not f in Out_\_Inp I
proof
let A be with_non_trivial_Instructions steady-programmed IC-Ins-separated
definite (non empty non void AMI-Struct over N),
f be Instruction-Location of A,
I be Instruction of A;
consider t being State of A;
consider J being set such that
A1: J in the Instructions of A & t.f <> J by YELLOW15:4;
reconsider J as Element of ObjectKind f by A1,AMI_1:def 14;
set s = t +* (f,J);
A2: dom t = the carrier of A by AMI_3:36;
A3: Exec(I,t).f = t.f by AMI_1:def 13;
Exec(I,s).f = s.f by AMI_1:def 13
.= J by A2,FUNCT_7:33;
hence thesis by A1,A3,Def4;
end;
theorem Th23:
for A being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I being Instruction of A st I is sequential
holds not IC A in Out_\_Inp I
proof
let A be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I be Instruction of A;
consider t being State of A;
assume
A1: for s being State of A holds Exec(I,s).IC A = NextLoc IC s;
set l = IC A;
reconsider w = NextLoc IC t as Element of ObjectKind l by AMI_1:def 11;
set s = t +* (l,w);
A2: Exec(I,t).l = NextLoc IC t & Exec(I,s).l = NextLoc IC s by A1;
A3: dom t = the carrier of A by AMI_3:36;
IC s = s.l by AMI_1:def 15
.= w by A3,FUNCT_7:33;
then Exec(I,t) <> Exec(I,s) by A2,AMISTD_1:35;
hence thesis by Def4;
end;
theorem Th24:
for A being IC-Ins-separated definite (non empty non void AMI-Struct over N),
I being Instruction of A st
ex s being State of A st Exec(I,s).IC A <> IC s
holds IC A in Output I
proof
let A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of A;
given s being State of A such that
A1: Exec(I,s).IC A <> IC s;
s.IC A = IC s by AMI_1:def 15;
hence IC A in Output I by A1,Def3;
end;
theorem Th25:
for A being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I being Instruction of A st I is sequential
holds IC A in Output I
proof
let A be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I be Instruction of A such that
A1: for s being State of A holds Exec(I, s).IC A = NextLoc IC s;
consider s being State of A;
Exec(I,s).IC A = NextLoc IC s by A1;
then Exec(I,s).IC A <> IC s by AMISTD_1:35;
hence IC A in Output I by Th24;
end;
theorem Th26:
for A being IC-Ins-separated definite (non empty non void AMI-Struct over N),
I being Instruction of A st
ex s being State of A st Exec(I,s).IC A <> IC s
holds IC A in Out_U_Inp I
proof
let A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of A;
assume ex s being State of A st Exec(I,s).IC A <> IC s;
then A1: IC A in Output I by Th24;
Output I c= Out_U_Inp I by Th11;
hence thesis by A1;
end;
theorem Th27:
for A being standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I being Instruction of A st I is sequential
holds IC A in Out_U_Inp I
proof
let A be standard (IC-Ins-separated definite
(non empty non void AMI-Struct over N)),
I be Instruction of A;
assume
A1: for s being State of A holds Exec(I,s).IC A = NextLoc IC s;
consider s being State of A;
Exec(I,s).IC A = NextLoc IC s by A1;
then Exec(I,s).IC A <> IC s by AMISTD_1:35;
hence thesis by Th26;
end;
theorem Th28:
for A being IC-Ins-separated definite (non empty non void AMI-Struct over N),
f being Instruction-Location of A,
I being Instruction of A
st for s being State of A, p being programmed FinPartState of A
holds Exec (I, s +* p) = Exec (I,s) +* p
holds not f in Out_U_Inp I
proof
let A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
f be Instruction-Location of A,
I be Instruction of A such that
A1: for s being State of A, p being programmed FinPartState of A
holds Exec (I, s +* p) = Exec (I,s) +* p;
assume f in Out_U_Inp I;
then consider s being State of A,
w being Element of ObjectKind f such that
A2: Exec(I,s+*(f,w)) <> Exec(I,s) +* (f,w) by Def5;
A3: dom s = the carrier of A by AMI_3:36;
A4: dom Exec(I,s) = the carrier of A by AMI_3:36;
set p = f .--> w;
dom p = {f} by CQC_LANG:5;
then dom p c= the Instruction-Locations of A by ZFMISC_1:37;
then reconsider p as programmed FinPartState of A by AMI_3:def 13;
A5: s+*(f,w) = s +* p by A3,FUNCT_7:def 3;
Exec (I, s +* p) = Exec (I,s) +* p by A1;
hence thesis by A2,A4,A5,FUNCT_7:def 3;
end;
theorem
for A being IC-Ins-separated definite (non empty non void AMI-Struct over N)
,
I being Instruction of A,
o being Object of A st I is jump-only
holds o in Output I implies o = IC A
proof
let A be IC-Ins-separated definite (non empty non void AMI-Struct over N),
I be Instruction of A,
o be Object of A;
assume
A1: for s being State of A, o being Object of A, J being Instruction of A
st InsCode I = InsCode J & o <> IC A holds Exec(J,s).o = s.o;
assume o in Output I;
then ex s being State of A st s.o <> Exec(I,s).o by Def3;
hence o = IC A by A1;
end;
begin :: SCM
reserve a, b for Data-Location,
f for Instruction-Location of SCM,
I for Instruction of SCM;
theorem Th30:
for s being State of SCM, w being Element of ObjectKind IC SCM
holds (s+*(IC SCM,w)).a = s.a
proof
let s be State of SCM,
w be Element of ObjectKind IC SCM;
a <> IC SCM by AMI_5:20;
hence (s+*(IC SCM,w)).a = s.a by FUNCT_7:34;
end;
theorem Th31:
f <> Next f
proof
consider j being Element of SCM-Instr-Loc such that
A1: j = f & Next f = Next j by AMI_3:def 11;
j + 0 <> j + 2 by REAL_1:67;
hence thesis by A1,AMI_2:def 15;
end;
definition
let s be State of SCM, dl be Data-Location, k be Integer;
redefine func s+*(dl,k) -> State of SCM;
coherence
proof
dom s = the carrier of SCM by AMI_3:36;
then s+*(dl,k) = s+*(dl .--> k) by FUNCT_7:def 3;
hence thesis;
end;
end;
consider t being State of SCM;
Lm1: dom t = the carrier of SCM by AMI_3:36;
Lm2:
for l being Data-Location, i being Integer holds
i is Element of ObjectKind l
proof
let l be Data-Location,
i be Integer;
INT = ObjectKind l by AMI_3:55;
hence thesis by INT_1:def 2;
end;
definition
cluster SCM -> with_non_trivial_ObjectKinds;
coherence
proof
let o be Object of SCM;
per cases by AMI_6:3;
suppose o = IC SCM;
hence thesis by AMI_1:def 11;
suppose o is Instruction-Location of SCM;
then A1: ObjectKind o = the Instructions of SCM by AMI_1:def 14;
consider a, b being Data-Location;
AddTo(a,b) = [2, <*a,b*>] & SubFrom(a,b) = [3, <*a,b*>]
by AMI_3:def 4,def 5;
then AddTo(a,b) <> SubFrom(a,b) by ZFMISC_1:33;
hence thesis by A1,YELLOW_8:def 1;
suppose o is Data-Location;
hence thesis by AMI_3:55;
end;
end;
theorem Th32:
Out_\_Inp (a:=a) = {}
proof
set I = a:=a;
assume not thesis;
then consider o being Object of SCM such that
A1: o in Out_\_Inp I by SUBSET_1:10;
per cases by AMI_6:3;
suppose o = IC SCM;
hence thesis by A1,Th23;
suppose o is Instruction-Location of SCM;
hence thesis by A1,Th22;
suppose o is Data-Location;
then reconsider o as Data-Location;
reconsider w = t.o + 1 as Element of ObjectKind o by Lm2;
set s = t +* (o,w);
thus thesis
proof
per cases;
suppose
A2: o = a;
then A3: Exec(I,s).o = s.a by AMI_3:8;
A4: Exec(I,t).o = t.a by A2,AMI_3:8;
A5: Exec(I,s).o = t.a + 1 by A2,A3,Lm1,FUNCT_7:33;
t.a + 0 <> t.a + 1 by XCMPLX_1:2;
hence thesis by A1,A4,A5,Def4;
suppose
A6: o <> a;
then A7: Exec(I,t).o = t.o + 0 by AMI_3:8;
Exec(I,s).o = s.o by A6,AMI_3:8
.= w by Lm1,FUNCT_7:33;
then Exec(I,t).o <> Exec(I,s).o by A7,XCMPLX_1:2;
hence thesis by A1,Def4;
end;
end;
theorem Th33:
a <> b implies Out_\_Inp (a:=b) = { a }
proof
set I = a:=b;
assume
A1: a <> b;
thus Out_\_Inp I c= {a}
proof
let o be set;
assume
A2: o in Out_\_Inp I;
then reconsider o as Object of SCM;
per cases by AMI_6:3;
suppose o = IC SCM;
hence thesis by A2,Th23;
suppose o is Instruction-Location of SCM;
hence thesis by A2,Th22;
suppose o is Data-Location;
then reconsider o as Data-Location;
thus thesis
proof
per cases;
suppose o = a;
hence thesis by TARSKI:def 1;
suppose
A3: o <> a;
then A4: Exec(I,t).o = t.o + 0 by AMI_3:8;
reconsider w = t.o + 1 as Element of ObjectKind o by Lm2;
set s = t +* (o,w);
Exec(I,s).o = s.o by A3,AMI_3:8
.= w by Lm1,FUNCT_7:33;
then Exec(I,t).o <> Exec(I,s).o by A4,XCMPLX_1:2;
hence thesis by A2,Def4;
end;
end;
let o be set;
assume o in {a};
then A5: o = a by TARSKI:def 1;
for s being State of SCM, w being Element of ObjectKind a
holds Exec(I,s) = Exec(I,s+*(a,w))
proof
let s be State of SCM,
w be Element of ObjectKind a;
a <> IC SCM by AMI_5:20;
then A6: IC Exec(I,s) = IC Exec(I,s+*(a,w)) by Th6;
A7: for d being Data-Location holds Exec(I,s).d = Exec(I,s+*(a,w)).d
proof
let d be Data-Location;
per cases;
suppose
A8: d = a;
hence Exec(I,s).d = s.b by AMI_3:8
.= (s+*(a,w)).b by A1,FUNCT_7:34
.= Exec(I,s+*(a,w)).d by A8,AMI_3:8;
suppose
A9: d <> a;
hence Exec(I,s).d = s.d by AMI_3:8
.= s+*(a,w).d by A9,FUNCT_7:34
.= Exec(I,s+*(a,w)).d by A9,AMI_3:8;
end;
for i being Instruction-Location of SCM holds
Exec(I,s).i = Exec(I,s+*(a,w)).i
proof
let i be Instruction-Location of SCM;
i <> a by AMI_5:22;
hence thesis by Th4;
end;
hence Exec(I,s) = Exec(I,s+*(a,w)) by A6,A7,AMI_5:26;
end;
hence thesis by A5,Def4;
end;
theorem Th34:
Out_\_Inp AddTo(a,b) = {}
proof
set I = AddTo(a,b);
assume not thesis;
then consider o being Object of SCM such that
A1: o in Out_\_Inp I by SUBSET_1:10;
per cases by AMI_6:3;
suppose o = IC SCM;
hence thesis by A1,Th23;
suppose o is Instruction-Location of SCM;
hence thesis by A1,Th22;
suppose o is Data-Location;
then reconsider o as Data-Location;
reconsider w = t.o + 1 as Element of ObjectKind o by Lm2;
reconsider w1 = w as Integer;
set s = t +* (o,w);
thus thesis
proof
per cases;
suppose
A2: o = a;
then A3: Exec(I,t).o = t.a + t.b + 0 by AMI_3:9;
A4: Exec(I,s).o = s.a + s.b by A2,AMI_3:9
.= w1 + s.b by A2,Lm1,FUNCT_7:33;
thus thesis
proof
per cases;
suppose
A5: a = b;
then A6: Exec(I,t).o = 2 * t.a by A3,XCMPLX_1:11;
A7: Exec(I,s).o = w1 + w1 by A2,A4,A5,Lm1,FUNCT_7:33
.= 2 * w1 by XCMPLX_1:11;
t.a + 0 <> t.a + 1 by XCMPLX_1:2;
then Exec(I,t).o <> Exec(I,s).o by A2,A6,A7,XCMPLX_1:5;
hence thesis by A1,Def4;
suppose
A8: a <> b;
A9: t.a + t.b + 1 = t.a + 1 + t.b by XCMPLX_1:1;
Exec(I,s).o = w1 + t.b by A2,A4,A8,FUNCT_7:34;
then Exec(I,t).o <> Exec(I,s).o by A2,A3,A9,XCMPLX_1:2;
hence thesis by A1,Def4;
end;
suppose
A10: o <> a;
then A11: Exec(I,t).o = t.o + 0 by AMI_3:9;
Exec(I,s).o = s.o by A10,AMI_3:9
.= w by Lm1,FUNCT_7:33;
then Exec(I,t).o <> Exec(I,s).o by A11,XCMPLX_1:2;
hence thesis by A1,Def4;
end;
end;
theorem Th35:
Out_\_Inp SubFrom(a,a) = { a }
proof
set I = SubFrom(a,a);
thus Out_\_Inp I c= {a}
proof
let o be set;
assume
A1: o in Out_\_Inp I;
then reconsider o as Object of SCM;
per cases by AMI_6:3;
suppose o = IC SCM;
hence thesis by A1,Th23;
suppose o is Instruction-Location of SCM;
hence thesis by A1,Th22;
suppose o is Data-Location;
then reconsider o as Data-Location;
thus thesis
proof
per cases;
suppose o = a;
hence thesis by TARSKI:def 1;
suppose
A2: o <> a;
then A3: Exec(I,t).o = t.o + 0 by AMI_3:10;
reconsider w = t.o + 1 as Element of ObjectKind o by Lm2;
set s = t +* (o,w);
Exec(I,s).o = s.o by A2,AMI_3:10
.= w by Lm1,FUNCT_7:33;
then Exec(I,t).o <> Exec(I,s).o by A3,XCMPLX_1:2;
hence thesis by A1,Def4;
end;
end;
let o be set;
assume o in {a};
then A4: o = a by TARSKI:def 1;
for s being State of SCM, w being Element of ObjectKind a
holds Exec(I,s) = Exec(I,s+*(a,w))
proof
let s be State of SCM,
w be Element of ObjectKind a;
a <> IC SCM by AMI_5:20;
then A5: IC Exec(I,s) = IC Exec(I,s+*(a,w)) by Th6;
A6: for d being Data-Location holds Exec(I,s).d = Exec(I,s+*(a,w)).d
proof
let d be Data-Location;
per cases;
suppose
A7: d = a;
hence Exec(I,s).d = s.d - s.d by AMI_3:10
.= 0 by XCMPLX_1:14
.= s+*(a,w).d - s+*(a,w).d by XCMPLX_1:14
.= Exec(I,s+*(a,w)).d by A7,AMI_3:10;
suppose
A8: d <> a;
hence Exec(I,s).d = s.d by AMI_3:10
.= s+*(a,w).d by A8,FUNCT_7:34
.= Exec(I,s+*(a,w)).d by A8,AMI_3:10;
end;
for i being Instruction-Location of SCM holds
Exec(I,s).i = Exec(I,s+*(a,w)).i
proof
let i be Instruction-Location of SCM;
i <> a by AMI_5:22;
hence thesis by Th4;
end;
hence Exec(I,s) = Exec(I,s+*(a,w)) by A5,A6,AMI_5:26;
end;
hence thesis by A4,Def4;
end;
theorem Th36:
a <> b implies Out_\_Inp SubFrom(a,b) = {}
proof
assume
A1: a <> b;
set I = SubFrom(a,b);
assume not thesis;
then consider o being Object of SCM such that
A2: o in Out_\_Inp I by SUBSET_1:10;
per cases by AMI_6:3;
suppose o = IC SCM;
hence thesis by A2,Th23;
suppose o is Instruction-Location of SCM;
hence thesis by A2,Th22;
suppose o is Data-Location;
then reconsider o as Data-Location;
reconsider w = t.o + 1 as Element of ObjectKind o by Lm2;
reconsider w1 = w as Integer;
set s = t +* (o,w);
thus thesis
proof
per cases;
suppose
A3: o = a;
then A4: Exec(I,t).o = t.a - t.b + 0 by AMI_3:10;
A5: Exec(I,s).o = s.a - s.b by A3,AMI_3:10
.= w1 - s.b by A3,Lm1,FUNCT_7:33;
A6: t.a - t.b + 1 = t.a + 1 - t.b by XCMPLX_1:29;
Exec(I,s).o = w1 - t.b by A1,A3,A5,FUNCT_7:34;
then Exec(I,t).o <> Exec(I,s).o by A3,A4,A6,XCMPLX_1:2;
hence thesis by A2,Def4;
suppose
A7: o <> a;
then A8: Exec(I,t).o = t.o + 0 by AMI_3:10;
Exec(I,s).o = s.o by A7,AMI_3:10
.= w by Lm1,FUNCT_7:33;
then Exec(I,t).o <> Exec(I,s).o by A8,XCMPLX_1:2;
hence thesis by A2,Def4;
end;
end;
theorem Th37:
Out_\_Inp MultBy(a,b) = {}
proof
set I = MultBy(a,b);
assume not thesis;
then consider o being Object of SCM such that
A1: o in Out_\_Inp I by SUBSET_1:10;
per cases by AMI_6:3;
suppose o = IC SCM;
hence thesis by A1,Th23;
suppose o is Instruction-Location of SCM;
hence thesis by A1,Th22;
suppose o is Data-Location;
then reconsider o as Data-Location;
thus thesis
proof
per cases;
suppose
A2: o = a;
then A3: Exec(I,t).o = t.a * t.b by AMI_3:11;
reconsider w = t.a + 1 as Element of ObjectKind o by Lm2;
reconsider w1 = w as Integer;
set s = t +* (o,w);
A4: Exec(I,s).o = s.a * s.b by A2,AMI_3:11
.= w1 * s.b by A2,Lm1,FUNCT_7:33;
thus thesis
proof
per cases;
suppose
A5: a = b;
then A6: Exec(I,t).o = (t.a)^2 by A3,SQUARE_1:def 3;
A7: Exec(I,s).o = w1 * w1 by A2,A4,A5,Lm1,FUNCT_7:33;
now
assume Exec(I,t).o = Exec(I,s).o;
then (t.a)^2 + 0 = (t.a + 1)^2 by A6,A7,SQUARE_1:def 3
.= (t.a)^2 + 2 * t.a * 1 + 1^2 by SQUARE_1:63
.= (t.a)^2 + (2 * t.a * 1 + 1^2) by XCMPLX_1:1;
then 0 = 2 * t.a + 1 by SQUARE_1:59,XCMPLX_1:2;
then 2 * t.a = 0 - 1 by XCMPLX_1:26;
then A8: t.a * 2 / 2 = -1 / 2;
A9: t.a * 1 = t.a * (2 / 2)
.= -1 / 2 by A8,XCMPLX_1:75;
-1 <= -1 / 2 & -1 / 2 - 1 < -1;
then [\ -1 / 2 /] = -1 by INT_1:def 4;
hence contradiction by A9,INT_1:47;
end;
hence thesis by A1,Def4;
suppose
A10: a <> b;
set r = t +* (b,1);
reconsider w = r.a + 1 as Element of ObjectKind o by Lm2;
reconsider w1 = w as Integer;
set s = r +* (o,w);
A11: dom r = the carrier of SCM by AMI_3:36;
A12: Exec(I,s).o = s.a * s.b by A2,AMI_3:11
.= w1 * s.b by A2,A11,FUNCT_7:33;
A13: Exec(I,r).o = r.a * r.b by A2,AMI_3:11;
now
assume Exec(I,r).o = Exec(I,s).o;
then A14: r.a * r.b = (r.a + 1) * r.b by A2,A10,A12,A13,FUNCT_7:34;
r.b = 1 by Lm1,FUNCT_7:33;
then r.a + 0 = r.a + 1 by A14;
hence contradiction by XCMPLX_1:2;
end;
hence thesis by A1,Def4;
end;
suppose
A15: o <> a;
then A16: Exec(I,t).o = t.o + 0 by AMI_3:11;
reconsider w = t.o + 1 as Element of ObjectKind o by Lm2;
set s = t +* (o,w);
Exec(I,s).o = s.o by A15,AMI_3:11
.= w by Lm1,FUNCT_7:33;
then Exec(I,t).o <> Exec(I,s).o by A16,XCMPLX_1:2;
hence thesis by A1,Def4;
end;
end;
theorem Th38:
Out_\_Inp Divide(a,a) = { a }
proof
set I = Divide(a,a);
thus Out_\_Inp I c= {a}
proof
let o be set;
assume
A1: o in Out_\_Inp I;
then reconsider o as Object of SCM;
per cases by AMI_6:3;
suppose o = IC SCM;
hence thesis by A1,Th23;
suppose o is Instruction-Location of SCM;
hence thesis by A1,Th22;
suppose o is Data-Location;
then reconsider o as Data-Location;
reconsider w = t.o + 1 as Element of ObjectKind o by Lm2;
reconsider w1 = w as Integer;
set s = t +* (o,w);
thus thesis
proof
per cases;
suppose o = a;
hence thesis by TARSKI:def 1;
suppose o <> a;
then A2: Exec(I,t).o = t.o & Exec(I,s).o = s.o by AMI_5:15;
s.o = w1 + 0 by Lm1,FUNCT_7:33;
then t.o <> s.o by XCMPLX_1:2;
hence thesis by A1,A2,Def4;
end;
end;
let o be set;
assume o in {a};
then A3: o = a by TARSKI:def 1;
for s being State of SCM, w being Element of ObjectKind a
holds Exec(I,s) = Exec(I,s+*(a,w))
proof
let s be State of SCM,
w be Element of ObjectKind a;
a <> IC SCM by AMI_5:20;
then A4: IC Exec(I,s) = IC Exec(I,s+*(a,w)) by Th6;
A5: for d being Data-Location holds Exec(I,s).d = Exec(I,s+*(a,w)).d
proof
let d be Data-Location;
per cases;
suppose
A6: d = a;
hence Exec(I,s).d = s.d mod s.d by AMI_5:15
.= 0 by INT_1:77
.= s+*(a,w).d mod s+*(a,w).d by INT_1:77
.= Exec(I,s+*(a,w)).d by A6,AMI_5:15;
suppose
A7: d <> a;
hence Exec(I,s).d = s.d by AMI_5:15
.= s+*(a,w).d by A7,FUNCT_7:34
.= Exec(I,s+*(a,w)).d by A7,AMI_5:15;
end;
for i being Instruction-Location of SCM holds
Exec(I,s).i = Exec(I,s+*(a,w)).i
proof
let i be Instruction-Location of SCM;
i <> a by AMI_5:22;
hence thesis by Th4;
end;
hence Exec(I,s) = Exec(I,s+*(a,w)) by A4,A5,AMI_5:26;
end;
hence thesis by A3,Def4;
end;
theorem Th39:
a <> b implies Out_\_Inp Divide(a,b) = {}
proof
assume
A1: a <> b;
set I = Divide(a,b);
assume not thesis;
then consider o being Object of SCM such that
A2: o in Out_\_Inp I by SUBSET_1:10;
per cases by AMI_6:3;
suppose o = IC SCM;
hence thesis by A2,Th23;
suppose o is Instruction-Location of SCM;
hence thesis by A2,Th22;
suppose o is Data-Location;
then reconsider o as Data-Location;
consider r being State of SCM;
set t = r +* (a .--> 7) +* (b .--> 4);
A3: t.a = 7 by A1,BVFUNC14:15;
A4: t.b = 4 by YELLOW14:3;
A5: 8 = 4 * 2 + 0;
A6: 7 = 4 * 1 + 3;
A7: 7 = 1 * 5 + 2;
A8: dom t = the carrier of SCM by AMI_3:36;
reconsider w = t.o + 1 as Element of ObjectKind o by Lm2;
reconsider w1 = w as Integer;
set s = t +* (o,w);
thus thesis
proof
per cases;
suppose
A9: o = a;
then A10: s.a = w by A8,FUNCT_7:33;
s.b = t.b by A1,A9,FUNCT_7:34;
then A11: Exec(I,s).o = (7 + 1) div t.b by A1,A3,A9,A10,AMI_3:12
.= 8 div 4 by A4,SCMFSA9A:5
.= 2 by A5,NAT_1:def 1;
Exec(I,t).o = 7 div t.b by A1,A3,A9,AMI_3:12
.= 7 div 4 by A4,SCMFSA9A:5
.= 1 by A6,NAT_1:def 1;
then Exec(I,s).o <> Exec(I,t).o by A11;
hence thesis by A2,Def4;
suppose that
A12: o <> a and
A13: o = b;
A14: s.a = t.a by A12,FUNCT_7:34;
s.b = w by A8,A13,FUNCT_7:33;
then A15: Exec(I,s).o = 7 mod (t.b + 1) by A3,A13,A14,AMI_3:12
.= 7 mod 5 by A4,SCMFSA9A:5
.= 2 by A7,NAT_1:def 2;
Exec(I,t).o = 7 mod t.b by A3,A13,AMI_3:12
.= 7 mod 4 by A4,SCMFSA9A:5
.= 3 by A6,NAT_1:def 2;
then Exec(I,s).o <> Exec(I,t).o by A15;
hence thesis by A2,Def4;
suppose o <> a & o <> b;
then A16: Exec(I,s).o = s.o & Exec(I,t).o = t.o by AMI_3:12;
s.o = w1 + 0 by A8,FUNCT_7:33;
then t.o <> s.o by XCMPLX_1:2;
hence thesis by A2,A16,Def4;
end;
end;
theorem Th40:
Out_\_Inp goto f = { IC SCM }
proof
set I = goto f;
thus Out_\_Inp I c= {IC SCM}
proof
let o be set;
assume
A1: o in Out_\_Inp I;
then reconsider o as Object of SCM;
per cases by AMI_6:3;
suppose o = IC SCM;
hence thesis by TARSKI:def 1;
suppose o is Instruction-Location of SCM;
hence thesis by A1,Th22;
suppose o is Data-Location;
then reconsider o as Data-Location;
reconsider w = t.o + 1 as Element of ObjectKind o by Lm2;
set s = t +* (o,w);
A2: Exec(I,t).o = t.o + 0 by AMI_3:13;
Exec(I,s).o = s.o by AMI_3:13
.= w by Lm1,FUNCT_7:33;
then Exec(I,t).o <> Exec(I,s).o by A2,XCMPLX_1:2;
hence thesis by A1,Def4;
end;
let o be set;
assume o in {IC SCM};
then A3: o = IC SCM by TARSKI:def 1;
for s being State of SCM, w being Element of ObjectKind IC SCM
holds Exec(I,s) = Exec(I,s+*(IC SCM,w))
proof
let s be State of SCM,
w be Element of ObjectKind IC SCM;
A4: IC Exec(I,s) = Exec(I,s).IC SCM by AMI_1:def 15
.= f by AMI_3:13
.= Exec(I,s+*(IC SCM,w)).IC SCM by AMI_3:13
.= IC Exec(I,s+*(IC SCM,w)) by AMI_1:def 15;
A5: for d being Data-Location holds Exec(I,s).d = Exec(I,s+*(IC SCM,w)).d
proof
let d be Data-Location;
thus Exec(I,s).d = s.d by AMI_3:13
.= (s+*(IC SCM,w)).d by Th30
.= Exec(I,s+*(IC SCM,w)).d by AMI_3:13;
end;
for i being Instruction-Location of SCM holds
Exec(I,s).i = Exec(I,s+*(IC SCM,w)).i
proof
let i be Instruction-Location of SCM;
i <> IC SCM by AMI_1:48;
hence thesis by Th4;
end;
hence Exec(I,s) = Exec(I,s+*(IC SCM,w)) by A4,A5,AMI_5:26;
end;
hence thesis by A3,Def4;
end;
consider q being State of SCM;
Lm3: dom q = the carrier of SCM by AMI_3:36;
theorem Th41:
Out_\_Inp (a =0_goto f) = {}
proof
set I = a =0_goto f;
set s = q +* (a,1);
A1: s.a = 1 by Lm3,FUNCT_7:33;
assume not thesis;
then consider o being Object of SCM such that
A2: o in Out_\_Inp I by SUBSET_1:10;
per cases by AMI_6:3;
suppose
A3: o = IC SCM;
reconsider w = Next IC s as Element of ObjectKind IC SCM by AMI_1:def 11;
set r = s +* (IC SCM,w);
A4: Exec(I,s).IC SCM = Next IC s by A1,AMI_3:14;
A5: IC Exec(I,r) = Exec(I,r).IC SCM by AMI_1:def 15;
A6: s+*(IC SCM,w).a = s.a by Th30;
A7: dom s = the carrier of SCM by AMI_3:36;
A8: IC (s+*(IC SCM,w)) = (s+*(IC SCM,w)).IC SCM by AMI_1:def 15
.= w by A7,FUNCT_7:33;
IC Exec(I,r) = Exec(I,r).IC SCM by AMI_1:def 15
.= Next Next IC s by A1,A6,A8,AMI_3:14;
then Exec(I,s).o <> Exec(I,r).o by A3,A4,A5,Th31;
hence thesis by A2,A3,Def4;
suppose o is Instruction-Location of SCM;
hence thesis by A2,Th22;
suppose o is Data-Location;
then reconsider o as Data-Location;
reconsider w = t.o + 1 as Element of ObjectKind o by Lm2;
set s = t +* (o,w);
A9: Exec(I,t).o = t.o + 0 by AMI_3:14;
Exec(I,s).o = s.o by AMI_3:14
.= w by Lm1,FUNCT_7:33;
then Exec(I,t).o <> Exec(I,s).o by A9,XCMPLX_1:2;
hence thesis by A2,Def4;
end;
theorem Th42:
Out_\_Inp (a >0_goto f) = {}
proof
set I = a >0_goto f;
set s = q +* (a,0);
A1: s.a = 0 by Lm3,FUNCT_7:33;
assume not thesis;
then consider o being Object of SCM such that
A2: o in Out_\_Inp I by SUBSET_1:10;
per cases by AMI_6:3;
suppose
A3: o = IC SCM;
reconsider w = Next IC s as Element of ObjectKind IC SCM by AMI_1:def 11;
set r = s +* (IC SCM,w);
A4: Exec(I,s).IC SCM = Next IC s by A1,AMI_3:15;
A5: IC Exec(I,r) = Exec(I,r).IC SCM by AMI_1:def 15;
A6: s+*(IC SCM,w).a = s.a by Th30;
A7: dom s = the carrier of SCM by AMI_3:36;
A8: IC (s+*(IC SCM,w)) = (s+*(IC SCM,w)).IC SCM by AMI_1:def 15
.= w by A7,FUNCT_7:33;
IC Exec(I,r) = Exec(I,r).IC SCM by AMI_1:def 15
.= Next Next IC s by A1,A6,A8,AMI_3:15;
then Exec(I,s).o <> Exec(I,r).o by A3,A4,A5,Th31;
hence thesis by A2,A3,Def4;
suppose o is Instruction-Location of SCM;
hence thesis by A2,Th22;
suppose o is Data-Location;
then reconsider o as Data-Location;
reconsider w = t.o + 1 as Element of ObjectKind o by Lm2;
set s = t +* (o,w);
A9: Exec(I,t).o = t.o + 0 by AMI_3:15;
Exec(I,s).o = s.o by AMI_3:15
.= w by Lm1,FUNCT_7:33;
then Exec(I,t).o <> Exec(I,s).o by A9,XCMPLX_1:2;
hence thesis by A2,Def4;
end;
theorem
Output (a:=a) = { IC SCM }
proof
set I = a:=a;
hereby
let x be set;
assume
A1: x in Output I;
per cases by A1,AMI_6:3;
suppose
A2: x is Data-Location;
A3: ex s being State of SCM st s.x <> Exec(I,s).x by A1,Def3;
a <> x or a = x;
hence x in {IC SCM} by A2,A3,AMI_3:8;
suppose
A4: x is Instruction-Location of SCM;
ex s being State of SCM st s.x <> Exec(I,s).x by A1,Def3;
hence x in {IC SCM} by A4,AMI_1:def 13;
suppose x = IC SCM;
hence x in {IC SCM} by TARSKI:def 1;
end;
let x be set;
assume x in {IC SCM};
then x = IC SCM by TARSKI:def 1;
hence thesis by Th25;
end;
theorem Th44:
a <> b implies Output (a:=b) = { a, IC SCM }
proof
set I = a:=b;
assume
A1: a <> b;
hereby
let x be set;
assume
A2: x in Output I;
then A3: ex s being State of SCM st s.x <> Exec(I,s).x by Def3;
per cases by A2,AMI_6:3;
suppose x is Data-Location;
then x = a by A3,AMI_3:8;
hence x in {a,IC SCM} by TARSKI:def 2;
suppose x is Instruction-Location of SCM;
hence x in {a,IC SCM} by A3,AMI_1:def 13;
suppose x = IC SCM;
hence x in {a,IC SCM} by TARSKI:def 2;
end;
let x be set;
assume
A4: x in {a,IC SCM};
per cases by A4,TARSKI:def 2;
suppose
A5: x = a;
A6: Out_\_Inp I c= Output I by Th10;
Out_\_Inp I = {a} by A1,Th33;
then a in Out_\_Inp I by TARSKI:def 1;
hence thesis by A5,A6;
suppose x = IC SCM;
hence thesis by Th25;
end;
theorem Th45:
Output AddTo(a,b) = { a, IC SCM }
proof
set I = AddTo(a,b);
hereby
let x be set;
assume
A1: x in Output I;
then A2: ex s being State of SCM st s.x <> Exec(I,s).x by Def3;
per cases by A1,AMI_6:3;
suppose x is Data-Location;
then x = a by A2,AMI_3:9;
hence x in {a,IC SCM} by TARSKI:def 2;
suppose x is Instruction-Location of SCM;
hence x in {a,IC SCM} by A2,AMI_1:def 13;
suppose x = IC SCM;
hence x in {a,IC SCM} by TARSKI:def 2;
end;
let x be set;
assume x in {a,IC SCM};
then A3: x = a or x = IC SCM by TARSKI:def 2;
consider s being State of SCM;
set t = s +* (b .--> 1);
now
A4: t.b = 1 by YELLOW14:3;
assume t.a = Exec(I,t).a;
then t.a = t.a + t.b by AMI_3:9;
then t.b = t.a - t.a by XCMPLX_1:26;
hence contradiction by A4,XCMPLX_1:14;
end;
hence thesis by A3,Def3,Th25;
end;
theorem Th46:
Output SubFrom(a,b) = { a, IC SCM }
proof
set I = SubFrom(a,b);
hereby
let x be set;
assume
A1: x in Output I;
then A2: ex s being State of SCM st s.x <> Exec(I,s).x by Def3;
per cases by A1,AMI_6:3;
suppose x is Data-Location;
then x = a by A2,AMI_3:10;
hence x in {a,IC SCM} by TARSKI:def 2;
suppose x is Instruction-Location of SCM;
hence x in {a,IC SCM} by A2,AMI_1:def 13;
suppose x = IC SCM;
hence x in {a,IC SCM} by TARSKI:def 2;
end;
let x be set;
assume x in {a,IC SCM};
then A3: x = a or x = IC SCM by TARSKI:def 2;
consider s being State of SCM;
set t = s +* (b .--> 1);
now
A4: t.b = 1 by YELLOW14:3;
assume t.a = Exec(I,t).a;
then t.a = t.a - t.b by AMI_3:10;
then t.b = t.a - t.a by XCMPLX_1:18;
hence contradiction by A4,XCMPLX_1:14;
end;
hence thesis by A3,Def3,Th25;
end;
theorem Th47:
Output MultBy(a,b) = { a, IC SCM }
proof
set I = MultBy(a,b);
hereby
let x be set;
assume
A1: x in Output I;
then A2: ex s being State of SCM st s.x <> Exec(I,s).x by Def3;
per cases by A1,AMI_6:3;
suppose x is Data-Location;
then x = a by A2,AMI_3:11;
hence x in {a,IC SCM} by TARSKI:def 2;
suppose x is Instruction-Location of SCM;
hence x in {a,IC SCM} by A2,AMI_1:def 13;
suppose x = IC SCM;
hence x in {a,IC SCM} by TARSKI:def 2;
end;
let x be set;
assume x in {a,IC SCM};
then A3: x = a or x = IC SCM by TARSKI:def 2;
consider s being State of SCM;
set t = s +* (a .--> 1) +* (b .--> 2);
now
A4: t.b = 2 by YELLOW14:3;
a <> b or a = b;
then A5: t.a <> 0 by BVFUNC14:15,YELLOW14:3;
assume t.a = Exec(I,t).a;
then t.a = t.a * t.b by AMI_3:11;
hence contradiction by A4,A5,XCMPLX_1:7;
end;
hence thesis by A3,Def3,Th25;
end;
theorem Th48:
Output Divide(a,b) = { a, b, IC SCM }
proof
set I = Divide(a,b);
hereby
let x be set;
assume
A1: x in Output I;
then A2: ex s being State of SCM st s.x <> Exec(I,s).x by Def3;
per cases by A1,AMI_6:3;
suppose x is Data-Location;
then x = a or x = b by A2,AMI_3:12;
hence x in {a,b,IC SCM} by ENUMSET1:14;
suppose x is Instruction-Location of SCM;
hence x in {a,b,IC SCM} by A2,AMI_1:def 13;
suppose x = IC SCM;
hence x in {a,b,IC SCM} by ENUMSET1:14;
end;
let x be set;
assume x in {a,b,IC SCM};
then A3: x = a or x = b or x = IC SCM by ENUMSET1:13;
per cases;
suppose
A4: a <> b;
consider s being State of SCM;
set t = s +* (a .--> 7) +* (b .--> 2);
A5: t.b = 2 by YELLOW14:3;
then A6: t.a = 7 or t.a = 2 by BVFUNC14:15;
A7: now
assume t.a = Exec(I,t).a;
then A8: t.a = t.a div t.b by A4,AMI_3:12;
7 = 2 * 3 + 1 & 2 = 2 * 1 + 0;
then 7 div 2 = 3 & 2 div 2 = 1 by NAT_1:def 1;
hence contradiction by A5,A6,A8,SCMFSA9A:5;
end;
now
assume t.b = Exec(I,t).b;
then A9: t.b = t.a mod t.b by AMI_3:12;
7 = 2 * 3 + 1 & 2 = 2 * 1 + 0;
then 7 mod 2 = 1 & 2 mod 2 = 0 by NAT_1:def 2;
hence contradiction by A5,A6,A9,SCMFSA9A:5;
end;
hence thesis by A3,A7,Def3,Th25;
suppose
A10: a = b;
A11: Out_\_Inp I c= Output I by Th10;
Out_\_Inp I = {a} by A10,Th38;
then a in Out_\_Inp I & b in Out_\_Inp I & IC SCM in Output I
by A10,Th25,TARSKI:def 1;
hence thesis by A3,A11;
end;
theorem Th49:
Output goto f = { IC SCM }
proof
set I = goto f;
hereby
let x be set;
assume
A1: x in Output I;
then A2: ex s being State of SCM st s.x <> Exec(I,s).x by Def3;
per cases by A1,AMI_6:3;
suppose x is Data-Location;
hence x in {IC SCM} by A2,AMI_3:13;
suppose x is Instruction-Location of SCM;
hence x in {IC SCM} by A2,AMI_1:def 13;
suppose x = IC SCM;
hence x in {IC SCM} by TARSKI:def 1;
end;
let x be set;
assume x in {IC SCM};
then A3: x = IC SCM by TARSKI:def 1;
A4: Out_\_Inp I c= Output I by Th10;
Out_\_Inp I = {IC SCM} by Th40;
then IC SCM in Out_\_Inp I by TARSKI:def 1;
hence thesis by A3,A4;
end;
theorem Th50:
Output (a =0_goto f) = { IC SCM }
proof
set I = a =0_goto f;
hereby
let x be set;
assume
A1: x in Output I;
then A2: ex s being State of SCM st s.x <> Exec(I,s).x by Def3;
per cases by A1,AMI_6:3;
suppose x is Data-Location;
hence x in {IC SCM} by A2,AMI_3:14;
suppose x is Instruction-Location of SCM;
hence x in {IC SCM} by A2,AMI_1:def 13;
suppose x = IC SCM;
hence x in {IC SCM} by TARSKI:def 1;
end;
let x be set;
assume x in {IC SCM};
then A3: x = IC SCM by TARSKI:def 1;
consider s being State of SCM;
ObjectKind IC SCM = the Instruction-Locations of SCM by AMI_1:def 11;
then reconsider w = IC SCM .--> Next f as FinPartState of SCM by AMI_1:59;
set t = s +* (a .--> 0) +* w;
A4: t.IC SCM = Next f by YELLOW14:3;
a <> IC SCM by AMI_5:20;
then t.a = 0 by BVFUNC14:15;
then Exec(I,t).IC SCM = f by AMI_3:14;
then t.IC SCM <> Exec(I,t).IC SCM by A4,Th31;
hence thesis by A3,Def3;
end;
theorem Th51:
Output (a >0_goto f) = { IC SCM }
proof
set I = a >0_goto f;
hereby
let x be set;
assume
A1: x in Output I;
then A2: ex s being State of SCM st s.x <> Exec(I,s).x by Def3;
per cases by A1,AMI_6:3;
suppose x is Data-Location;
hence x in {IC SCM} by A2,AMI_3:15;
suppose x is Instruction-Location of SCM;
hence x in {IC SCM} by A2,AMI_1:def 13;
suppose x = IC SCM;
hence x in {IC SCM} by TARSKI:def 1;
end;
let x be set;
assume x in {IC SCM};
then A3: x = IC SCM by TARSKI:def 1;
consider s being State of SCM;
ObjectKind IC SCM = the Instruction-Locations of SCM by AMI_1:def 11;
then reconsider w = IC SCM .--> Next f as FinPartState of SCM by AMI_1:59;
set t = s +* (a .--> 1) +* w;
A4: t.IC SCM = Next f by YELLOW14:3;
a <> IC SCM by AMI_5:20;
then t.a = 1 by BVFUNC14:15;
then Exec(I,t).IC SCM = f by AMI_3:15;
then t.IC SCM <> Exec(I,t).IC SCM by A4,Th31;
hence thesis by A3,Def3;
end;
theorem Th52:
not f in Out_U_Inp I
proof
assume
A1: f in Out_U_Inp I;
for s being State of SCM, p being programmed FinPartState of SCM
holds Exec (I, s +* p) = Exec (I,s) +* p by AMI_5:77;
hence thesis by A1,Th28;
end;
theorem Th53:
Out_U_Inp (a:=a) = { IC SCM }
proof
set I = a:=a;
thus Out_U_Inp I c= { IC SCM }
proof
let o be set;
assume
A1: o in Out_U_Inp I;
then reconsider o as Object of SCM;
consider s being State of SCM, w being Element of ObjectKind o such that
A2: Exec(I,s+*(o,w)) <> Exec(I,s) +* (o,w) by A1,Def5;
A3: dom s = the carrier of SCM by AMI_3:36;
A4: dom Exec(I,s) = the carrier of SCM by AMI_3:36;
now
assume not o in {IC SCM};
then o <> IC SCM by TARSKI:def 1;
then A5: IC Exec(I,s+*(o,w)) = IC (Exec(I,s) +* (o,w)) by Th7;
A6: for d being Data-Location holds
Exec(I,s+*(o,w)).d = (Exec(I,s) +* (o,w)).d
proof
let d be Data-Location;
per cases;
suppose that
A7: d = a and
A8: d = o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).a by A7,AMI_3:8
.= w by A3,A7,A8,FUNCT_7:33
.= (Exec(I,s) +* (o,w)).d by A4,A8,FUNCT_7:33;
suppose that
A9: d = a and
A10: d <> o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).a by A9,AMI_3:8
.= s.a by A9,A10,FUNCT_7:34
.= Exec(I,s).d by A9,AMI_3:8
.= (Exec(I,s) +* (o,w)).d by A10,FUNCT_7:34;
suppose that
A11: d <> a and
A12: d = o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by A11,AMI_3:8
.= w by A3,A12,FUNCT_7:33
.= (Exec(I,s) +* (o,w)).d by A4,A12,FUNCT_7:33;
suppose that
A13: d <> a and
A14: d <> o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by A13,AMI_3:8
.= s.d by A14,FUNCT_7:34
.= Exec(I,s).d by A13,AMI_3:8
.= (Exec(I,s) +* (o,w)).d by A14,FUNCT_7:34;
end;
for i being Instruction-Location of SCM holds
Exec(I,s+*(o,w)).i = (Exec(I,s) +* (o,w)).i by Th8;
hence contradiction by A2,A5,A6,AMI_5:26;
end;
hence thesis;
end;
let o be set;
assume o in {IC SCM};
then o = IC SCM by TARSKI:def 1;
hence thesis by Th27;
end;
theorem Th54:
a <> b implies Out_U_Inp (a:=b) = { a, b, IC SCM }
proof
assume
A1: a <> b;
set I = a:=b;
thus Out_U_Inp I c= { a, b, IC SCM }
proof
let o be set;
assume
A2: o in Out_U_Inp I;
then reconsider o as Object of SCM;
consider s being State of SCM, w being Element of ObjectKind o such that
A3: Exec(I,s+*(o,w)) <> Exec(I,s) +* (o,w) by A2,Def5;
A4: dom s = the carrier of SCM by AMI_3:36;
A5: dom Exec(I,s) = the carrier of SCM by AMI_3:36;
now
assume that
A6: o <> a and
A7: o <> b;
assume o <> IC SCM;
then A8: IC Exec(I,s+*(o,w)) = IC (Exec(I,s) +* (o,w)) by Th7;
A9: for d being Data-Location holds
Exec(I,s+*(o,w)).d = (Exec(I,s) +* (o,w)).d
proof
let d be Data-Location;
per cases;
suppose
A10: d = a;
hence Exec(I,s+*(o,w)).d = (s+*(o,w)).b by AMI_3:8
.= s.b by A7,FUNCT_7:34
.= Exec(I,s).d by A10,AMI_3:8
.= (Exec(I,s) +* (o,w)).d by A6,A10,FUNCT_7:34;
suppose that
A11: d <> a and
A12: d = o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by A11,AMI_3:8
.= w by A4,A12,FUNCT_7:33
.= (Exec(I,s) +* (o,w)).d by A5,A12,FUNCT_7:33;
suppose that
A13: d <> a and
A14: d <> o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by A13,AMI_3:8
.= s.d by A14,FUNCT_7:34
.= Exec(I,s).d by A13,AMI_3:8
.= (Exec(I,s) +* (o,w)).d by A14,FUNCT_7:34;
end;
for i being Instruction-Location of SCM holds
Exec(I,s+*(o,w)).i = (Exec(I,s) +* (o,w)).i by Th8;
hence contradiction by A3,A8,A9,AMI_5:26;
end;
hence thesis by ENUMSET1:14;
end;
let o be set;
assume
A15: o in { a, b, IC SCM };
per cases by A15,ENUMSET1:13;
suppose
A16: o = a;
A17: Output I c= Out_U_Inp I by Th11;
Output I = {a,IC SCM} by A1,Th44;
then a in Output I by TARSKI:def 2;
hence thesis by A16,A17;
suppose
A18: o = b;
then reconsider o as Data-Location;
reconsider w = 0 as Element of ObjectKind o by Lm2;
reconsider w2 = 1 as Element of ObjectKind o by Lm2;
set q = t +* (a,0);
set s = q +* (o,w2);
A19: dom s = the carrier of SCM by AMI_3:36;
A20: dom q = the carrier of SCM by AMI_3:36;
A21: Exec(I,s+*(o,w)).a = (s+*(o,w)).b by AMI_3:8
.= 0 by A18,A19,FUNCT_7:33;
(Exec(I,s) +* (o,w)).a = Exec(I,s).a by A1,A18,FUNCT_7:34
.= s.b by AMI_3:8
.= 1 by A18,A20,FUNCT_7:33;
hence thesis by A21,Def5;
suppose o = IC SCM;
hence thesis by Th27;
end;
theorem Th55:
Out_U_Inp AddTo(a,b) = { a, b, IC SCM }
proof
set I = AddTo(a,b);
thus Out_U_Inp I c= { a, b, IC SCM }
proof
let o be set;
assume
A1: o in Out_U_Inp I;
then reconsider o as Object of SCM;
consider s being State of SCM, w being Element of ObjectKind o such that
A2: Exec(I,s+*(o,w)) <> Exec(I,s) +* (o,w) by A1,Def5;
A3: dom s = the carrier of SCM by AMI_3:36;
A4: dom Exec(I,s) = the carrier of SCM by AMI_3:36;
now
assume that
A5: o <> a and
A6: o <> b;
assume o <> IC SCM;
then A7: IC Exec(I,s+*(o,w)) = IC (Exec(I,s) +* (o,w)) by Th7;
A8: for d being Data-Location holds
Exec(I,s+*(o,w)).d = (Exec(I,s) +* (o,w)).d
proof
let d be Data-Location;
per cases;
suppose
A9: d = a;
hence Exec(I,s+*(o,w)).d = (s+*(o,w)).a + (s+*(o,w)).b by AMI_3:9
.= s.a + (s+*(o,w)).b by A5,FUNCT_7:34
.= s.a + s.b by A6,FUNCT_7:34
.= Exec(I,s).d by A9,AMI_3:9
.= (Exec(I,s) +* (o,w)).d by A5,A9,FUNCT_7:34;
suppose that
A10: d <> a and
A11: d = o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by A10,AMI_3:9
.= w by A3,A11,FUNCT_7:33
.= (Exec(I,s) +* (o,w)).d by A4,A11,FUNCT_7:33;
suppose that
A12: d <> a and
A13: d <> o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by A12,AMI_3:9
.= s.d by A13,FUNCT_7:34
.= Exec(I,s).d by A12,AMI_3:9
.= (Exec(I,s) +* (o,w)).d by A13,FUNCT_7:34;
end;
for i being Instruction-Location of SCM holds
Exec(I,s+*(o,w)).i = (Exec(I,s) +* (o,w)).i by Th8;
hence contradiction by A2,A7,A8,AMI_5:26;
end;
hence thesis by ENUMSET1:14;
end;
let o be set;
assume
A14: o in { a, b, IC SCM };
A15: now
A16: Output I c= Out_U_Inp I by Th11;
Output I = {a,IC SCM} by Th45;
then a in Output I by TARSKI:def 2;
hence a in Out_U_Inp I by A16;
end;
per cases by A14,ENUMSET1:13;
suppose o = a;
hence thesis by A15;
suppose
A17: o = b;
then reconsider o as Data-Location;
reconsider w = 0 as Element of ObjectKind o by Lm2;
reconsider w2 = 1 as Element of ObjectKind o by Lm2;
set q = t +* (a,0);
set s = q +* (o,w2);
A18: dom s = the carrier of SCM by AMI_3:36;
A19: dom q = the carrier of SCM by AMI_3:36;
now
per cases;
suppose a = b;
hence thesis by A15,A17;
suppose
A20: a <> b;
A21: Exec(I,s+*(o,w)).a = (s+*(o,w)).a + (s+*(o,w)).b by AMI_3:9
.= (s+*(o,w)).a + 0 by A17,A18,FUNCT_7:33
.= s.a + 0 by A17,A20,FUNCT_7:34;
(Exec(I,s) +* (o,w)).a = Exec(I,s).a by A17,A20,FUNCT_7:34
.= s.a + s.b by AMI_3:9
.= s.a + 1 by A17,A19,FUNCT_7:33;
then Exec(I,s+*(o,w)).a <> (Exec(I,s) +* (o,w)).a by A21,XCMPLX_1:2;
hence thesis by Def5;
end;
hence thesis;
suppose o = IC SCM;
hence thesis by Th27;
end;
theorem Th56:
Out_U_Inp SubFrom(a,b) = { a, b, IC SCM }
proof
set I = SubFrom(a,b);
thus Out_U_Inp I c= { a, b, IC SCM }
proof
let o be set;
assume
A1: o in Out_U_Inp I;
then reconsider o as Object of SCM;
consider s being State of SCM, w being Element of ObjectKind o such that
A2: Exec(I,s+*(o,w)) <> Exec(I,s) +* (o,w) by A1,Def5;
A3: dom s = the carrier of SCM by AMI_3:36;
A4: dom Exec(I,s) = the carrier of SCM by AMI_3:36;
now
assume that
A5: o <> a and
A6: o <> b;
assume o <> IC SCM;
then A7: IC Exec(I,s+*(o,w)) = IC (Exec(I,s) +* (o,w)) by Th7;
A8: for d being Data-Location holds
Exec(I,s+*(o,w)).d = (Exec(I,s) +* (o,w)).d
proof
let d be Data-Location;
per cases;
suppose
A9: d = a;
hence Exec(I,s+*(o,w)).d = (s+*(o,w)).a - (s+*(o,w)).b by AMI_3:10
.= s.a - (s+*(o,w)).b by A5,FUNCT_7:34
.= s.a - s.b by A6,FUNCT_7:34
.= Exec(I,s).d by A9,AMI_3:10
.= (Exec(I,s) +* (o,w)).d by A5,A9,FUNCT_7:34;
suppose that
A10: d <> a and
A11: d = o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by A10,AMI_3:10
.= w by A3,A11,FUNCT_7:33
.= (Exec(I,s) +* (o,w)).d by A4,A11,FUNCT_7:33;
suppose that
A12: d <> a and
A13: d <> o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by A12,AMI_3:10
.= s.d by A13,FUNCT_7:34
.= Exec(I,s).d by A12,AMI_3:10
.= (Exec(I,s) +* (o,w)).d by A13,FUNCT_7:34;
end;
for i being Instruction-Location of SCM holds
Exec(I,s+*(o,w)).i = (Exec(I,s) +* (o,w)).i by Th8;
hence contradiction by A2,A7,A8,AMI_5:26;
end;
hence thesis by ENUMSET1:14;
end;
let o be set;
assume
A14: o in { a, b, IC SCM };
A15: now
A16: Output I c= Out_U_Inp I by Th11;
Output I = {a,IC SCM} by Th46;
then a in Output I by TARSKI:def 2;
hence a in Out_U_Inp I by A16;
end;
per cases by A14,ENUMSET1:13;
suppose o = a;
hence thesis by A15;
suppose
A17: o = b;
then reconsider o as Data-Location;
reconsider w = 0 as Element of ObjectKind o by Lm2;
reconsider w2 = 1 as Element of ObjectKind o by Lm2;
set q = t +* (a,0);
set s = q +* (o,w2);
A18: dom s = the carrier of SCM by AMI_3:36;
A19: dom q = the carrier of SCM by AMI_3:36;
now
per cases;
suppose a = b;
hence thesis by A15,A17;
suppose
A20: a <> b;
A21: Exec(I,s+*(o,w)).a = (s+*(o,w)).a - (s+*(o,w)).b by AMI_3:10
.= (s+*(o,w)).a - 0 by A17,A18,FUNCT_7:33
.= s.a - 0 by A17,A20,FUNCT_7:34;
(Exec(I,s) +* (o,w)).a = Exec(I,s).a by A17,A20,FUNCT_7:34
.= s.a - s.b by AMI_3:10
.= s.a - 1 by A17,A19,FUNCT_7:33;
then Exec(I,s+*(o,w)).a <> (Exec(I,s) +* (o,w)).a by A21,XCMPLX_1:20
;
hence thesis by Def5;
end;
hence thesis;
suppose o = IC SCM;
hence thesis by Th27;
end;
theorem Th57:
Out_U_Inp MultBy(a,b) = { a, b, IC SCM }
proof
set I = MultBy(a,b);
thus Out_U_Inp I c= { a, b, IC SCM }
proof
let o be set;
assume
A1: o in Out_U_Inp I;
then reconsider o as Object of SCM;
consider s being State of SCM, w being Element of ObjectKind o such that
A2: Exec(I,s+*(o,w)) <> Exec(I,s) +* (o,w) by A1,Def5;
A3: dom s = the carrier of SCM by AMI_3:36;
A4: dom Exec(I,s) = the carrier of SCM by AMI_3:36;
now
assume that
A5: o <> a and
A6: o <> b;
assume o <> IC SCM;
then A7: IC Exec(I,s+*(o,w)) = IC (Exec(I,s) +* (o,w)) by Th7;
A8: for d being Data-Location holds
Exec(I,s+*(o,w)).d = (Exec(I,s) +* (o,w)).d
proof
let d be Data-Location;
per cases;
suppose
A9: d = a;
hence Exec(I,s+*(o,w)).d = (s+*(o,w)).a * (s+*(o,w)).b by AMI_3:11
.= s.a * (s+*(o,w)).b by A5,FUNCT_7:34
.= s.a * s.b by A6,FUNCT_7:34
.= Exec(I,s).d by A9,AMI_3:11
.= (Exec(I,s) +* (o,w)).d by A5,A9,FUNCT_7:34;
suppose that
A10: d <> a and
A11: d = o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by A10,AMI_3:11
.= w by A3,A11,FUNCT_7:33
.= (Exec(I,s) +* (o,w)).d by A4,A11,FUNCT_7:33;
suppose that
A12: d <> a and
A13: d <> o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by A12,AMI_3:11
.= s.d by A13,FUNCT_7:34
.= Exec(I,s).d by A12,AMI_3:11
.= (Exec(I,s) +* (o,w)).d by A13,FUNCT_7:34;
end;
for i being Instruction-Location of SCM holds
Exec(I,s+*(o,w)).i = (Exec(I,s) +* (o,w)).i by Th8;
hence contradiction by A2,A7,A8,AMI_5:26;
end;
hence thesis by ENUMSET1:14;
end;
let o be set;
assume
A14: o in { a, b, IC SCM };
A15: now
A16: Output I c= Out_U_Inp I by Th11;
Output I = {a,IC SCM} by Th47;
then a in Output I by TARSKI:def 2;
hence a in Out_U_Inp I by A16;
end;
per cases by A14,ENUMSET1:13;
suppose o = IC SCM;
hence thesis by Th27;
suppose o = a;
hence thesis by A15;
suppose
A17: o = b;
then reconsider o as Data-Location;
reconsider w = 0 as Element of ObjectKind o by Lm2;
reconsider w2 = 1 as Element of ObjectKind o by Lm2;
set q = t +* (a,2);
set s = q +* (o,w2);
A18: dom s = the carrier of SCM by AMI_3:36;
A19: dom q = the carrier of SCM by AMI_3:36;
now
per cases;
suppose a = b;
hence thesis by A15,A17;
suppose
A20: a <> b;
then A21: s.a = q.a by A17,FUNCT_7:34
.= 2 by Lm1,FUNCT_7:33;
A22: Exec(I,s+*(o,w)).a = (s+*(o,w)).a * (s+*(o,w)).b by AMI_3:11
.= (s+*(o,w)).a * 0 by A17,A18,FUNCT_7:33
.= s.a * 0;
(Exec(I,s) +* (o,w)).a = Exec(I,s).a by A17,A20,FUNCT_7:34
.= s.a * s.b by AMI_3:11
.= s.a * 1 by A17,A19,FUNCT_7:33;
hence thesis by A21,A22,Def5;
end;
hence thesis;
end;
theorem Th58:
Out_U_Inp Divide(a,b) = { a, b, IC SCM }
proof
set I = Divide(a,b);
per cases;
suppose
A1: a <> b;
thus Out_U_Inp I c= { a, b, IC SCM }
proof
let o be set;
assume
A2: o in Out_U_Inp I;
then reconsider o as Object of SCM;
consider s being State of SCM, w being Element of ObjectKind o such that
A3: Exec(I,s+*(o,w)) <> Exec(I,s) +* (o,w) by A2,Def5;
A4: dom s = the carrier of SCM by AMI_3:36;
A5: dom Exec(I,s) = the carrier of SCM by AMI_3:36;
now
assume that
A6: o <> a and
A7: o <> b;
assume o <> IC SCM;
then A8: IC Exec(I,s+*(o,w)) = IC (Exec(I,s) +* (o,w)) by Th7;
A9: for d being Data-Location holds
Exec(I,s+*(o,w)).d = (Exec(I,s) +* (o,w)).d
proof
let d be Data-Location;
per cases;
suppose
A10: d = a;
hence Exec(I,s+*(o,w)).d = (s+*(o,w)).a div (s+*(o,w)).b
by A1,AMI_3:12
.= s.a div (s+*(o,w)).b by A6,FUNCT_7:34
.= s.a div s.b by A7,FUNCT_7:34
.= Exec(I,s).d by A1,A10,AMI_3:12
.= (Exec(I,s) +* (o,w)).d by A6,A10,FUNCT_7:34;
suppose
A11: d = b;
hence Exec(I,s+*(o,w)).d = (s+*(o,w)).a mod (s+*(o,w)).b
by AMI_3:12
.= s.a mod (s+*(o,w)).b by A6,FUNCT_7:34
.= s.a mod s.b by A7,FUNCT_7:34
.= Exec(I,s).d by A11,AMI_3:12
.= (Exec(I,s) +* (o,w)).d by A7,A11,FUNCT_7:34;
suppose that
A12: d <> a and
A13: d <> b and
A14: d = o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by A12,A13,AMI_3:12
.= w by A4,A14,FUNCT_7:33
.= (Exec(I,s) +* (o,w)).d by A5,A14,FUNCT_7:33;
suppose that
A15: d <> a and
A16: d <> b and
A17: d <> o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by A15,A16,AMI_3:12
.= s.d by A17,FUNCT_7:34
.= Exec(I,s).d by A15,A16,AMI_3:12
.= (Exec(I,s) +* (o,w)).d by A17,FUNCT_7:34;
end;
for i being Instruction-Location of SCM holds
Exec(I,s+*(o,w)).i = (Exec(I,s) +* (o,w)).i by Th8;
hence contradiction by A3,A8,A9,AMI_5:26;
end;
hence thesis by ENUMSET1:14;
end;
let o be set;
assume
A18: o in { a, b, IC SCM };
A19: now
A20: Output I c= Out_U_Inp I by Th11;
Output I = {a,b,IC SCM} by Th48;
then a in Output I by ENUMSET1:14;
hence a in Out_U_Inp I by A20;
end;
thus thesis
proof
per cases by A18,ENUMSET1:13;
suppose o = IC SCM;
hence thesis by Th27;
suppose o = a;
hence thesis by A19;
suppose
A21: o = b;
then reconsider o as Data-Location;
reconsider w = 0 as Element of ObjectKind o by Lm2;
reconsider w2 = 1 as Element of ObjectKind o by Lm2;
set q = t +* (a,2);
set s = q +* (o,w2);
A22: dom s = the carrier of SCM by AMI_3:36;
A23: dom q = the carrier of SCM by AMI_3:36;
A24: s.a = q.a by A1,A21,FUNCT_7:34
.= 2 by Lm1,FUNCT_7:33;
A25: Exec(I,s+*(o,w)).a = (s+*(o,w)).a div (s+*(o,w)).b by A1,AMI_3:12
.= (s+*(o,w)).a div 0 by A21,A22,FUNCT_7:33
.= 0 by INT_1:75;
(Exec(I,s) +* (o,w)).a = Exec(I,s).a by A1,A21,FUNCT_7:34
.= s.a div s.b by A1,AMI_3:12
.= s.a div 1 by A21,A23,FUNCT_7:33
.= s.a by PRE_FF:2;
hence thesis by A24,A25,Def5;
end;
suppose
A26: a = b;
thus Out_U_Inp I c= { a, b, IC SCM }
proof
let o be set;
assume
A27: o in Out_U_Inp I;
then reconsider o as Object of SCM;
consider s being State of SCM, w being Element of ObjectKind o such that
A28: Exec(I,s+*(o,w)) <> Exec(I,s) +* (o,w) by A27,Def5;
A29: dom s = the carrier of SCM by AMI_3:36;
A30: dom Exec(I,s) = the carrier of SCM by AMI_3:36;
now
assume that
A31: o <> a and
A32: o <> b;
assume o <> IC SCM;
then A33: IC Exec(I,s+*(o,w)) = IC (Exec(I,s) +* (o,w)) by Th7;
A34: for d being Data-Location holds
Exec(I,s+*(o,w)).d = (Exec(I,s) +* (o,w)).d
proof
let d be Data-Location;
per cases;
suppose
A35: d = a;
hence Exec(I,s+*(o,w)).d = (s+*(o,w)).a mod (s+*(o,w)).b
by A26,AMI_5:15
.= s.a mod (s+*(o,w)).b by A31,FUNCT_7:34
.= s.a mod s.b by A32,FUNCT_7:34
.= Exec(I,s).d by A26,A35,AMI_5:15
.= (Exec(I,s) +* (o,w)).d by A31,A35,FUNCT_7:34;
suppose that
A36: d <> a and
A37: d = o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by A26,A36,AMI_5:15
.= w by A29,A37,FUNCT_7:33
.= (Exec(I,s) +* (o,w)).d by A30,A37,FUNCT_7:33;
suppose that
A38: d <> a and
A39: d <> o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by A26,A38,AMI_5:15
.= s.d by A39,FUNCT_7:34
.= Exec(I,s).d by A26,A38,AMI_5:15
.= (Exec(I,s) +* (o,w)).d by A39,FUNCT_7:34;
end;
for i being Instruction-Location of SCM holds
Exec(I,s+*(o,w)).i = (Exec(I,s) +* (o,w)).i by Th8;
hence contradiction by A28,A33,A34,AMI_5:26;
end;
hence thesis by ENUMSET1:14;
end;
let o be set;
assume
A40: o in { a, b, IC SCM };
A41: now
A42: Output I c= Out_U_Inp I by Th11;
Output I = {a,a,IC SCM} by A26,Th48
.= {a,IC SCM} by ENUMSET1:70;
then a in Output I by TARSKI:def 2;
hence a in Out_U_Inp I by A42;
end;
thus thesis
proof
per cases by A40,ENUMSET1:13;
suppose o = IC SCM;
hence thesis by Th27;
suppose o = a or o = b;
hence thesis by A26,A41;
end;
end;
theorem Th59:
Out_U_Inp (goto f) = { IC SCM }
proof
set I = goto f;
thus Out_U_Inp I c= { IC SCM }
proof
let o be set;
assume
A1: o in Out_U_Inp I;
then reconsider o as Object of SCM;
consider s being State of SCM,
w being Element of ObjectKind o such that
A2: Exec(I,s+*(o,w)) <> Exec(I,s) +* (o,w) by A1,Def5;
A3: dom s = the carrier of SCM by AMI_3:36;
A4: dom Exec(I,s) = the carrier of SCM by AMI_3:36;
per cases;
suppose o = IC SCM;
hence thesis by TARSKI:def 1;
suppose
A5: o <> IC SCM;
A6: IC Exec(I,s+*(o,w)) = Exec(I,s+*(o,w)).IC SCM by AMI_1:def 15
.= f by AMI_3:13
.= Exec(I,s).IC SCM by AMI_3:13
.= (Exec(I,s) +* (o,w)).IC SCM by A5,FUNCT_7:34
.= IC (Exec(I,s) +* (o,w)) by AMI_1:def 15;
A7: for d being Data-Location holds
Exec(I,s+*(o,w)).d = (Exec(I,s) +* (o,w)).d
proof
let d be Data-Location;
per cases;
suppose
A8: d = o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by AMI_3:13
.= w by A3,A8,FUNCT_7:33
.= (Exec(I,s) +* (o,w)).d by A4,A8,FUNCT_7:33;
suppose
A9: d <> o;
thus Exec(I,s+*(o,w)).d = (s+*(o,w)).d by AMI_3:13
.= s.d by A9,FUNCT_7:34
.= Exec(I,s).d by AMI_3:13
.= (Exec(I,s) +* (o,w)).d by A9,FUNCT_7:34;
end;
for i being Instruction-Location of SCM holds
Exec(I,s+*(o,w)).i = (Exec(I,s) +* (o,w)).i by Th8;
hence thesis by A2,A6,A7,AMI_5:26;
end;
let o be set;
assume o in { IC SCM };
then A10: o = IC SCM by TARSKI:def 1;
A11: Output I c= Out_U_Inp I by Th11;
Output I = {IC SCM} by Th49;
then IC SCM in Output I by TARSKI:def 1;
hence thesis by A10,A11;
end;
theorem Th60:
Out_U_Inp (a =0_goto f) = { a, IC SCM }
proof
set I = a =0_goto f;
thus Out_U_Inp I c= { a, IC SCM }
proof
let o be set;
assume
A1: o in Out_U_Inp I;
then reconsider o as Object of SCM;
consider s being State of SCM,
w being Element of ObjectKind o such that
A2: Exec(I,s+*(o,w)) <> Exec(I,s) +* (o,w) by A1,Def5;
per cases by AMI_6:3;
suppose o = IC SCM;
hence thesis by TARSKI:def 2;
suppose o is Instruction-Location of SCM;
hence thesis by A1,Th52;
suppose o is Data-Location & a = o;
hence thesis by TARSKI:def 2;
suppose that
A3: o is Data-Location and
A4: a <> o;
A5: o <> IC SCM by A3,AMI_5:20;
A6: dom s = the carrier of SCM by AMI_3:36;
A7: dom Exec(I,s) = the carrier of SCM by AMI_3:36;
A8: for d being Data-Location holds
Exec(I,s+*(o,w)).d = (Exec(I,s) +* (o,w)).d
proof
let d be Data-Location;
A9: Exec(I,s+*(o,w)).d = (s+*(o,w)).d by AMI_3:14;
per cases;
suppose
A10: d = o;
hence Exec(I,s+*(o,w)).d = w by A6,A9,FUNCT_7:33
.= (Exec(I,s) +* (o,w)).d by A7,A10,FUNCT_7:33;
suppose
A11: d <> o;
hence Exec(I,s+*(o,w)).d = s.d by A9,FUNCT_7:34
.= Exec(I,s).d by AMI_3:14
.= (Exec(I,s) +* (o,w)).d by A11,FUNCT_7:34;
end;
A12: for i being Instruction-Location of SCM holds
Exec(I,s+*(o,w)).i = (Exec(I,s) +* (o,w)).i by Th8;
A13: (s+*(o,w)).a = s.a by A4,FUNCT_7:34;
A14: IC Exec(I,s+*(o,w)) = Exec(I,s+*(o,w)).IC SCM by AMI_1:def 15;
A15: Exec(I,s).IC SCM = IC Exec(I,s) by AMI_1:def 15
.= IC (Exec(I,s) +* (o,w)) by A5,Th5;
now per cases;
suppose
A16: s.a = 0;
hence IC Exec(I,s+*(o,w)) = f by A13,A14,AMI_3:14
.= IC (Exec(I,s) +* (o,w)) by A15,A16,AMI_3:14;
suppose
A17: s.a <> 0;
hence IC Exec(I,s+*(o,w)) = Next IC (s+*(o,w)) by A13,A14,AMI_3:14
.= Next IC s by A5,Th5
.= IC (Exec(I,s) +* (o,w)) by A15,A17,AMI_3:14;
end;
hence thesis by A2,A8,A12,AMI_5:26;
end;
let o be set;
assume
A18: o in { a, IC SCM };
per cases by A18,TARSKI:def 2;
suppose
A19: o = a;
A20: a <> IC SCM by AMI_5:20;
reconsider nf = f as Element of ObjectKind IC SCM by AMI_1:def 11;
set q = t +* (IC SCM,nf);
set s = q +* (a,1);
A21: IC s = s.IC SCM by AMI_1:def 15
.= q.IC SCM by A20,FUNCT_7:34
.= nf by Lm1,FUNCT_7:33;
dom q = the carrier of SCM by AMI_3:36;
then A22: s.a = 1 by FUNCT_7:33;
reconsider w = 0 as Element of ObjectKind a by Lm2;
dom s = the carrier of SCM by AMI_3:36;
then (s+*(a,w)).a = w by FUNCT_7:33;
then A23: Exec(I,s+*(a,w)).IC SCM = f by AMI_3:14;
(Exec(I,s) +* (a,w)).IC SCM = IC (Exec(I,s) +* (a,w)) by AMI_1:def 15
.= IC Exec(I,s) by A20,Th5
.= Exec(I,s).IC SCM by AMI_1:def 15
.= Next f by A21,A22,AMI_3:14;
then Exec(I,s+*(a,w)) <> Exec(I,s) +* (a,w) by A23,Th31;
hence thesis by A19,Def5;
suppose
A24: o = IC SCM;
A25: Output I c= Out_U_Inp I by Th11;
Output I = {IC SCM} by Th50;
then IC SCM in Output I by TARSKI:def 1;
hence thesis by A24,A25;
end;
theorem Th61:
Out_U_Inp (a >0_goto f) = { a, IC SCM }
proof
set I = a >0_goto f;
thus Out_U_Inp I c= { a, IC SCM }
proof
let o be set;
assume
A1: o in Out_U_Inp I;
then reconsider o as Object of SCM;
consider s being State of SCM,
w being Element of ObjectKind o such that
A2: Exec(I,s+*(o,w)) <> Exec(I,s) +* (o,w) by A1,Def5;
per cases by AMI_6:3;
suppose o = IC SCM;
hence thesis by TARSKI:def 2;
suppose o is Instruction-Location of SCM;
hence thesis by A1,Th52;
suppose o is Data-Location & a = o;
hence thesis by TARSKI:def 2;
suppose that
A3: o is Data-Location and
A4: a <> o;
A5: o <> IC SCM by A3,AMI_5:20;
A6: dom s = the carrier of SCM by AMI_3:36;
A7: dom Exec(I,s) = the carrier of SCM by AMI_3:36;
A8: for d being Data-Location holds
Exec(I,s+*(o,w)).d = (Exec(I,s) +* (o,w)).d
proof
let d be Data-Location;
A9: Exec(I,s+*(o,w)).d = (s+*(o,w)).d by AMI_3:15;
per cases;
suppose
A10: d = o;
hence Exec(I,s+*(o,w)).d = w by A6,A9,FUNCT_7:33
.= (Exec(I,s) +* (o,w)).d by A7,A10,FUNCT_7:33;
suppose
A11: d <> o;
hence Exec(I,s+*(o,w)).d = s.d by A9,FUNCT_7:34
.= Exec(I,s).d by AMI_3:15
.= (Exec(I,s) +* (o,w)).d by A11,FUNCT_7:34;
end;
A12: for i being Instruction-Location of SCM holds
Exec(I,s+*(o,w)).i = (Exec(I,s) +* (o,w)).i by Th8;
A13: (s+*(o,w)).a = s.a by A4,FUNCT_7:34;
A14: IC Exec(I,s+*(o,w)) = Exec(I,s+*(o,w)).IC SCM by AMI_1:def 15;
A15: Exec(I,s).IC SCM = IC Exec(I,s) by AMI_1:def 15
.= IC (Exec(I,s) +* (o,w)) by A5,Th5;
now per cases;
suppose
A16: s.a > 0;
hence IC Exec(I,s+*(o,w)) = f by A13,A14,AMI_3:15
.= IC (Exec(I,s) +* (o,w)) by A15,A16,AMI_3:15;
suppose
A17: s.a <= 0;
hence IC Exec(I,s+*(o,w)) = Next IC (s+*(o,w)) by A13,A14,AMI_3:15
.= Next IC s by A5,Th5
.= IC (Exec(I,s) +* (o,w)) by A15,A17,AMI_3:15;
end;
hence thesis by A2,A8,A12,AMI_5:26;
end;
let o be set;
assume
A18: o in { a, IC SCM };
per cases by A18,TARSKI:def 2;
suppose
A19: o = a;
A20: a <> IC SCM by AMI_5:20;
reconsider nf = f as Element of ObjectKind IC SCM by AMI_1:def 11;
set q = t +* (IC SCM,nf);
set s = q +* (a,0);
A21: IC s = s.IC SCM by AMI_1:def 15
.= q.IC SCM by A20,FUNCT_7:34
.= nf by Lm1,FUNCT_7:33;
dom q = the carrier of SCM by AMI_3:36;
then A22: s.a = 0 by FUNCT_7:33;
reconsider w = 1 as Element of ObjectKind a by Lm2;
dom s = the carrier of SCM by AMI_3:36;
then (s+*(a,w)).a = w by FUNCT_7:33;
then A23: Exec(I,s+*(a,w)).IC SCM = f by AMI_3:15;
(Exec(I,s) +* (a,w)).IC SCM = IC (Exec(I,s) +* (a,w)) by AMI_1:def 15
.= IC Exec(I,s) by A20,Th5
.= Exec(I,s).IC SCM by AMI_1:def 15
.= Next f by A21,A22,AMI_3:15;
then Exec(I,s+*(a,w)) <> Exec(I,s) +* (a,w) by A23,Th31;
hence thesis by A19,Def5;
suppose
A24: o = IC SCM;
A25: Output I c= Out_U_Inp I by Th11;
Output I = {IC SCM} by Th51;
then IC SCM in Output I by TARSKI:def 1;
hence thesis by A24,A25;
end;
theorem
Input (a:=a) = { IC SCM }
proof
set I = a:=a;
thus Input I = Out_U_Inp I \ Out_\_Inp I by Def6
.= { IC SCM } \ Out_\_Inp I by Th53
.= { IC SCM } \ {} by Th32
.= { IC SCM };
end;
theorem
a <> b implies Input (a:=b) = { b, IC SCM }
proof
set I = a:=b;
assume
A1: a <> b;
A2: Input I = Out_U_Inp I \ Out_\_Inp I by Def6;
A3: a <> IC SCM by AMI_5:20;
Out_U_Inp I = { a, b, IC SCM } & Out_\_Inp I = { a } by A1,Th33,Th54;
hence thesis by A1,A2,A3,Th1;
end;
theorem
Input AddTo(a,b) = { a, b, IC SCM }
proof
set I = AddTo(a,b);
thus Input I = Out_U_Inp I \ Out_\_Inp I by Def6
.= { a, b, IC SCM } \ Out_\_Inp I by Th55
.= { a, b, IC SCM } \ {} by Th34
.= { a, b, IC SCM };
end;
theorem
Input SubFrom(a,a) = { IC SCM }
proof
set I = SubFrom(a,a);
A1: a <> IC SCM by AMI_5:20;
thus Input I = Out_U_Inp I \ Out_\_Inp I by Def6
.= { a, a, IC SCM } \ Out_\_Inp I by Th56
.= { a, a, IC SCM } \ {a} by Th35
.= { a, IC SCM } \ {a} by ENUMSET1:70
.= { IC SCM } by A1,ZFMISC_1:23;
end;
theorem
a <> b implies Input SubFrom(a,b) = { a, b, IC SCM }
proof
set I = SubFrom(a,b);
assume
A1: a <> b;
thus Input I = Out_U_Inp I \ Out_\_Inp I by Def6
.= { a, b, IC SCM } \ Out_\_Inp I by Th56
.= { a, b, IC SCM } \ {} by A1,Th36
.= { a, b, IC SCM };
end;
theorem
Input MultBy(a,b) = { a, b, IC SCM }
proof
set I = MultBy(a,b);
thus Input I = Out_U_Inp I \ Out_\_Inp I by Def6
.= { a, b, IC SCM } \ Out_\_Inp I by Th57
.= { a, b, IC SCM } \ {} by Th37
.= { a, b, IC SCM };
end;
theorem
Input Divide(a,a) = { IC SCM }
proof
set I = Divide(a,a);
A1: a <> IC SCM by AMI_5:20;
thus Input I = Out_U_Inp I \ Out_\_Inp I by Def6
.= { a, a, IC SCM } \ Out_\_Inp I by Th58
.= { a, a, IC SCM } \ {a} by Th38
.= { a, IC SCM } \ {a} by ENUMSET1:70
.= { IC SCM } by A1,ZFMISC_1:23;
end;
theorem
a <> b implies Input Divide(a,b) = { a, b, IC SCM }
proof
set I = Divide(a,b);
assume
A1: a <> b;
thus Input I = Out_U_Inp I \ Out_\_Inp I by Def6
.= { a, b, IC SCM } \ Out_\_Inp I by Th58
.= { a, b, IC SCM } \ {} by A1,Th39
.= { a, b, IC SCM };
end;
theorem
Input goto f = {}
proof
set I = goto f;
thus Input I = Out_U_Inp I \ Out_\_Inp I by Def6
.= {IC SCM} \ Out_\_Inp I by Th59
.= {IC SCM} \ {IC SCM} by Th40
.= {} by XBOOLE_1:37;
end;
theorem
Input (a =0_goto f) = { a, IC SCM }
proof
set I = a =0_goto f;
thus Input I = Out_U_Inp I \ Out_\_Inp I by Def6
.= {a, IC SCM} \ Out_\_Inp I by Th60
.= {a, IC SCM} \ {} by Th41
.= {a, IC SCM};
end;
theorem
Input (a >0_goto f) = { a, IC SCM }
proof
set I = a >0_goto f;
thus Input I = Out_U_Inp I \ Out_\_Inp I by Def6
.= {a, IC SCM} \ Out_\_Inp I by Th61
.= {a, IC SCM} \ {} by Th42
.= {a, IC SCM};
end;