:: by Julian J. Schl\"oder and Peter Koepke

::

:: Received May 7, 2012

:: Copyright (c) 2012-2019 Association of Mizar Users

definition
end;

:: deftheorem Def1 defines -expanding QC_TRANS:def 1 :

for Al, Al2 being QC-alphabet holds

( Al2 is Al -expanding iff Al c= Al2 );

for Al, Al2 being QC-alphabet holds

( Al2 is Al -expanding iff Al c= Al2 );

registration
end;

registration

let Al1, Al2 be countable QC-alphabet ;

existence

ex b_{1} being QC-alphabet st

( b_{1} is countable & b_{1} is Al1 -expanding & b_{1} is Al2 -expanding )

end;
existence

ex b

( b

proof end;

definition

let Al, Al2 be QC-alphabet ;

let P be Subset of (CQC-WFF Al);

end;
let P be Subset of (CQC-WFF Al);

attr P is Al2 -Consistent means :: QC_TRANS:def 2

for S being Subset of (CQC-WFF Al2) st P = S holds

S is Consistent ;

for S being Subset of (CQC-WFF Al2) st P = S holds

S is Consistent ;

:: deftheorem defines -Consistent QC_TRANS:def 2 :

for Al, Al2 being QC-alphabet

for P being Subset of (CQC-WFF Al) holds

( P is Al2 -Consistent iff for S being Subset of (CQC-WFF Al2) st P = S holds

S is Consistent );

for Al, Al2 being QC-alphabet

for P being Subset of (CQC-WFF Al) holds

( P is Al2 -Consistent iff for S being Subset of (CQC-WFF Al2) st P = S holds

S is Consistent );

registration

let Al be QC-alphabet ;

existence

ex b_{1} being Subset of (CQC-WFF Al) st

( not b_{1} is empty & b_{1} is Consistent )

end;
existence

ex b

( not b

proof end;

registration

let Al be QC-alphabet ;

coherence

for b_{1} being Subset of (CQC-WFF Al) st b_{1} is Consistent holds

b_{1} is Al -Consistent
;

coherence

for b_{1} being Subset of (CQC-WFF Al) st b_{1} is Al -Consistent holds

b_{1} is Consistent
;

end;
coherence

for b

b

coherence

for b

b

theorem Th1: :: QC_TRANS:1

for Al being QC-alphabet

for k being Nat

for l being CQC-variable_list of k,Al

for P being QC-pred_symbol of k,Al holds the_arity_of P = len l

for k being Nat

for l being CQC-variable_list of k,Al

for P being QC-pred_symbol of k,Al holds the_arity_of P = len l

proof end;

theorem Th2: :: QC_TRANS:2

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet holds QC-symbols Al c= QC-symbols Al2

for Al2 being b

proof end;

theorem Th3: :: QC_TRANS:3

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet holds QC-pred_symbols Al c= QC-pred_symbols Al2

for Al2 being b

proof end;

theorem Th4: :: QC_TRANS:4

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet holds bound_QC-variables Al c= bound_QC-variables Al2

for Al2 being b

proof end;

theorem Th5: :: QC_TRANS:5

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for k being Nat

for l being CQC-variable_list of k,Al holds l is CQC-variable_list of k,Al2

for Al2 being b

for k being Nat

for l being CQC-variable_list of k,Al holds l is CQC-variable_list of k,Al2

proof end;

theorem Th6: :: QC_TRANS:6

for Al being QC-alphabet

for k being Nat

for P being QC-pred_symbol of k,Al

for Al2 being b_{1} -expanding QC-alphabet holds P is QC-pred_symbol of k,Al2

for k being Nat

for P being QC-pred_symbol of k,Al

for Al2 being b

proof end;

theorem Th7: :: QC_TRANS:7

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for p being Element of CQC-WFF Al holds p is Element of CQC-WFF Al2

for Al2 being b

for p being Element of CQC-WFF Al holds p is Element of CQC-WFF Al2

proof end;

definition

let Al be QC-alphabet ;

let Al2 be Al -expanding QC-alphabet ;

let p be Element of CQC-WFF Al;

coherence

p is Element of CQC-WFF Al2 by Th7;

end;
let Al2 be Al -expanding QC-alphabet ;

let p be Element of CQC-WFF Al;

coherence

p is Element of CQC-WFF Al2 by Th7;

:: deftheorem defines -Cast QC_TRANS:def 3 :

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for p being Element of CQC-WFF Al holds Al2 -Cast p = p;

for Al being QC-alphabet

for Al2 being b

for p being Element of CQC-WFF Al holds Al2 -Cast p = p;

definition

let Al be QC-alphabet ;

let Al2 be Al -expanding QC-alphabet ;

let x be bound_QC-variable of Al;

coherence

x is bound_QC-variable of Al2 by Th4, TARSKI:def 3;

end;
let Al2 be Al -expanding QC-alphabet ;

let x be bound_QC-variable of Al;

coherence

x is bound_QC-variable of Al2 by Th4, TARSKI:def 3;

:: deftheorem defines -Cast QC_TRANS:def 4 :

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for x being bound_QC-variable of Al holds Al2 -Cast x = x;

for Al being QC-alphabet

for Al2 being b

for x being bound_QC-variable of Al holds Al2 -Cast x = x;

definition

let Al be QC-alphabet ;

let Al2 be Al -expanding QC-alphabet ;

let k be Nat;

let P be QC-pred_symbol of k,Al;

coherence

P is QC-pred_symbol of k,Al2 by Th6;

end;
let Al2 be Al -expanding QC-alphabet ;

let k be Nat;

let P be QC-pred_symbol of k,Al;

coherence

P is QC-pred_symbol of k,Al2 by Th6;

:: deftheorem defines -Cast QC_TRANS:def 5 :

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for k being Nat

for P being QC-pred_symbol of k,Al holds Al2 -Cast P = P;

for Al being QC-alphabet

for Al2 being b

for k being Nat

for P being QC-pred_symbol of k,Al holds Al2 -Cast P = P;

definition

let Al be QC-alphabet ;

let Al2 be Al -expanding QC-alphabet ;

let k be Nat;

let l be CQC-variable_list of k,Al;

coherence

l is CQC-variable_list of k,Al2 by Th5;

end;
let Al2 be Al -expanding QC-alphabet ;

let k be Nat;

let l be CQC-variable_list of k,Al;

coherence

l is CQC-variable_list of k,Al2 by Th5;

:: deftheorem defines -Cast QC_TRANS:def 6 :

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for k being Nat

for l being CQC-variable_list of k,Al holds Al2 -Cast l = l;

for Al being QC-alphabet

for Al2 being b

for k being Nat

for l being CQC-variable_list of k,Al holds Al2 -Cast l = l;

theorem Th8: :: QC_TRANS:8

for Al being QC-alphabet

for k being Nat

for p, r being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al

for Al2 being b_{1} -expanding QC-alphabet holds

( Al2 -Cast (VERUM Al) = VERUM Al2 & Al2 -Cast (P ! l) = (Al2 -Cast P) ! (Al2 -Cast l) & Al2 -Cast ('not' p) = 'not' (Al2 -Cast p) & Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) & Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) )

