(benchmark crt_file_inv1_INV :logic LRM :extrasorts ((OBJECT 0)) :extrafuns ((parent (Map OBJECT OBJECT))) :extrafuns ((root OBJECT)) :extrafuns ((tcl (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT)))) :extrafuns ((|objects'| (Set OBJECT))) :extrafuns ((obj OBJECT)) :extrafuns ((directories (Set OBJECT))) :extrafuns ((files (Set OBJECT))) :extrafuns ((|parent'| (Set ((ind Tuple 2) OBJECT OBJECT)))) :extrafuns ((|files'| (Set OBJECT))) :extrafuns ((indr OBJECT)) :extrafuns ((objects (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 ((joinRelations13 (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) (joinRelations13 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 "obj∈OBJECT ∖ (files∪directories)" :assumption (not (or (in obj files) (in obj directories))) :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 "∀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 "∀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 "∀x·(tcl(parent))∼[{x}] ◁ parent∈(tcl(parent))∼[{x}] → (tcl(parent))∼[{x}]∪{x}" :assumption (forall ((x OBJECT)) true) :notes "∀s·s⊆parent∼[s]⇒s=∅" :assumption (forall ((s (Set OBJECT))) (implies (subset s (relImage2 (pfunConverse3 parent) s)) (= s (as emptySet (Set OBJECT))))) :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 (joinRelations13 (joinRelations13 (pfunConverse3 c) (pfun2Relation5 f)) (pfun2Relation5 c)) )) true)) :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 "∀x·(tcl(parent))∼[{x}] ◁ parent∈((tcl(parent))∼[{x}]∪{x}) ∖ {x} → (tcl(parent))∼[{x}]∪{x}" :assumption (forall ((x OBJECT)) true) :notes "indr∈directories" :assumption (in indr directories) :notes "files⊆objects" :assumption (subset files objects) :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 "∀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 ((var23 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var23 (tcl (pfun2Relation5 parent))) (= ((ind project 2 1) var23) ((ind project 2 2) var23))) (in var23 (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) (joinRelations13 (joinRelations13 (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 (joinRelations13 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 (joinRelations13 r (tcl r)) )))) :notes "tcl(∅)=∅" :assumption (= (tcl (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))) (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))) :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 (joinRelations13 r t) t)) (subset (tcl r) t))) :notes "ran(parent)⊆directories" :assumption (subset (range parent) directories) :notes "ran(parent{obj ↦ indr})⊆directories" :formula (not (subset (range (overwrite parent obj indr)) directories)) )