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

registration
let I be set ;
let S be non empty non void ManySortedSign ;
let AF be MSAlgebra-Family of I,S;
cluster product AF -> non-empty ;
coherence
product AF is non-empty
by MSUALG_1:def 8;
end;

definition
let I be set ;
:: original: id
redefine func id I -> ManySortedSet of I;
coherence
id I is ManySortedSet of I
proof end;
end;

registration
let X be with_non-empty_elements set ;
cluster id X -> non-empty ;
coherence
id X is non-empty
proof end;
end;

theorem Th1: :: PRALG_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, F being Function
for A being set st f in product F holds
f | A in product (F | A)
proof end;

theorem Th2: :: PRALG_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for a being non empty Subset of I
for Aa being MSAlgebra-Family of a,S st A | a = Aa holds
Carrier Aa,s = (Carrier A,s) | a
proof end;

theorem Th3: :: PRALG_3:3  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 I being non empty set
for EqR being Equivalence_Relation of I
for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds
c1 = c2
proof end;

Lm1: for f being Function
for x being set st x in product f holds
x is Function
proof end;

theorem :: PRALG_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PRALG_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being ManySortedFunction of D
for C being non empty functional with_common_domain set st C = rng F holds
for d being Element of D
for e being set st d in dom F & e in DOM C holds
(F . d) . e = ((commute F) . e) . d
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let o be OperSymbol of S;
func const o,U0 -> set equals :: PRALG_3:def 1
(Den o,U0) . {} ;
correctness
coherence
(Den o,U0) . {} is set
;
;
end;

:: deftheorem defines const PRALG_3:def 1 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for o being OperSymbol of S holds const o,U0 = (Den o,U0) . {} ;

theorem Th6: :: PRALG_3: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 empty non void ManySortedSign
for U0 being MSAlgebra of S
for o being OperSymbol of S st the_arity_of o = {} & Result o,U0 <> {} holds
const o,U0 in Result o,U0
proof end;

theorem :: PRALG_3:7  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 U0 being MSAlgebra of S
for s being SortSymbol of S st the Sorts of U0 . s <> {} holds
Constants U0,s = { (const o,U0) where o is Element of the OperSymbols of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }
proof end;

