:: MSAFREE3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let S be non empty non void ManySortedSign ;
let A be non empty MSAlgebra of S;
cluster Union the Sorts of A -> non empty ;
coherence
not Union the Sorts of A is empty
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let A be non empty MSAlgebra of S;
mode Element of A is Element of Union the Sorts of A;
end;

theorem Th1: :: MSAFREE3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for f being Function st X c= dom f & f is one-to-one holds
f " (f .: X) = X
proof end;

theorem :: MSAFREE3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I st F is "1-1" & A c= doms F holds
F "" (F .:.: A) = A
proof end;

definition
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
canceled;
func Free S,X -> strict MSAlgebra of S means :Def2: :: MSAFREE3:def 2
ex A being MSSubset of (FreeMSA (X \/ (the carrier of S --> {0}))) st
( it = GenMSAlg A & A = (Reverse (X \/ (the carrier of S --> {0}))) "" X );
uniqueness
for b1, b2 being strict MSAlgebra of S st ex A being MSSubset of (FreeMSA (X \/ (the carrier of S --> {0}))) st
( b1 = GenMSAlg A & A = (Reverse (X \/ (the carrier of S --> {0}))) "" X ) & ex A being MSSubset of (FreeMSA (X \/ (the carrier of S --> {0}))) st
( b2 = GenMSAlg A & A = (Reverse (X \/ (the carrier of S --> {0}))) "" X ) holds
b1 = b2
;
existence
ex b1 being strict MSAlgebra of S ex A being MSSubset of (FreeMSA (X \/ (the carrier of S --> {0}))) st
( b1 = GenMSAlg A & A = (Reverse (X \/ (the carrier of S --> {0}))) "" X )
proof end;
end;

:: deftheorem MSAFREE3:def 1 :
canceled;

:: deftheorem Def2 defines Free MSAFREE3:def 2 :
for S being non void Signature
for X being ManySortedSet of the carrier of S
for b3 being strict MSAlgebra of S holds
( b3 = Free S,X iff ex A being MSSubset of (FreeMSA (X \/ (the carrier of S --> {0}))) st
( b3 = GenMSAlg A & A = (Reverse (X \/ (the carrier of S --> {0}))) "" X ) );

theorem Th3: :: MSAFREE3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for S being non void Signature
for X being V3 ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( [x,s] in the carrier of (DTConMSA X) iff x in X . s )
proof end;

theorem Th4: :: MSAFREE3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for S being non void Signature
for Y being V3 ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )
proof end;

theorem Th5: :: MSAFREE3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for S being non void Signature
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S st x in X . s holds
root-tree [x,s] in the Sorts of (Free S,X) . s
proof end;

theorem Th6: :: MSAFREE3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being ManySortedSet of the carrier of S
for o being OperSymbol of S st the_arity_of o = {} holds
root-tree [o,the carrier of S] in the Sorts of (Free S,X) . (the_result_sort_of o)
proof end;

registration
let S be non void Signature;
let X be V4 ManySortedSet of the carrier of S;
cluster Free S,X -> strict non empty ;
coherence
not Free S,X is empty
proof end;
end;

theorem :: MSAFREE3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for S being non void Signature
for X being V3 ManySortedSet of the carrier of S holds
( x is Element of (FreeMSA X) iff x is Term of S,X )
proof end;

theorem Th8: :: MSAFREE3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being V3 ManySortedSet of the carrier of S
for s being SortSymbol of S
for x being Term of S,X holds
( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s )
proof end;

theorem Th9: :: MSAFREE3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being V4 ManySortedSet of the carrier of S
for x being Element of (Free S,X) holds x is Term of S,(X \/ (the carrier of S --> {0}))
proof end;

registration
let S be non empty non void ManySortedSign ;
let X be V4 ManySortedSet of the carrier of S;
cluster -> Relation-like Function-like Element of Union the Sorts of (Free S,X);
coherence
for b1 being Element of (Free S,X) holds
( b1 is Relation-like & b1 is Function-like )
by Th9;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V4 ManySortedSet of the carrier of S;
cluster -> Relation-like Function-like finite DecoratedTree-like Element of Union the Sorts of (Free S,X);
coherence
for b1 being Element of (Free S,X) holds
( b1 is finite & b1 is DecoratedTree-like )
by Th9;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V4 ManySortedSet of the carrier of S;
cluster -> Relation-like Function-like finite DecoratedTree-like finite-branching Element of Union the Sorts of (Free S,X);
coherence
for b1 being Element of (Free S,X) holds b1 is finite-branching
;
end;

registration
cluster -> non empty set ;
coherence
for b1 being DecoratedTree holds not b1 is empty
proof end;
end;

