(benchmark copy_act3_SIM :logic LRM :extrasorts ((USER 0)) :extrasorts ((OBJECT 0)) :extrasorts ((GROUP 0)) :extrasorts ((NAME 0)) :extrasorts ((DATA 0)) :extrasorts ((PERMISSION 0)) :extrafuns ((wbg PERMISSION)) :extrafuns ((root OBJECT)) :extrafuns ((fbuffer (Map OBJECT (Map Int DATA)))) :extrafuns ((objs (Set OBJECT))) :extrafuns ((xbw PERMISSION)) :extrafuns ((|directories'| (Set OBJECT))) :extrafuns ((XPerm ((ind Tuple 2) ((ind Tuple 2) ((ind Tuple 2) (Set ((ind Tuple 2) OBJECT PERMISSION)) (Map OBJECT USER)) (Map OBJECT GROUP)) (Set ((ind Tuple 2) USER GROUP))) (Set ((ind Tuple 2) OBJECT USER)))) :extrafuns ((rbg PERMISSION)) :extrafuns ((rbw PERMISSION)) :extrafuns ((|obj_owner| (Map OBJECT USER))) :extrafuns ((|user_grps| (Set ((ind Tuple 2) USER GROUP)))) :extrafuns ((|obj_perms'| (Set ((ind Tuple 2) OBJECT PERMISSION)))) :extrafuns ((fs (Set OBJECT))) :extrafuns ((rname NAME)) :extrafuns ((tcl (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT)))) :extrafuns ((corres (Map OBJECT OBJECT))) :extrafuns ((|obj_owner'| (Set ((ind Tuple 2) OBJECT USER)))) :extrafuns ((replica (Set ((ind Tuple 2) OBJECT OBJECT)))) :extrafuns ((xbo PERMISSION)) :extrafuns ((|files'| (Set OBJECT))) :extrafuns ((|obj_perms| (Set ((ind Tuple 2) OBJECT PERMISSION)))) :extrafuns ((|obj_grp| (Map OBJECT GROUP))) :extrafuns ((nobjs (Set OBJECT))) :extrafuns ((xbg PERMISSION)) :extrafuns ((parent (Map OBJECT OBJECT))) :extrafuns ((WPerm ((ind Tuple 2) ((ind Tuple 2) ((ind Tuple 2) (Set ((ind Tuple 2) OBJECT PERMISSION)) (Map OBJECT USER)) (Map OBJECT GROUP)) (Set ((ind Tuple 2) USER GROUP))) (Set ((ind Tuple 2) OBJECT USER)))) :extrafuns ((users (Set USER))) :extrafuns ((fcontent (Map OBJECT (Map Int DATA)))) :extrafuns ((groups (Set GROUP))) :extrafuns ((to OBJECT)) :extrafuns ((|obj_grp'| (Set ((ind Tuple 2) OBJECT GROUP)))) :extrafuns ((nobj OBJECT)) :extrafuns ((su USER)) :extrafuns ((obj OBJECT)) :extrafuns ((directories (Set OBJECT))) :extrafuns ((objects (Set OBJECT))) :extrafuns ((wbo PERMISSION)) :extrafuns ((|user_pgrp| (Map USER GROUP))) :extrafuns ((|opened_files| (Set OBJECT))) :extrafuns ((des (Set OBJECT))) :extrafuns ((admin GROUP)) :extrafuns ((subparent (Map OBJECT OBJECT))) :extrafuns ((rbo PERMISSION)) :extrafuns ((RPerm ((ind Tuple 2) ((ind Tuple 2) ((ind Tuple 2) (Set ((ind Tuple 2) OBJECT PERMISSION)) (Map OBJECT USER)) (Map OBJECT GROUP)) (Set ((ind Tuple 2) USER GROUP))) (Set ((ind Tuple 2) OBJECT USER)))) :extrafuns ((usr USER)) :extrafuns ((|fcontent'| (Set ((ind Tuple 2) OBJECT (Set ((ind Tuple 2) Int DATA)))))) :extrafuns ((|parent'| (Set ((ind Tuple 2) OBJECT OBJECT)))) :extrafuns ((ds (Set OBJECT))) :extrafuns ((files (Set OBJECT))) :extrafuns ((wbw PERMISSION)) :extrafuns ((relImage10 (Set ((ind Tuple 2) OBJECT OBJECT)) (Set OBJECT) (Set OBJECT))) :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT))) (s (Set OBJECT)) (b OBJECT)) (= (in b (relImage10 r s)) (exists ((a OBJECT)) (and (in a s) (in ((ind tuple 2) a b) r))))) :extrafuns ((relConverse12 (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT)))) :assumption (forall ((f (Set ((ind Tuple 2) OBJECT OBJECT))) (a OBJECT) (b OBJECT)) (= (in ((ind tuple 2) b a) (relConverse12 f)) (in ((ind tuple 2) a b) f))) :extrafuns ((pfun2Relation13 (Map OBJECT OBJECT) (Set ((ind Tuple 2) OBJECT OBJECT)))) :assumption (forall ((f (Map OBJECT OBJECT)) (a OBJECT) (b OBJECT)) (= (in ((ind tuple 2) a b) (pfun2Relation13 f)) (and (in a (domain f)) (= b (apply f a))))) :extrafuns ((pfunConverse11 ((x (Map OBJECT OBJECT))) (relConverse12 (pfun2Relation13 x)))) :extrafuns ((pfun2Relation28 (Map OBJECT USER) (Set ((ind Tuple 2) OBJECT USER)))) :assumption (forall ((f (Map OBJECT USER)) (a OBJECT) (b USER)) (= (in ((ind tuple 2) a b) (pfun2Relation28 f)) (and (in a (domain f)) (= b (apply f a))))) :extrafuns ((relImage29 (Set ((ind Tuple 2) USER GROUP)) (Set USER) (Set GROUP))) :assumption (forall ((r (Set ((ind Tuple 2) USER GROUP))) (s (Set USER)) (b GROUP)) (= (in b (relImage29 r s)) (exists ((a USER)) (and (in a s) (in ((ind tuple 2) a b) r))))) :extrafuns ((joinRelations39 (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT)))) :assumption (forall ((r1 (Set ((ind Tuple 2) OBJECT OBJECT))) (r2 (Set ((ind Tuple 2) OBJECT OBJECT))) (a OBJECT) (c OBJECT)) (= (in ((ind tuple 2) a c) (joinRelations39 r1 r2)) (exists ((b OBJECT)) (and (in ((ind tuple 2) a b) r1) (in ((ind tuple 2) b c) r2))))) :notes "objects∈ℙ(OBJECT)" :assumption true :notes "WPerm∈(OBJECT ↔ PERMISSION) × (OBJECT ⇸ USER) × (OBJECT ⇸ GROUP) × (USER ↔ GROUP) → (OBJECT ↔ USER)" :assumption true :notes "des⊆files∪directories" :assumption (subset des (union files directories)) :notes "to ↦ usr∈WPerm(obj_perms ↦ obj_owner ↦ obj_grp ↦ user_grps)" :assumption (in ((ind tuple 2) to usr) (WPerm ((ind tuple 2) ((ind tuple 2) ((ind tuple 2) |obj_perms| |obj_owner|) |obj_grp|) |user_grps|))) :notes "∀s·s⊆parent∼[s]⇒s=∅" :assumption (forall ((s (Set OBJECT))) (implies (subset s (relImage10 (pfunConverse11 parent) s)) (= s (as emptySet (Set OBJECT))))) :notes "opened_files⊆files" :assumption (subset |opened_files| files) :notes "user_pgrp∈users → groups" :assumption true :notes "admin∈GROUP" :assumption true :notes "obj ↦ usr∈RPerm(obj_perms ↦ obj_owner ↦ obj_grp ↦ user_grps)" :assumption (in ((ind tuple 2) obj usr) (RPerm ((ind tuple 2) ((ind tuple 2) ((ind tuple 2) |obj_perms| |obj_owner|) |obj_grp|) |user_grps|))) :notes "to∈directories" :assumption (in to directories) :notes "objects=files∪directories" :assumption (= objects (union files directories)) :notes "tcl∈objrel → objrel" :assumption true :notes "∀f,g,t,u,x,M,N·N⊆OBJECT∧M⊆OBJECT∧N∩M=∅∧t∈M∧f∈M ∖ {t} → M∧u∈N∧g∈N ∖ {u} → N∧x∈M⇒f∪g∪{u ↦ x}∈(M∪N) ∖ {t} → M∪N" :assumption (forall ((f (Map OBJECT OBJECT))(g (Map OBJECT OBJECT))(t OBJECT)(u OBJECT)(x OBJECT)(M (Set OBJECT))(N (Set OBJECT))) (implies (and true true (= (inter N M) (as emptySet (Set OBJECT))) (in t M) false (in u N) false (in x M)) true)) :notes "nobj=corres(obj)" :assumption (= nobj (apply corres obj)) :notes "nobjs⊆OBJECT ∖ (files∪directories)" :assumption (forall ((var21 OBJECT)) (implies (in var21 nobjs) (not (or (in var21 files) (in var21 directories))))) :notes "obj_owner∈files∪directories → users" :assumption true :notes "∀o,u,p,s,g,m·o∈OBJECT∧u∈USER∧p∈OBJECT ↔ PERMISSION∧s∈OBJECT ⇸ USER∧g∈OBJECT ⇸ GROUP∧m∈USER ↔ GROUP∧o∈dom(g)⇒(o ↦ u∈XPerm(p ↦ s ↦ g ↦ m)⇔(o ↦ u∈s∧o ↦ xbo∈p)∨(g(o)∈m[{u}]∧o ↦ xbg∈p)∨o ↦ xbw∈p∨u=su)" :assumption (forall ((o OBJECT)(u USER)(p (Set ((ind Tuple 2) OBJECT PERMISSION)))(s (Map OBJECT USER))(g (Map OBJECT GROUP))(m (Set ((ind Tuple 2) USER GROUP)))) (implies (and true true true true true true (in o (domain g))) (= (in ((ind tuple 2) o u) (XPerm ((ind tuple 2) ((ind tuple 2) ((ind tuple 2) p s) g) m))) (or (and (in ((ind tuple 2) o u) (pfun2Relation28 s)) (in ((ind tuple 2) o xbo) p)) (and (in (apply g o) (relImage29 m (insert u (as emptySet (Set USER))))) (in ((ind tuple 2) o xbg) p)) (in ((ind tuple 2) o xbw) p) (= u su))))) :notes "root∈objects" :assumption (in root objects) :notes "fs=corres[objs∩files]" :assumption (= fs (range (restrict corres (inter objs files)))) :notes "∀f,g,t,u,x,M,N·N⊆OBJECT∧M⊆OBJECT∧N∩M=∅∧t∈M∧f∈M ∖ {t} → M∧u∈N∧g∈N ∖ {u} → N∧x∈M∧(∀A·A⊆f∼[A]⇒A=∅)∧(∀B·B⊆g∼[B]⇒B=∅)∧f∪g∪{u ↦ x}∈(M∪N) ∖ {t} → M∪N⇒(∀C·C⊆(f∪g∪{u ↦ x})∼[C]⇒C=∅)" :assumption (forall ((f (Map OBJECT OBJECT))(g (Map OBJECT OBJECT))(t OBJECT)(u OBJECT)(x OBJECT)(M (Set OBJECT))(N (Set OBJECT))) (implies (and true true (= (inter N M) (as emptySet (Set OBJECT))) (in t M) false (in u N) false (in x M) (forall ((A (Set OBJECT))) (implies (subset A (relImage10 (pfunConverse11 f) A)) (= A (as emptySet (Set OBJECT))))) (forall ((B (Set OBJECT))) (implies (subset B (relImage10 (pfunConverse11 g) B)) (= B (as emptySet (Set OBJECT))))) false) (forall ((C (Set OBJECT))) (implies (subset C (relImage10 (relConverse12 (union (pfun2Relation13 f) (pfun2Relation13 g) (insert ((ind tuple 2) u x) (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))) C)) (= C (as emptySet (Set OBJECT))))))) :notes "∀x·((tcl(parent))∼[{x}]∪{x}) ⩤ parent∈(objects ∖ ((tcl(parent))∼[{x}]∪{x})) ∖ {root} → objects ∖ ((tcl(parent))∼[{x}]∪{x})" :assumption (forall ((x OBJECT)) true) :notes "tcl(parent)∩(OBJECT ◁ id)=∅" :assumption (forall ((var32 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var32 (tcl (pfun2Relation13 parent))) (= ((ind project 2 1) var32) ((ind project 2 2) var32))) (in var32 (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))) :notes "ds=corres[objs∩directories]" :assumption (= ds (range (restrict corres (inter objs directories)))) :notes "objfn⊆objrel" :assumption true :notes "∀f,c,g,t,u,M,N·N⊆OBJECT∧M⊆OBJECT∧t∈M∧f∈M ∖ {t} → M∧(∀s·s⊆f∼[s]⇒s=∅)∧u∈N∧c∈M ⤖ N∧u=c(t)∧g=c∼;f;c∧g∈N ∖ {u} → N⇒(∀w·w⊆g∼[w]⇒w=∅)" :assumption (forall ((f (Map OBJECT OBJECT))(c (Map OBJECT OBJECT))(g (Map OBJECT OBJECT))(t OBJECT)(u OBJECT)(M (Set OBJECT))(N (Set OBJECT))) (implies (and true true (in t M) false (forall ((s (Set OBJECT))) (implies (subset s (relImage10 (pfunConverse11 f) s)) (= s (as emptySet (Set OBJECT))))) (in u N) false (= u (apply c t)) (= (pfun2Relation13 g) (joinRelations39 (joinRelations39 (pfunConverse11 c) (pfun2Relation13 f)) (pfun2Relation13 c)) ) false) (forall ((w (Set OBJECT))) (implies (subset w (relImage10 (pfunConverse11 g) w)) (= w (as emptySet (Set OBJECT))))))) :notes "parent∈objects ∖ {root} → objects" :assumption true :notes "root∈OBJECT" :assumption true :notes "∀r·r∈objrel⇒r;tcl(r)⊆tcl(r)" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (subset (joinRelations39 r (tcl r)) (tcl r)))) :notes "tcl(∅)=∅" :assumption (= (tcl (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))) (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))) :notes "user_grps∈users ↔ groups" :assumption true :notes "users⊆USER" :assumption true :notes "rname∈NAME" :assumption true :notes "files∩directories=∅" :assumption (= (inter files directories) (as emptySet (Set OBJECT))) :notes "⊤" :assumption true :notes "∀r·r∈objrel⇒r⊆tcl(r)" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (subset r (tcl r)))) :notes "PERMISSION={rbo,wbo,xbo,rbg,wbg,xbg,rbw,wbw,xbw}" :assumption (forall ((var45 PERMISSION)) (= true (or (= var45 rbo) (= var45 wbo) (= var45 xbo) (= var45 rbg) (= var45 wbg) (= var45 xbg) (= var45 rbw) (= var45 wbw) (= var45 xbw)))) :notes "obj_perms∈OBJECT ↔ PERMISSION" :assumption true :notes "objfn=OBJECT ∖ {root} ⇸ OBJECT" :assumption true :notes "fcontent∈files → CONTENT" :assumption true :notes "∀t·t∈objfn∧(∀s·s⊆t∼[s]⇒s=∅)⇒tcl(t)∩(OBJECT ◁ id)=∅" :assumption (forall ((t (Map OBJECT OBJECT))) (implies (and (forall ((var48 OBJECT)) (implies (in var48 (domain t)) (not (= var48 root)))) (forall ((s (Set OBJECT))) (implies (subset s (relImage10 (pfunConverse11 t) s)) (= s (as emptySet (Set OBJECT)))))) (forall ((var49 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var49 (tcl (pfun2Relation13 t))) (= ((ind project 2 1) var49) ((ind project 2 2) var49))) (in var49 (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))))) :notes "∅∈CONTENT" :assumption (forall ((var50 Int) (var51 DATA) (var52 DATA)) (implies (and (in ((ind tuple 2) var50 var51) (as emptySet (Set ((ind Tuple 2) Int DATA)))) (in ((ind tuple 2) var50 var52) (as emptySet (Set ((ind Tuple 2) Int DATA))))) (and (= var51 var52) (>= var50 0)))) :notes "∀r,r2·r∈objrel∧r2∈objrel∧r2⊆r∧(∀s·s⊆r[s]⇒s=∅)⇒(∀t·t⊆r2[t]⇒t=∅)" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))(r2 (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies (and true true (subset r2 r) (forall ((s (Set OBJECT))) (implies (subset s (relImage10 r s)) (= s (as emptySet (Set OBJECT)))))) (forall ((t (Set OBJECT))) (implies (subset t (relImage10 r2 t)) (= t (as emptySet (Set OBJECT))))))) :notes "∀x·x∉ran(parent)⇒(tcl(parent))∼[{x}]=∅" :assumption (forall ((x OBJECT)) (implies (not (in x (range parent))) (= (relImage10 (relConverse12 (tcl (pfun2Relation13 parent))) (insert x (as emptySet (Set OBJECT)))) (as emptySet (Set OBJECT))))) :notes "objrel=OBJECT ↔ OBJECT" :assumption true :notes "obj_grp∈files∪directories → groups" :assumption true :notes "fbuffer∈opened_files → CONTENT" :assumption true :notes "objs=des∪{obj}" :assumption (= objs (union des (insert obj (as emptySet (Set OBJECT))))) :notes "∀x·(tcl(parent))∼[{x}] ◁ parent∈(tcl(parent))∼[{x}] → (tcl(parent))∼[{x}]∪{x}" :assumption (forall ((x OBJECT)) true) :notes "∀f,g,c,t,u,M,N·N⊆OBJECT∧M⊆OBJECT∧N∩M=∅∧t∈M∧f∈M ∖ {t} → M∧u∈N∧c∈M ⤖ N∧u=c(t)∧g=c∼;f;c⇒g∈N ∖ {u} → N" :assumption (forall ((f (Map OBJECT OBJECT))(g (Set ((ind Tuple 2) OBJECT OBJECT)))(c (Map OBJECT OBJECT))(t OBJECT)(u OBJECT)(M (Set OBJECT))(N (Set OBJECT))) (implies (and true true (= (inter N M) (as emptySet (Set OBJECT))) (in t M) false (in u N) false (= u (apply c t)) (= g (joinRelations39 (joinRelations39 (pfunConverse11 c) (pfun2Relation13 f)) (pfun2Relation13 c)) )) true)) :notes "directories⊆objects" :assumption (subset directories objects) :notes "∀x·(tcl(parent))∼[{x}] ◁ parent∈((tcl(parent))∼[{x}]∪{x}) ∖ {x} → (tcl(parent))∼[{x}]∪{x}" :assumption (forall ((x OBJECT)) true) :notes "usr∈users" :assumption (in usr users) :notes "files⊆objects" :assumption (subset files objects) :notes "subparent=des ◁ parent" :assumption (= subparent (restrict parent des)) :notes "des=(tcl(parent))∼[{obj}]" :assumption (= des (relImage10 (relConverse12 (tcl (pfun2Relation13 parent))) (insert obj (as emptySet (Set OBJECT))))) :notes "CONTENT=ℕ ⇸ DATA" :assumption true :notes "obj∈(files∪directories) ∖ {root}" :assumption (in obj (setminus (union files directories))) :notes "to∉des∪{obj}" :assumption (not (in to (union des (insert obj (as emptySet (Set OBJECT)))))) :notes "∀o,u,p,s,g,m·o∈OBJECT∧u∈USER∧p∈OBJECT ↔ PERMISSION∧s∈OBJECT ⇸ USER∧g∈OBJECT ⇸ GROUP∧m∈USER ↔ GROUP∧o∈dom(g)⇒(o ↦ u∈RPerm(p ↦ s ↦ g ↦ m)⇔(o ↦ u∈s∧o ↦ rbo∈p)∨(g(o)∈m[{u}]∧o ↦ rbg∈p)∨o ↦ rbw∈p∨u=su)" :assumption (forall ((o OBJECT)(u USER)(p (Set ((ind Tuple 2) OBJECT PERMISSION)))(s (Map OBJECT USER))(g (Map OBJECT GROUP))(m (Set ((ind Tuple 2) USER GROUP)))) (implies (and true true true true true true (in o (domain g))) (= (in ((ind tuple 2) o u) (RPerm ((ind tuple 2) ((ind tuple 2) ((ind tuple 2) p s) g) m))) (or (and (in ((ind tuple 2) o u) (pfun2Relation28 s)) (in ((ind tuple 2) o rbo) p)) (and (in (apply g o) (relImage29 m (insert u (as emptySet (Set USER))))) (in ((ind tuple 2) o rbg) p)) (in ((ind tuple 2) o rbw) p) (= u su))))) :notes "XPerm∈(OBJECT ↔ PERMISSION) × (OBJECT ⇸ USER) × (OBJECT ⇸ GROUP) × (USER ↔ GROUP) → (OBJECT ↔ USER)" :assumption true :notes "∀T·root∈T∧parent∼[T]⊆T⇒objects⊆T" :assumption (forall ((T (Set OBJECT))) (implies (and (in root T) (subset (relImage10 (pfunConverse11 parent) T) T)) (subset objects T))) :notes "∀x,s·s⊆((tcl(parent))∼[{x}] ◁ parent)∼[s]⇒s=∅" :assumption (forall ((x OBJECT)(s (Set OBJECT))) (implies (subset s (relImage10 (pfunConverse11 (restrict parent (relImage10 (relConverse12 (tcl (pfun2Relation13 parent))) (insert x (as emptySet (Set OBJECT)))))) s)) (= s (as emptySet (Set OBJECT))))) :notes "∀r·r∈objrel⇒tcl(r)=r∪(r;tcl(r))" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (= (tcl r) (union r (joinRelations39 r (tcl r)) )))) :notes "∀o,u,p,s,g,m·o∈OBJECT∧u∈USER∧p∈OBJECT ↔ PERMISSION∧s∈OBJECT ⇸ USER∧g∈OBJECT ⇸ GROUP∧m∈USER ↔ GROUP∧o∈dom(g)⇒(o ↦ u∈WPerm(p ↦ s ↦ g ↦ m)⇔(o ↦ u∈s∧o ↦ wbo∈p)∨(g(o)∈m[{u}]∧o ↦ wbg∈p)∨o ↦ wbw∈p∨u=su)" :assumption (forall ((o OBJECT)(u USER)(p (Set ((ind Tuple 2) OBJECT PERMISSION)))(s (Map OBJECT USER))(g (Map OBJECT GROUP))(m (Set ((ind Tuple 2) USER GROUP)))) (implies (and true true true true true true (in o (domain g))) (= (in ((ind tuple 2) o u) (WPerm ((ind tuple 2) ((ind tuple 2) ((ind tuple 2) p s) g) m))) (or (and (in ((ind tuple 2) o u) (pfun2Relation28 s)) (in ((ind tuple 2) o wbo) p)) (and (in (apply g o) (relImage29 m (insert u (as emptySet (Set USER))))) (in ((ind tuple 2) o wbg) p)) (in ((ind tuple 2) o wbw) p) (= u su))))) :notes "objects ∖ {root}⊆(tcl(parent))∼[{root}]" :assumption (subset (setminus objects (insert root (as emptySet (Set OBJECT)))) (relImage10 (relConverse12 (tcl (pfun2Relation13 parent))) (insert root (as emptySet (Set OBJECT))))) :notes "obj_perms∈files∪directories ↔ PERMISSION" :assumption true :notes "root∈directories" :assumption (in root directories) :notes "RPerm∈(OBJECT ↔ PERMISSION) × (OBJECT ⇸ USER) × (OBJECT ⇸ GROUP) × (USER ↔ GROUP) → (OBJECT ↔ USER)" :assumption true :notes "su∈USER" :assumption true :notes "objects⊆{root}∪(tcl(parent))∼[{root}]" :assumption (subset objects (union (insert root (as emptySet (Set OBJECT))) (relImage10 (relConverse12 (tcl (pfun2Relation13 parent))) (insert root (as emptySet (Set OBJECT)))))) :notes "replica=corres∼;subparent;corres" :assumption (= replica (joinRelations39 (joinRelations39 (pfunConverse11 corres) (pfun2Relation13 subparent)) (pfun2Relation13 corres)) ) :notes "corres∈objs ⤖ nobjs" :assumption true :notes "groups⊆GROUP" :assumption true :notes "∀u·u∈users⇒user_pgrp(u)∈user_grps[{u}]" :assumption (forall ((u USER)) (implies (in u users) (in (apply |user_pgrp| u) (relImage29 |user_grps| (insert u (as emptySet (Set USER))))))) :notes "∀r,t·r∈objrel∧r⊆t∧r;t⊆t⇒tcl(r)⊆t" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))(t (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies (and true (subset r t) (subset (joinRelations39 r t) t)) (subset (tcl r) t))) :notes "ran(parent)⊆directories" :assumption (subset (range parent) directories) :notes "files∪fs=files∪corres[objs∩files]" :formula (not (= (union files fs) (union files (range (restrict corres (inter objs files)))))) )