for k being Nat

for p, r being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al

for Al2 being b

( Al2 -Cast (VERUM Al) = VERUM Al2 & Al2 -Cast (P ! l) = (Al2 -Cast P) ! (Al2 -Cast l) & Al2 -Cast ('not' p) = 'not' (Al2 -Cast p) & Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) & Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) )

proof end;

theorem Th9: :: QC_TRANS:9

for Al being QC-alphabet

for r being Element of CQC-WFF Al

for A being non empty set

for Al2 being b_{1} -expanding QC-alphabet

for J2 being interpretation of Al2,A

for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

for r being Element of CQC-WFF Al

for A being non empty set

for Al2 being b

for J2 being interpretation of Al2,A

for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

proof end;

theorem :: QC_TRANS:10

for Al being QC-alphabet

for PHI being Consistent Subset of (CQC-WFF Al)

for Al2 being b_{1} -expanding QC-alphabet

for THETA being Subset of (CQC-WFF Al2) st PHI c= THETA holds

for A2 being non empty set

for J2 being interpretation of Al2,A2

for v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA holds

ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI

for PHI being Consistent Subset of (CQC-WFF Al)

for Al2 being b

for THETA being Subset of (CQC-WFF Al2) st PHI c= THETA holds

for A2 being non empty set

for J2 being interpretation of Al2,A2

