[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
actualize
ablock-store-refsize-cons
with
groupnode
by morphism
:store → group-store;
:address-store → group-address-store;
:ablock → group-block;
:list → group-node-list;
:elem → group-node;
[] → [];
∅ → ∅;
∅ → ∅;
.list → .gndlist;
.list:= → .gndlist:=;
mkblock → groupblock;
+ → +;
# → #;
' → ';
+ → +;
+ → +;
+2 → +2;
++ → ++;
rmdup → rmdup;
rev → rev;
mklist → mklist;
fillfirst → fillfirst;
-l → -l;
-1l → -1l;
-p → -p;
pos → pos;
frome → frome;
prefixn → prefixn;
dropn → dropn;
slice → slice;
.ladrlist → .ladrlist;
.ref-size → .ref-size;
.ladrlist:= → .ladrlist:=;
.ref-size:= → .ref-size:=;
[ ] → [ ];
# → #;
-- → --;
\ → \;
| → |;
dom → dom;
⊕ → ⊕;
.map → .map;
.map → .map;
.flashsize → .flashsize;
.flashsize → .flashsize;
remove-refsize0 → remove-refsize0;
[ ] → [ ];
[ ] → [ ];
# → #;
-- → --;
\ → \;
| → |;
dom → dom;
⊕ → ⊕;
.map → .map;
.map → .map;
nodes → nodes;
< → <;
∈ → ∈;
dups → dups;
disj → disj;
⊑ → ⊑;
⊒ → ⊒;
∈ → ∈;
⊆ → ⊆;
∈ → ∈;
⊑ → ⊑;
=○refsize → =○refsize;
inv-flashsize → inv-flashsize;
inv → inv;
inv → inv;
∈ → ∈;
∈ → ∈;
⊆ → ⊆;
∈ → ∈;
refsize-cons → refsize-cons;
st → gstore;
st0 → gstore0;
st1 → gstore1;
st2 → gstore2;
dataf → gdataf;
elemdataf → gelemdataf;
ast → gast;
ast0 → gast0;
ast1 → gast1;
ast2 → gast2;
elemf → gelemf;
addresselemf → addressgf;
ablock → gblock;
ablock0 → gblock0;
ablock1 → gblock1;
ablock2 → gblock2;
a → gnd;
a0 → gnd0;
b → gnd1;
c → gnd2;
x → gndx;
x0 → gndx0;
x1 → gndx1;
y → gndx2;
z → gndx3;
.head → .head;
.tail → .tail;
.last → .last;
.butlast → .butlast;
butlastn → butlastn;
[ ] → [ ];
[ ] → [ ];
firstn → firstn;
restn → restn;
lastn → lastn;
sublist → sublist;
[ ] → [ ];
[ ] → [ ]
end actualize