{ 
[A:Type]. [p,q:DataflowProgram(A)]. [R:df-program-statetype(p)?
df-program-statetype(q)?
].
df-prog-equiv(A;p;q;s1,s2.R[s1;s2]) 
supposing df-program-type(q) = df-program-type(p) }
{ Proof }
Definitions occuring in Statement :
df-prog-equiv: df-prog-equiv(A;p;q;s1,s2.R[s1; s2]),
df-program-statetype: df-program-statetype(dfp),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
so_apply: x[s1;s2],
unit: Unit,
member: t T,
function: x:A B[x],
union: left + right,
universe: Type,
equal: s = t
Definitions :
tactic: Error :tactic,
set: {x:A| B[x]} ,
universe: Type,
equal: s = t,
member: t T,
isect: 
x:A. B[x],
uimplies: b supposing a,
function: x:A B[x],
unit: Unit,
df-program-statetype: df-program-statetype(dfp),
union: left + right,
prop: ,
uall: [x:A]. B[x],
dataflow-program: DataflowProgram(A),
df-prog-equiv: df-prog-equiv(A;p;q;s1,s2.R[s1; s2]),
so_apply: x[s1;s2],
apply: f a,
axiom: Ax,
df-program-type: df-program-type(dfp),
product: x:A 
B[x],
all: x:A. B[x],
limited-type: LimitedType,
bool: 
,
and: P 
Q,
inl: inl x ,
df-program-state: df-program-state(dfp),
implies: P 
Q,
spread: spread def,
df-program-in-state-ap': df-program-in-state-ap'(dfp;s;m),
bag: bag(T),
pair: <a, b>,
cand: A c B,
quotient: x,y:A//B[x; y],
list: type List,
permutation: permutation(T;L1;L2),
subtype: S 
T,
fpf: a:A fp-> B[a],
subtype_rel: A r B,
uiff: uiff(P;Q),
less_than: a < b,
not: 
A,
ge: i 
j ,
le: A 
B,
strong-subtype: strong-subtype(A;B)
Lemmas :
subtype_rel_wf,
member_wf,
permutation_wf,
bag_wf,
df-program-in-state-ap'_wf,
df-program-type_wf,
df-program-statetype_wf,
dataflow-program_wf,
df-program-state_wf,
unit_wf
\mforall{}[A:Type]. \mforall{}[p,q:DataflowProgram(A)].
\mforall{}[R:df-program-statetype(p)? {}\mrightarrow{} df-program-statetype(q)? {}\mrightarrow{} \mBbbP{}].
df-prog-equiv(A;p;q;s1,s2.R[s1;s2]) \mmember{} \mBbbP{} supposing df-program-type(q) = df-program-type(p)
Date html generated:
2011_08_16-AM-09_36_31
Last ObjectModification:
2011_06_17-PM-01_18_25
Home
Index