:: Input and Output of Instructions
:: by Artur Korni{\l}owicz
::
:: Received May 8, 2001
:: Copyright (c) 2001 Association of Mizar Users
theorem :: AMI_7:1
canceled;
theorem Th2: :: AMI_7:2
theorem :: AMI_7:3
theorem :: AMI_7:4
theorem :: AMI_7:5
canceled;
theorem Th6: :: AMI_7:6
theorem :: AMI_7:7
theorem :: AMI_7:8
:: deftheorem Def1 defines with_non_trivial_Instructions AMI_7:def 1 :
:: deftheorem Def2 defines with_non_trivial_ObjectKinds AMI_7:def 2 :
:: deftheorem Def3 defines Output AMI_7:def 3 :
definition
let IL be non
empty set ;
let N be
with_non-empty_elements set ;
let A be non
empty stored-program IC-Ins-separated definite AMI-Struct of
IL,
N;
let I be
Instruction of
A;
func Out_\_Inp I -> Subset of
A means :
Def4:
:: AMI_7:def 4
for
o being
Object of
A holds
(
o in it iff for
s being
State of
A for
a being
Element of
ObjectKind o holds
Exec I,
s = Exec I,
(s +* o,a) );
existence
ex b1 being Subset of A st
for o being Object of A holds
( o in b1 iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) )
uniqueness
for b1, b2 being Subset of A st ( for o being Object of A holds
( o in b1 iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) ) ) & ( for o being Object of A holds
( o in b2 iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) ) ) holds
b1 = b2
func Out_U_Inp I -> Subset of
A means :
Def5:
:: AMI_7:def 5
for
o being
Object of
A holds
(
o in it iff ex
s being
State of
A ex
a being
Element of
ObjectKind o st
Exec I,
(s +* o,a) <> (Exec I,s) +* o,
a );
existence
ex b1 being Subset of A st
for o being Object of A holds
( o in b1 iff ex s being State of A ex a being Element of ObjectKind o st Exec I,(s +* o,a) <> (Exec I,s) +* o,a )
uniqueness
for b1, b2 being Subset of A st ( for o being Object of A holds
( o in b1 iff ex s being State of A ex a being Element of ObjectKind o st Exec I,(s +* o,a) <> (Exec I,s) +* o,a ) ) & ( for o being Object of A holds
( o in b2 iff ex s being State of A ex a being Element of ObjectKind o st Exec I,(s +* o,a) <> (Exec I,s) +* o,a ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines Out_\_Inp AMI_7:def 4 :
:: deftheorem Def5 defines Out_U_Inp AMI_7:def 5 :
:: deftheorem defines Input AMI_7:def 6 :
theorem :: AMI_7:9
canceled;
theorem Th10: :: AMI_7:10
theorem Th11: :: AMI_7:11
theorem :: AMI_7:12
canceled;
theorem :: AMI_7:13
theorem :: AMI_7:14
theorem Th15: :: AMI_7:15
theorem :: AMI_7:16
theorem :: AMI_7:17
theorem Th18: :: AMI_7:18
theorem Th19: :: AMI_7:19
theorem Th20: :: AMI_7:20
theorem Th21: :: AMI_7:21
theorem :: AMI_7:22
theorem :: AMI_7:23
theorem :: AMI_7:24
theorem :: AMI_7:25
theorem Th26: :: AMI_7:26
theorem :: AMI_7:27
theorem :: AMI_7:28
theorem :: AMI_7:29