for v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA holds

ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI

proof end;

theorem Th11: :: QC_TRANS:11

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for f being FinSequence of CQC-WFF Al2

for g being FinSequence of CQC-WFF Al st f = g holds

( Ant f = Ant g & Suc f = Suc g )

for Al2 being b

for f being FinSequence of CQC-WFF Al2

for g being FinSequence of CQC-WFF Al st f = g holds

( Ant f = Ant g & Suc f = Suc g )

proof end;

theorem Th12: :: QC_TRANS:12

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p)

for Al2 being b

for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p)

proof end;

theorem Th13: :: QC_TRANS:13

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for p2 being Element of CQC-WFF Al2

for S being CQC_Substitution of Al

for S2 being CQC_Substitution of Al2

for x2 being bound_QC-variable of Al2

for x being bound_QC-variable of Al

for p being Element of CQC-WFF Al st p = p2 & S = S2 & x = x2 holds

RestrictSub (x,p,S) = RestrictSub (x2,p2,S2)

for Al2 being b

for p2 being Element of CQC-WFF Al2

for S being CQC_Substitution of Al

for S2 being CQC_Substitution of Al2

for x2 being bound_QC-variable of Al2

for x being bound_QC-variable of Al

for p being Element of CQC-WFF Al st p = p2 & S = S2 & x = x2 holds

RestrictSub (x,p,S) = RestrictSub (x2,p2,S2)

proof end;

theorem Th14: :: QC_TRANS:14

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for p2 being Element of CQC-WFF Al2

for S being finite CQC_Substitution of Al

for S2 being finite CQC_Substitution of Al2

for p being Element of CQC-WFF Al st S = S2 & p = p2 holds

upVar (S,p) = upVar (S2,p2)

for Al2 being b

for p2 being Element of CQC-WFF Al2

for S being finite CQC_Substitution of Al

for S2 being finite CQC_Substitution of Al2

for p being Element of CQC-WFF Al st S = S2 & p = p2 holds

upVar (S,p) = upVar (S2,p2)

proof end;

theorem Th15: :: QC_TRANS:15

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for p2 being Element of CQC-WFF Al2

for S being CQC_Substitution of Al

for S2 being CQC_Substitution of Al2

for x2 being bound_QC-variable of Al2

for x being bound_QC-variable of Al

for p being Element of CQC-WFF Al st p = p2 & S = S2 & x = x2 holds

ExpandSub (x,p,(RestrictSub (x,(All (x,p)),S))) = ExpandSub (x2,p2,(RestrictSub (x2,(All (x2,p2)),S2)))

for Al2 being b

for p2 being Element of CQC-WFF Al2

for S being CQC_Substitution of Al

for S2 being CQC_Substitution of Al2

for x2 being bound_QC-variable of Al2

for x being bound_QC-variable of Al

for p being Element of CQC-WFF Al st p = p2 & S = S2 & x = x2 holds

ExpandSub (x,p,(RestrictSub (x,(All (x,p)),S))) = ExpandSub (x2,p2,(RestrictSub (x2,(All (x2,p2)),S2)))

proof end;

theorem Th16: :: QC_TRANS:16

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for Z being Element of CQC-Sub-WFF Al