definition
let S be ManySortedSign ;
let t be non empty Relation;
func S variables_in t -> ManySortedSet of the carrier of S means :Def3: :: MSAFREE3:def 3
for s being set st s in the carrier of S holds
it . s = { (a `1 ) where a is Element of rng t : a `2 = s } ;
existence
ex b1 being ManySortedSet of the carrier of S st
for s being set st s in the carrier of S holds
b1 . s = { (a `1 ) where a is Element of rng t : a `2 = s }
proof end;
uniqueness
for b1, b2 being ManySortedSet of the carrier of S st ( for s being set st s in the carrier of S holds
b1 . s = { (a `1 ) where a is Element of rng t : a `2 = s } ) & ( for s being set st s in the carrier of S holds
b2 . s = { (a `1 ) where a is Element of rng t : a `2 = s } ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines variables_in MSAFREE3:def 3 :
for S being ManySortedSign
for t being non empty Relation
for b3 being ManySortedSet of the carrier of S holds
( b3 = S variables_in t iff for s being set st s in the carrier of S holds
b3 . s = { (a `1 ) where a is Element of rng t : a `2 = s } );

definition
let S be ManySortedSign ;
let X be ManySortedSet of the carrier of S;
let t be non empty Relation;
func X variables_in t -> ManySortedSubset of X equals :: MSAFREE3:def 4
X /\ (S variables_in t);
coherence
X /\ (S variables_in t) is ManySortedSubset of X
proof end;
end;

:: deftheorem defines variables_in MSAFREE3:def 4 :
for S being ManySortedSign
for X being ManySortedSet of the carrier of S
for t being non empty Relation holds X variables_in t = X /\ (S variables_in t);

theorem Th10: :: MSAFREE3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being ManySortedSign
for X being ManySortedSet of the carrier of S
for t being non empty Relation
for V being ManySortedSubset of X holds
( V = X variables_in t iff for s being set st s in the carrier of S holds
V . s = (X . s) /\ { (a `1 ) where a is Element of rng t : a `2 = s } )
proof end;

theorem Th11: :: MSAFREE3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being ManySortedSign
for s, x being set holds
( ( s in the carrier of S implies (S variables_in (root-tree [x,s])) . s = {x} ) & ( for s' being set st ( s' <> s or not s in the carrier of S ) holds
(S variables_in (root-tree [x,s])) . s' = {} ) )
proof end;

theorem Th12: :: MSAFREE3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, z being set
for S being ManySortedSign
for s being set st s in the carrier of S holds
for p being DTree-yielding FinSequence holds
( x in (S variables_in ([z,the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (S variables_in t) . s ) )
proof end;

theorem Th13: :: MSAFREE3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being ManySortedSign
for X being ManySortedSet of the carrier of S
for s, x being set holds
( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s' being set st ( s' <> s or not x in X . s ) holds
(X variables_in (root-tree [x,s])) . s' = {} ) )
proof end;

theorem Th14: :: MSAFREE3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, z being set
for S being ManySortedSign
for X being ManySortedSet of the carrier of S
for s being set st s in the carrier of S holds
for p being DTree-yielding FinSequence holds
( x in (X variables_in ([z,the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) )
proof end;

theorem Th15: :: MSAFREE3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being V3 ManySortedSet of the carrier of S
for t being Term of S,X holds S variables_in t c= X
proof end;

definition
let S be non void Signature;
let X be V3 ManySortedSet of the carrier of S;
let t be Term of S,X;
func variables_in t -> ManySortedSubset of X equals :: MSAFREE3:def 5
S variables_in t;
correctness
coherence
S variables_in t is ManySortedSubset of X
;
proof end;
end;

:: deftheorem defines variables_in MSAFREE3:def 5 :
for S being non void Signature
for X being V3 ManySortedSet of the carrier of S
for t being Term of S,X holds variables_in t = S variables_in t;

theorem Th16: :: MSAFREE3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being V3 ManySortedSet of the carrier of S
for t being Term of S,X holds variables_in t = X variables_in t
proof end;

definition
let S be non void Signature;
let Y be V3 ManySortedSet of the carrier of S;
let X be ManySortedSet of the carrier of S;
func S -Terms X,Y -> MSSubset of (FreeMSA Y) means :Def6: :: MSAFREE3:def 6
for s being SortSymbol of S holds it . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ;
existence
ex b1 being MSSubset of (FreeMSA Y) st
for s being SortSymbol of S holds b1 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) }
proof end;
correctness
uniqueness
for b1, b2 being MSSubset of (FreeMSA Y) st ( for s being SortSymbol of S holds b1 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ) & ( for s being SortSymbol of S holds b2 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def6 defines -Terms MSAFREE3:def 6 :
for S being non void Signature
for Y being V3 ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for b4 being MSSubset of (FreeMSA Y) holds
( b4 = S -Terms X,Y iff for s being SortSymbol of S holds b4 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } );

theorem Th17: :: MSAFREE3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for S being non void Signature
for Y being V3 ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S st x in (S -Terms X,Y) . s holds
x is Term of S,Y
proof end;

theorem Th18: :: MSAFREE3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for Y being V3 ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for t being Term of S,Y
for s being SortSymbol of S st t in (S -Terms X,Y) . s holds
( the_sort_of t = s & variables_in t c= X )
proof end;

theorem Th19: :: MSAFREE3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for S being non void Signature
for Y being V3 ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( root-tree [x,s] in (S -Terms X,Y) . s iff ( x in X . s & x in Y . s ) )
proof end;

theorem Th20: :: MSAFREE3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for Y being V3 ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being ArgumentSeq of Sym o,Y holds
( (Sym o,Y) -tree p in (S -Terms X,Y) . (the_result_sort_of o) iff rng p c= Union (S -Terms X,Y) )
proof end;

theorem Th21: :: MSAFREE3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being V3 ManySortedSet of the carrier of S
for A being MSSubset of (FreeMSA X) holds
( A is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym o,X st rng p c= Union A holds
(Sym o,X) -tree p in A . (the_result_sort_of o) )
proof end;

theorem Th22: :: MSAFREE3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for Y being V3 ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S holds S -Terms X,Y is opers_closed
proof end;

theorem Th23: :: MSAFREE3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for Y being V3 ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S holds (Reverse Y) "" X c= S -Terms X,Y
proof end;

theorem Th24: :: MSAFREE3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being ManySortedSet of the carrier of S
for t being Term of S,(X \/ (the carrier of S --> {0}))
for s being SortSymbol of S st t in (S -Terms X,(X \/ (the carrier of S --> {0}))) . s holds
t in the Sorts of (Free S,X) . s
proof end;

theorem Th25: :: MSAFREE3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being ManySortedSet of the carrier of S holds the Sorts of (Free S,X) = S -Terms X,(X \/ (the carrier of S --> {0}))
proof end;

theorem :: MSAFREE3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being ManySortedSet of the carrier of S holds (FreeMSA (X \/ (the carrier of S --> {0}))) | (S -Terms X,(X \/ (the carrier of S --> {0}))) = Free S,X
proof end;

theorem Th27: :: MSAFREE3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X, Y being V3 ManySortedSet of the carrier of S
for A being MSSubAlgebra of FreeMSA X
for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds
MSAlgebra(# the Sorts of A,the Charact of A #) = MSAlgebra(# the Sorts of B,the Charact of B #)
proof end;

theorem Th28: :: MSAFREE3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being V4 ManySortedSet of the carrier of S
for Y being ManySortedSet of the carrier of S
for t being Element of (Free S,X) holds S variables_in t c= X
proof end;

theorem Th29: :: MSAFREE3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being V3 ManySortedSet of the carrier of S
for t being Term of S,X holds variables_in t c= X
proof end;

theorem Th30: :: MSAFREE3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X, Y being V3 ManySortedSet of the carrier of S
for t1 being Term of S,X
for t2 being Term of S,Y st t1 = t2 holds
the_sort_of t1 = the_sort_of t2
proof end;

theorem Th31: :: MSAFREE3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X, Y being V3 ManySortedSet of the carrier of S
for t being Term of S,Y st variables_in t c= X holds
t is Term of S,X
proof end;

theorem :: MSAFREE3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being V3 ManySortedSet of the carrier of S holds Free S,X = FreeMSA X
proof end;

theorem Th33: :: MSAFREE3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for Y being V3 ManySortedSet of the carrier of S
for t being Term of S,Y
for p being Element of dom t holds variables_in (t | p) c= variables_in t
proof end;

theorem Th34: :: MSAFREE3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being V4 ManySortedSet of the carrier of S
for t being Element of (Free S,X)
for p being Element of dom t holds t | p is Element of (Free S,X)
proof end;

theorem Th35: :: MSAFREE3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being V3 ManySortedSet of the carrier of S
for t being Term of S,X
for a being Element of rng t holds a = [(a `1 ),(a `2 )]
proof end;

theorem :: MSAFREE3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for S being non void Signature
for X being V4 ManySortedSet of the carrier of S
for t being Element of (Free S,X)
for s being SortSymbol of S holds
( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )
proof end;

theorem :: MSAFREE3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being ManySortedSet of the carrier of S st ( for s being SortSymbol of S st X . s = {} holds
ex o being OperSymbol of S st
( the_result_sort_of o = s & the_arity_of o = {} ) ) holds
Free S,X is non-empty
proof end;

theorem Th38: :: MSAFREE3:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for B being MSSubAlgebra of A
for o being OperSymbol of S holds Args o,B c= Args o,A
proof end;

theorem Th39: :: MSAFREE3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for A being feasible MSAlgebra of S
for B being MSSubAlgebra of A holds B is feasible
proof end;

registration
let S be non void Signature;
let A be feasible MSAlgebra of S;
cluster -> feasible MSSubAlgebra of A;
coherence
for b1 being MSSubAlgebra of A holds b1 is feasible
by Th39;
end;

theorem Th40: :: MSAFREE3:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non void Signature
for X being ManySortedSet of the carrier of S holds
( Free S,X is feasible & Free S,X is free )
proof end;

registration
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
cluster Free S,X -> strict free feasible ;
coherence
( Free S,X is feasible & Free S,X is free )
by Th40;
end;