(benchmark delete_inv2_INV :logic LRM :extrasorts ((NAME 0)) :extrasorts ((DATA 0)) :extrasorts ((OBJECT 0)) :extrafuns ((des (Set OBJECT))) :extrafuns ((parent (Map OBJECT OBJECT))) :extrafuns ((root OBJECT)) :extrafuns ((tcl (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT)))) :extrafuns ((fcontent (Map OBJECT (Map Int DATA)))) :extrafuns ((fbuffer (Map OBJECT (Map Int DATA)))) :extrafuns ((objs (Set OBJECT))) :extrafuns ((|fcontent'| (Set ((ind Tuple 2) OBJECT (Set ((ind Tuple 2) Int DATA)))))) :extrafuns ((|directories'| (Set OBJECT))) :extrafuns ((obj OBJECT)) :extrafuns ((|parent'| (Set ((ind Tuple 2) OBJECT OBJECT)))) :extrafuns ((|files'| (Set OBJECT))) :extrafuns ((directories (Set OBJECT))) :extrafuns ((files (Set OBJECT))) :extrafuns ((objects (Set OBJECT))) :extrafuns ((rname NAME)) :extrafuns ((|opened_files| (Set OBJECT))) :extrafuns ((relImage2 (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 (relImage2 r s)) (exists ((a OBJECT)) (and (in a s) (in ((ind tuple 2) a b) r))))) :extrafuns ((relConverse4 (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) (relConverse4 f)) (in ((ind tuple 2) a b) f))) :extrafuns ((pfun2Relation5 (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) (pfun2Relation5 f)) (and (in a (domain f)) (= b (apply f a))))) :extrafuns ((pfunConverse3 ((x (Map OBJECT OBJECT))) (relConverse4 (pfun2Relation5 x)))) :extrafuns ((joinRelations16 (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) (joinRelations16 r1 r2)) (exists ((b OBJECT)) (and (in ((ind tuple 2) a b) r1) (in ((ind tuple 2) b c) r2))))) :notes "objfn=OBJECT ∖ {root} ⇸ OBJECT" :assumption true :notes "objects∈ℙ(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 ((var1 OBJECT)) (implies (in var1 (domain t)) (not (= var1 root)))) (forall ((s (Set OBJECT))) (implies (subset s (relImage2 (pfunConverse3 t) s)) (= s (as emptySet (Set OBJECT)))))) (forall ((var6 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var6 (tcl (pfun2Relation5 t))) (= ((ind project 2 1) var6) ((ind project 2 2) var6))) (in var6 (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))))) :notes "∅∈CONTENT" :assumption (forall ((var7 Int) (var8 DATA) (var9 DATA)) (implies (and (in ((ind tuple 2) var7 var8) (as emptySet (Set ((ind Tuple 2) Int DATA)))) (in ((ind tuple 2) var7 var9) (as emptySet (Set ((ind Tuple 2) Int DATA))))) (and (= var8 var9) (>= var7 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 (relImage2 r s)) (= s (as emptySet (Set OBJECT)))))) (forall ((t (Set OBJECT))) (implies (subset t (relImage2 r2 t)) (= t (as emptySet (Set OBJECT))))))) :notes "des⊆files∪directories" :assumption (subset des (union files directories)) :notes "∀x·x∉ran(parent)⇒(tcl(parent))∼[{x}]=∅" :assumption (forall ((x OBJECT)) (implies (not (in x (range parent))) (= (relImage2 (relConverse4 (tcl (pfun2Relation5 parent))) (insert x (as emptySet (Set OBJECT)))) (as emptySet (Set OBJECT))))) :notes "objrel=OBJECT ↔ OBJECT" :assumption true :notes "fbuffer∈opened_files → CONTENT" :assumption true :notes "objs=des∪{obj}" :assumption (= objs (union des (insert obj (as emptySet (Set OBJECT))))) :notes "∀s·s⊆parent∼[s]⇒s=∅" :assumption (forall ((s (Set OBJECT))) (implies (subset s (relImage2 (pfunConverse3 parent) s)) (= s (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 (joinRelations16 (joinRelations16 (pfunConverse3 c) (pfun2Relation5 f)) (pfun2Relation5 c)) )) true)) :notes "opened_files⊆files" :assumption (subset |opened_files| files) :notes "tcl∈objrel → objrel" :assumption true :notes "directories⊆objects" :assumption (subset directories objects) :notes "objects=files∪directories" :assumption (= objects (union files directories)) :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 "objs∩opened_files=∅" :assumption (= (inter objs |opened_files|) (as emptySet (Set OBJECT))) :notes "∀x·(tcl(parent))∼[{x}] ◁ parent∈((tcl(parent))∼[{x}]∪{x}) ∖ {x} → (tcl(parent))∼[{x}]∪{x}" :assumption (forall ((x OBJECT)) true) :notes "files⊆objects" :assumption (subset files objects) :notes "des=(tcl(parent))∼[{obj}]" :assumption (= des (relImage2 (relConverse4 (tcl (pfun2Relation5 parent))) (insert obj (as emptySet (Set OBJECT))))) :notes "root∈objects" :assumption (in root objects) :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 (relImage2 (pfunConverse3 f) A)) (= A (as emptySet (Set OBJECT))))) (forall ((B (Set OBJECT))) (implies (subset B (relImage2 (pfunConverse3 g) B)) (= B (as emptySet (Set OBJECT))))) false) (forall ((C (Set OBJECT))) (implies (subset C (relImage2 (relConverse4 (union (pfun2Relation5 f) (pfun2Relation5 g) (insert ((ind tuple 2) u x) (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))) C)) (= C (as emptySet (Set OBJECT))))))) :notes "obj∈(files∪directories) ∖ {root}" :assumption (in obj (setminus (union files directories))) :notes "CONTENT=ℕ ⇸ DATA" :assumption true :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 ((var26 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var26 (tcl (pfun2Relation5 parent))) (= ((ind project 2 1) var26) ((ind project 2 2) var26))) (in var26 (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))) :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 (relImage2 (pfunConverse3 f) s)) (= s (as emptySet (Set OBJECT))))) (in u N) false (= u (apply c t)) (= (pfun2Relation5 g) (joinRelations16 (joinRelations16 (pfunConverse3 c) (pfun2Relation5 f)) (pfun2Relation5 c)) ) false) (forall ((w (Set OBJECT))) (implies (subset w (relImage2 (pfunConverse3 g) w)) (= w (as emptySet (Set OBJECT))))))) :notes "objfn⊆objrel" :assumption true :notes "parent∈objects ∖ {root} → objects" :assumption true :notes "root∈OBJECT" :assumption true :notes "∀T·root∈T∧parent∼[T]⊆T⇒objects⊆T" :assumption (forall ((T (Set OBJECT))) (implies (and (in root T) (subset (relImage2 (pfunConverse3 parent) T) T)) (subset objects T))) :notes "∀r·r∈objrel⇒r;tcl(r)⊆tcl(r)" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (subset (joinRelations16 r (tcl r)) (tcl r)))) :notes "∀x,s·s⊆((tcl(parent))∼[{x}] ◁ parent)∼[s]⇒s=∅" :assumption (forall ((x OBJECT)(s (Set OBJECT))) (implies (subset s (relImage2 (pfunConverse3 (restrict parent (relImage2 (relConverse4 (tcl (pfun2Relation5 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 (joinRelations16 r (tcl r)) )))) :notes "tcl(∅)=∅" :assumption (= (tcl (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))) (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))) :notes "rname∈NAME" :assumption true :notes "objects ∖ {root}⊆(tcl(parent))∼[{root}]" :assumption (subset (setminus objects (insert root (as emptySet (Set OBJECT)))) (relImage2 (relConverse4 (tcl (pfun2Relation5 parent))) (insert root (as emptySet (Set OBJECT))))) :notes "files∩directories=∅" :assumption (= (inter files directories) (as emptySet (Set OBJECT))) :notes "root∈directories" :assumption (in root directories) :notes "⊤" :assumption true :notes "objects⊆{root}∪(tcl(parent))∼[{root}]" :assumption (subset objects (union (insert root (as emptySet (Set OBJECT))) (relImage2 (relConverse4 (tcl (pfun2Relation5 parent))) (insert root (as emptySet (Set OBJECT)))))) :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 (joinRelations16 r t) t)) (subset (tcl r) t))) :notes "ran(parent)⊆directories" :assumption (subset (range parent) directories) :notes "opened_files⊆files ∖ (objs∩files)" :formula (not (subset |opened_files| (setminus files (inter objs files)))) )