for Z2 being Element of CQC-Sub-WFF Al2 st Z `1 is universal & Z2 `1 is universal & bound_in (Z `1) = bound_in (Z2 `1) & the_scope_of (Z `1) = the_scope_of (Z2 `1) & Z = Z2 holds

S_Bound (@ Z) = S_Bound (@ Z2)

for Al2 being b

for Z being Element of CQC-Sub-WFF Al

for Z2 being Element of CQC-Sub-WFF Al2 st Z `1 is universal & Z2 `1 is universal & bound_in (Z `1) = bound_in (Z2 `1) & the_scope_of (Z `1) = the_scope_of (Z2 `1) & Z = Z2 holds

S_Bound (@ Z) = S_Bound (@ Z2)

proof end;

theorem Th17: :: QC_TRANS:17

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for p2 being Element of CQC-WFF Al2

for x2, y2 being bound_QC-variable of Al2

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al st p = p2 & x = x2 & y = y2 holds

p . (x,y) = p2 . (x2,y2)

for Al2 being b

for p2 being Element of CQC-WFF Al2

for x2, y2 being bound_QC-variable of Al2

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al st p = p2 & x = x2 & y = y2 holds

p . (x,y) = p2 . (x2,y2)

proof end;

theorem Th18: :: QC_TRANS:18

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for PHI being Consistent Subset of (CQC-WFF Al2) st PHI is Subset of (CQC-WFF Al) holds

PHI is Al -Consistent

for Al2 being b

for PHI being Consistent Subset of (CQC-WFF Al2) st PHI is Subset of (CQC-WFF Al) holds

PHI is Al -Consistent

proof end;

theorem Th19: :: QC_TRANS:19

for Al being QC-alphabet

for p being Element of CQC-WFF Al ex Al1 being countable QC-alphabet st

( p is Element of CQC-WFF Al1 & Al is Al1 -expanding )

for p being Element of CQC-WFF Al ex Al1 being countable QC-alphabet st

( p is Element of CQC-WFF Al1 & Al is Al1 -expanding )

proof end;

theorem Th20: :: QC_TRANS:20

for Al being QC-alphabet

for PHI being finite Subset of (CQC-WFF Al) ex Al1 being countable QC-alphabet st

( PHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding )

for PHI being finite Subset of (CQC-WFF Al) ex Al1 being countable QC-alphabet st

( PHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding )

proof end;

registration

let Al be QC-alphabet ;

let PHI be finite Subset of (CQC-WFF Al);

coherence

still_not-bound_in PHI is finite

end;
let PHI be finite Subset of (CQC-WFF Al);

coherence

still_not-bound_in PHI is finite

proof end;

theorem Th21: :: QC_TRANS:21

for Al being QC-alphabet

for PHI being Consistent Subset of (CQC-WFF Al)

for Al2 being b_{1} -expanding QC-alphabet

for THETA being Subset of (CQC-WFF Al2) st PHI = THETA holds

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

for PHI being Consistent Subset of (CQC-WFF Al)

for Al2 being b

for THETA being Subset of (CQC-WFF Al2) st PHI = THETA holds

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

proof end;

theorem Th22: :: QC_TRANS:22

for Al being QC-alphabet

for PHI being Consistent Subset of (CQC-WFF Al)

for CHI being Subset of (CQC-WFF Al) st CHI c= PHI holds

CHI is Consistent

for PHI being Consistent Subset of (CQC-WFF Al)

for CHI being Subset of (CQC-WFF Al) st CHI c= PHI holds

CHI is Consistent

proof end;

theorem :: QC_TRANS:23

for Al being QC-alphabet

for PHI being Consistent Subset of (CQC-WFF Al)

for Al2 being b_{1} -expanding QC-alphabet holds PHI is Al2 -Consistent

for PHI being Consistent Subset of (CQC-WFF Al)

for Al2 being b

proof end;