(benchmark INITIALISATION_inv7_INV :logic LRM :extrasorts ((NAME 0)) :extrasorts ((DATA 0)) :extrasorts ((USER 0)) :extrasorts ((OBJECT 0)) :extrasorts ((GROUP 0)) :extrasorts ((PERMISSION 0)) :extrafuns ((xbg PERMISSION)) :extrafuns ((wbg PERMISSION)) :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 ((|groups'| (Set GROUP))) :extrafuns ((root OBJECT)) :extrafuns ((|obj_grp'| (Set ((ind Tuple 2) OBJECT GROUP)))) :extrafuns ((xbw PERMISSION)) :extrafuns ((|directories'| (Set OBJECT))) :extrafuns ((|user_pgrp'| (Set ((ind Tuple 2) USER GROUP)))) :extrafuns ((su USER)) :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 ((|users'| (Set USER))) :extrafuns ((|user_grps'| (Set ((ind Tuple 2) USER GROUP)))) :extrafuns ((rbw PERMISSION)) :extrafuns ((|obj_perms'| (Set ((ind Tuple 2) OBJECT PERMISSION)))) :extrafuns ((wbo PERMISSION)) :extrafuns ((rname NAME)) :extrafuns ((admin GROUP)) :extrafuns ((tcl (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) 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 ((|opened_files'| (Set OBJECT))) :extrafuns ((|fcontent'| (Set ((ind Tuple 2) OBJECT (Set ((ind Tuple 2) Int DATA)))))) :extrafuns ((|fbuffer'| (Set ((ind Tuple 2) OBJECT (Set ((ind Tuple 2) Int DATA)))))) :extrafuns ((|obj_owner'| (Set ((ind Tuple 2) OBJECT USER)))) :extrafuns ((xbo PERMISSION)) :extrafuns ((|parent'| (Set ((ind Tuple 2) OBJECT OBJECT)))) :extrafuns ((|files'| (Set OBJECT))) :extrafuns ((wbw PERMISSION)) :extrafuns ((relImage11 (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 (relImage11 r s)) (exists ((a OBJECT)) (and (in a s) (in ((ind tuple 2) a b) r))))) :extrafuns ((relConverse13 (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) (relConverse13 f)) (in ((ind tuple 2) a b) f))) :extrafuns ((pfun2Relation14 (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) (pfun2Relation14 f)) (and (in a (domain f)) (= b (apply f a))))) :extrafuns ((pfunConverse12 ((x (Map OBJECT OBJECT))) (relConverse13 (pfun2Relation14 x)))) :extrafuns ((joinRelations25 (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) (joinRelations25 r1 r2)) (exists ((b OBJECT)) (and (in ((ind tuple 2) a b) r1) (in ((ind tuple 2) b c) r2))))) :extrafuns ((pfun2Relation39 (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) (pfun2Relation39 f)) (and (in a (domain f)) (= b (apply f a))))) :extrafuns ((relImage40 (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 (relImage40 r s)) (exists ((a USER)) (and (in a s) (in ((ind tuple 2) a b) r))))) :notes "PERMISSION={rbo,wbo,xbo,rbg,wbg,xbg,rbw,wbw,xbw}" :assumption (forall ((var0 PERMISSION)) (= true (or (= var0 rbo) (= var0 wbo) (= var0 xbo) (= var0 rbg) (= var0 wbg) (= var0 xbg) (= var0 rbw) (= var0 wbw) (= var0 xbw)))) :notes "objfn=OBJECT ∖ {root} ⇸ OBJECT" :assumption true :notes "WPerm∈(OBJECT ↔ PERMISSION) × (OBJECT ⇸ USER) × (OBJECT ⇸ GROUP) × (USER ↔ GROUP) → (OBJECT ↔ USER)" :assumption true :notes "∀t·t∈objfn∧(∀s·s⊆t∼[s]⇒s=∅)⇒tcl(t)∩(OBJECT ◁ id)=∅" :assumption (forall ((t (Map OBJECT OBJECT))) (implies (and (forall ((var10 OBJECT)) (implies (in var10 (domain t)) (not (= var10 root)))) (forall ((s (Set OBJECT))) (implies (subset s (relImage11 (pfunConverse12 t) s)) (= s (as emptySet (Set OBJECT)))))) (forall ((var15 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var15 (tcl (pfun2Relation14 t))) (= ((ind project 2 1) var15) ((ind project 2 2) var15))) (in var15 (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))))) :notes "∅∈CONTENT" :assumption (forall ((var16 Int) (var17 DATA) (var18 DATA)) (implies (and (in ((ind tuple 2) var16 var17) (as emptySet (Set ((ind Tuple 2) Int DATA)))) (in ((ind tuple 2) var16 var18) (as emptySet (Set ((ind Tuple 2) Int DATA))))) (and (= var17 var18) (>= var16 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 (relImage11 r s)) (= s (as emptySet (Set OBJECT)))))) (forall ((t (Set OBJECT))) (implies (subset t (relImage11 r2 t)) (= t (as emptySet (Set OBJECT))))))) :notes "objrel=OBJECT ↔ OBJECT" :assumption 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 (joinRelations25 (joinRelations25 (pfunConverse12 c) (pfun2Relation14 f)) (pfun2Relation14 c)) )) true)) :notes "admin∈GROUP" :assumption true :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 "∀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) (pfun2Relation39 s)) (in ((ind tuple 2) o xbo) p)) (and (in (apply g o) (relImage40 m (insert u (as emptySet (Set USER))))) (in ((ind tuple 2) o xbg) p)) (in ((ind tuple 2) o xbw) p) (= u su))))) :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 (relImage11 (pfunConverse12 f) A)) (= A (as emptySet (Set OBJECT))))) (forall ((B (Set OBJECT))) (implies (subset B (relImage11 (pfunConverse12 g) B)) (= B (as emptySet (Set OBJECT))))) false) (forall ((C (Set OBJECT))) (implies (subset C (relImage11 (relConverse13 (union (pfun2Relation14 f) (pfun2Relation14 g) (insert ((ind tuple 2) u x) (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))) C)) (= C (as emptySet (Set OBJECT))))))) :notes "CONTENT=ℕ ⇸ DATA" :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 (relImage11 (pfunConverse12 f) s)) (= s (as emptySet (Set OBJECT))))) (in u N) false (= u (apply c t)) (= (pfun2Relation14 g) (joinRelations25 (joinRelations25 (pfunConverse12 c) (pfun2Relation14 f)) (pfun2Relation14 c)) ) false) (forall ((w (Set OBJECT))) (implies (subset w (relImage11 (pfunConverse12 g) w)) (= w (as emptySet (Set OBJECT))))))) :notes "objfn⊆objrel" :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∈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) (pfun2Relation39 s)) (in ((ind tuple 2) o rbo) p)) (and (in (apply g o) (relImage40 m (insert u (as emptySet (Set USER))))) (in ((ind tuple 2) o rbg) p)) (in ((ind tuple 2) o rbw) p) (= u su))))) :notes "root∈OBJECT" :assumption true :notes "XPerm∈(OBJECT ↔ PERMISSION) × (OBJECT ⇸ USER) × (OBJECT ⇸ GROUP) × (USER ↔ GROUP) → (OBJECT ↔ USER)" :assumption true :notes "∀r·r∈objrel⇒r;tcl(r)⊆tcl(r)" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (subset (joinRelations25 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 "∀r·r∈objrel⇒tcl(r)=r∪(r;tcl(r))" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (= (tcl r) (union r (joinRelations25 r (tcl r)) )))) :notes "rname∈NAME" :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∈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) (pfun2Relation39 s)) (in ((ind tuple 2) o wbo) p)) (and (in (apply g o) (relImage40 m (insert u (as emptySet (Set USER))))) (in ((ind tuple 2) o wbg) p)) (in ((ind tuple 2) o wbw) p) (= u su))))) :notes "RPerm∈(OBJECT ↔ PERMISSION) × (OBJECT ⇸ USER) × (OBJECT ⇸ GROUP) × (USER ↔ GROUP) → (OBJECT ↔ USER)" :assumption true :notes "su∈USER" :assumption true :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 "∀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 (joinRelations25 r t) t)) (subset (tcl r) t))) :notes "{su ↦ admin}∈{su} → {admin}" :formula (not false) )