| | Who Cites ioa all? |
|
| ioa_all | Def ioa_all(I; i.A(i)) == mk_ioa( i:I. A(i).ds, i:I. A(i).da, i:I. A(i).init, i:I. A(i).pre, i:I. A(i).eff, i:I. A(i).frame) |
| | | Thm*  I:Type, A:(I  ioa{i:l}()). ioa_all(I; i.A(i))  ioa{i:l}() |
|
| ioa_frame | Def t.frame == 2of(2of(2of(2of(2of(t))))) |
| | | Thm* t:ioa{i:l}(). t.frame Collection(frame()) |
|
| col_union | Def (i:I. C(i))(x) ==  i:I. x C(i) |
| | | Thm* T,I:Type, C:(ICollection(T)). (i:I. C(i)) Collection(T) |
|
| ioa_eff | Def t.eff == 1of(2of(2of(2of(2of(t))))) |
| | | Thm* t:ioa{i:l}(). t.eff Collection(eff()) |
|
| ioa_pre | Def t.pre == 1of(2of(2of(2of(t)))) |
| | | Thm* t:ioa{i:l}(). t.pre Collection(pre()) |
|
| ioa_init | Def t.init == 1of(2of(2of(t))) |
| | | Thm* t:ioa{i:l}(). t.init Collection(rel()) |
| | | Thm* t:ioa{i:l}(). t.init Fmla |
|
| ioa_da | Def t.da == 1of(2of(t)) |
| | | Thm* t:ioa{i:l}(). t.da Collection(dec()) |
|
| ioa_ds | Def t.ds == 1of(t) |
| | | Thm* t:ioa{i:l}(). t.ds Collection(dec()) |
|
| mk_ioa | Def mk_ioa(ds, da, init, pre, eff, frame) == < ds,da,init,pre,eff,frame > |
| | | Thm* ds,da:Collection(dec()), init:Collection(rel()), pre:Collection(pre()), eff:Collection(eff()), frame:Collection(frame()). mk_ioa(ds, da, init, pre, eff, frame) ioa{i:l}() |
|
| pi2 | Def 2of(t) == t.2 |
| | | Thm* A:Type, B:(AType), p:(a:A B(a)). 2of(p) B(1of(p)) |
|
| col_member | Def x c == c(x) |
| | | Thm* T:Type, x:T, c:Collection(T). x c Prop |
|
| pi1 | Def 1of(t) == t.1 |
| | | Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A |