theorem Th8: :: PRALG_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(commute (OPER A)) . o in Funcs I,(Funcs {{} },(union { (Result o,(A . i')) where i' is Element of I : verum } ))
proof end;

theorem Th9: :: PRALG_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
const o,(product A) in Funcs I,(union { (Result o,(A . i')) where i' is Element of I : verum } )
proof end;

registration
let S be non empty non void ManySortedSign ;
let I be non empty set ;
let o be OperSymbol of S;
let A be MSAlgebra-Family of I,S;
cluster const o,(product A) -> Relation-like Function-like ;
coherence
( const o,(product A) is Relation-like & const o,(product A) is Function-like )
proof end;
end;

theorem Th10: :: PRALG_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(const o,(product A)) . i = const o,(A . i)
proof end;

theorem :: PRALG_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const o,(A . i) ) holds
f = const o,(product A)
proof end;

theorem Th12: :: PRALG_3:12  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 U1, U2 being MSAlgebra of S
for o being OperSymbol of S
for e being Element of Args o,U1 st e = {} & the_arity_of o = {} & Args o,U1 <> {} & Args o,U2 <> {} holds
for F being ManySortedFunction of U1,U2 holds F # e = {}
proof end;

theorem Th13: :: PRALG_3:13  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 o being OperSymbol of S
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2
for x being Element of Args o,U1 holds x in product (doms (F * (the_arity_of o)))
proof end;

theorem Th14: :: PRALG_3:14  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 o being OperSymbol of S
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2
for x being Element of Args o,U1
for n being set st n in dom (the_arity_of o) holds
(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
proof end;

theorem Th15: :: PRALG_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args o,(product A) holds x in Funcs (dom (the_arity_of o)),(Funcs I,(union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ))
proof end;

theorem Th16: :: PRALG_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args o,(product A)
for n being set st n in dom (the_arity_of o) holds
x . n in product (Carrier A,((the_arity_of o) /. n))
proof end;

theorem Th17: :: PRALG_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for i being Element of I
for n being set st n in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args o,(product A)
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
proof end;

theorem Th18: :: PRALG_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for y being Element of Args o,(product A) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
proof end;

theorem Th19: :: PRALG_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for y being Element of Args o,(product A) st the_arity_of o <> {} holds
y in dom (Commute (Frege (A ?. o)))
proof end;

theorem Th20: :: PRALG_3:20  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 S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args o,(product A) holds (Den o,(product A)) . x in product (Carrier A,(the_result_sort_of o))
proof end;

theorem Th21: :: PRALG_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for i being Element of I
for o being OperSymbol of S st the_arity_of o <> {} holds
for U1 being non-empty MSAlgebra of S
for x being Element of Args o,(product A) holds (commute x) . i is Element of Args o,(A . i)
proof end;

theorem Th22: :: PRALG_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for i being Element of I
for o being OperSymbol of S
for x being Element of Args o,(product A)
for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . i
proof end;

theorem Th23: :: PRALG_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o <> {} holds
for y being Element of Args o,(product A)
for i' being Element of I
for g being Function st g = (Den o,(product A)) . y holds
g . i' = (Den o,(A . i')) . ((commute y) . i')
proof end;

definition
let f be Function;
let x be set ;
func proj f,x -> Function means :Def2: :: PRALG_3:def 2
( dom it = product f & ( for y being Function st y in dom it holds
it . y = y . x ) );
existence
ex b1 being Function st
( dom b1 = product f & ( for y being Function st y in dom b1 holds
b1 . y = y . x ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = product f & ( for y being Function st y in dom b1 holds
b1 . y = y . x ) & dom b2 = product f & ( for y being Function st y in dom b2 holds
b2 . y = y . x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines proj PRALG_3:def 2 :
for f being Function
for x being set
for b3 being Function holds
( b3 = proj f,x iff ( dom b3 = product f & ( for y being Function st y in dom b3 holds
b3 . y = y . x ) ) );

definition
let I be non empty set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
let i be Element of I;
func proj A,i -> ManySortedFunction of (product A),(A . i) means :Def3: :: PRALG_3:def 3
for s being Element of S holds it . s = proj (Carrier A,s),i;
existence
ex b1 being ManySortedFunction of (product A),(A . i) st
for s being Element of S holds b1 . s = proj (Carrier A,s),i
proof end;
uniqueness
for b1, b2 being ManySortedFunction of (product A),(A . i) st ( for s being Element of S holds b1 . s = proj (Carrier A,s),i ) & ( for s being Element of S holds b2 . s = proj (Carrier A,s),i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines proj PRALG_3:def 3 :
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for i being Element of I
for b5 being ManySortedFunction of (product A),(A . i) holds
( b5 = proj A,i iff for s being Element of S holds b5 . s = proj (Carrier A,s),i );

theorem Th24: :: PRALG_3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args o,(product A) st Args o,(product A) <> {} & the_arity_of o <> {} holds
for i being Element of I holds (proj A,i) # x = (commute x) . i
proof end;

theorem :: PRALG_3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S holds proj A,i is_homomorphism product A,A . i
proof end;

theorem Th26: :: PRALG_3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
( F in Funcs I,(Funcs the carrier of S,{ ((F . i') . s1) where s1 is SortSymbol of S, i' is Element of I : verum } ) & ((commute F) . s) . i = (F . i) . s )
proof end;

theorem Th27: :: PRALG_3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
(commute F) . s in Funcs I,(Funcs (the Sorts of U1 . s),(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum } ))
proof end;

theorem Th28: :: PRALG_3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for F' being ManySortedFunction of U1,(A . i) st F' = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F' . s) . x
proof end;

theorem Th29: :: PRALG_3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s)
proof end;

theorem :: PRALG_3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj A,i) ** H = F . i ) )
proof end;

definition
let I be non empty set ;
let J be ManySortedSet of I;
let S be non empty non void ManySortedSign ;
mode MSAlgebra-Class of S,J -> ManySortedSet of I means :Def4: :: PRALG_3:def 4
for i being set st i in I holds
it . i is MSAlgebra-Family of J . i,S;
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i is MSAlgebra-Family of J . i,S
proof end;
end;

:: deftheorem Def4 defines MSAlgebra-Class PRALG_3:def 4 :
for I being non empty set
for J being ManySortedSet of I
for S being non empty non void ManySortedSign
for b4 being ManySortedSet of I holds
( b4 is MSAlgebra-Class of S,J iff for i being set st i in I holds
b4 . i is MSAlgebra-Family of J . i,S );

definition
let I be non empty set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
let EqR be Equivalence_Relation of I;
func A / EqR -> MSAlgebra-Class of S, id (Class EqR) means :Def5: :: PRALG_3:def 5
for c being set st c in Class EqR holds
it . c = A | c;
existence
ex b1 being MSAlgebra-Class of S, id (Class EqR) st
for c being set st c in Class EqR holds
b1 . c = A | c
proof end;
uniqueness
for b1, b2 being MSAlgebra-Class of S, id (Class EqR) st ( for c being set st c in Class EqR holds
b1 . c = A | c ) & ( for c being set st c in Class EqR holds
b2 . c = A | c ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines / PRALG_3:def 5 :
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for EqR being Equivalence_Relation of I
for b5 being MSAlgebra-Class of S, id (Class EqR) holds
( b5 = A / EqR iff for c being set st c in Class EqR holds
b5 . c = A | c );

definition
let I be non empty set ;
let S be non empty non void ManySortedSign ;
let J be V2 ManySortedSet of I;
let C be MSAlgebra-Class of S,J;
func product C -> MSAlgebra-Family of I,S means :Def6: :: PRALG_3:def 6
for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & it . i = product Cs );
existence
ex b1 being MSAlgebra-Family of I,S st
for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b1 . i = product Cs )
proof end;
uniqueness
for b1, b2 being MSAlgebra-Family of I,S st ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b1 . i = product Cs ) ) & ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b2 . i = product Cs ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines product PRALG_3:def 6 :
for I being non empty set
for S being non empty non void ManySortedSign
for J being V2 ManySortedSet of I
for C being MSAlgebra-Class of S,J
for b5 being MSAlgebra-Family of I,S holds
( b5 = product C iff for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b5 . i = product Cs ) );

theorem :: PRALG_3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic
proof end;