let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for F1, F2 being Function of (QC-WFF A),(QC-WFF A) st ( for q being Element of QC-WFF A holds
( F1 . (VERUM A) = VERUM A & ( q is atomic implies F1 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F1 . q = 'not' (F1 . (the_argument_of q)) ) & ( q is conjunctive implies F1 . q = (F1 . (the_left_argument_of q)) '&' (F1 . (the_right_argument_of q)) ) & ( q is universal implies F1 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F1 . (the_scope_of q))))) ) ) ) & ( for q being Element of QC-WFF A holds
( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F2 . q = 'not' (F2 . (the_argument_of q)) ) & ( q is conjunctive implies F2 . q = (F2 . (the_left_argument_of q)) '&' (F2 . (the_right_argument_of q)) ) & ( q is universal implies F2 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F2 . (the_scope_of q))))) ) ) ) holds
F1 = F2
let x be bound_QC-variable of A; :: thesis: for F1, F2 being Function of (QC-WFF A),(QC-WFF A) st ( for q being Element of QC-WFF A holds
( F1 . (VERUM A) = VERUM A & ( q is atomic implies F1 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F1 . q = 'not' (F1 . (the_argument_of q)) ) & ( q is conjunctive implies F1 . q = (F1 . (the_left_argument_of q)) '&' (F1 . (the_right_argument_of q)) ) & ( q is universal implies F1 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F1 . (the_scope_of q))))) ) ) ) & ( for q being Element of QC-WFF A holds
( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F2 . q = 'not' (F2 . (the_argument_of q)) ) & ( q is conjunctive implies F2 . q = (F2 . (the_left_argument_of q)) '&' (F2 . (the_right_argument_of q)) ) & ( q is universal implies F2 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F2 . (the_scope_of q))))) ) ) ) holds
F1 = F2
deffunc H₁( Element of QC-WFF A, Element of QC-WFF A) -> Element of QC-WFF A = $1 '&' $2;
deffunc H₂( Element of QC-WFF A) -> Element of QC-WFF A = 'not' $1;
let F1, F2 be Function of (QC-WFF A),(QC-WFF A); :: thesis: ( ( for q being Element of QC-WFF A holds
( F1 . (VERUM A) = VERUM A & ( q is atomic implies F1 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F1 . q = 'not' (F1 . (the_argument_of q)) ) & ( q is conjunctive implies F1 . q = (F1 . (the_left_argument_of q)) '&' (F1 . (the_right_argument_of q)) ) & ( q is universal implies F1 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F1 . (the_scope_of q))))) ) ) ) & ( for q being Element of QC-WFF A holds
( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F2 . q = 'not' (F2 . (the_argument_of q)) ) & ( q is conjunctive implies F2 . q = (F2 . (the_left_argument_of q)) '&' (F2 . (the_right_argument_of q)) ) & ( q is universal implies F2 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F2 . (the_scope_of q))))) ) ) ) implies F1 = F2 )
deffunc H₃( Element of QC-WFF A) -> Element of QC-WFF A = (the_pred_symbol_of $1) ! (Subst ((the_arguments_of $1),((A a. 0) .--> x)));
deffunc H₄( Element of QC-WFF A, Element of QC-WFF A) -> Element of QC-WFF A = IFEQ ((bound_in $1),x,$1,(All ((bound_in $1),$2)));
assume for q being Element of QC-WFF A holds
( F1 . (VERUM A) = VERUM A & ( q is atomic implies F1 . q = H₃(q) ) & ( q is negative implies F1 . q = 'not' (F1 . (the_argument_of q)) ) & ( q is conjunctive implies F1 . q = (F1 . (the_left_argument_of q)) '&' (F1 . (the_right_argument_of q)) ) & ( q is universal implies F1 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F1 . (the_scope_of q))))) ) ) ; :: thesis: ( ex q being Element of QC-WFF A st
( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F2 . q = 'not' (F2 . (the_argument_of q)) ) & ( q is conjunctive implies F2 . q = (F2 . (the_left_argument_of q)) '&' (F2 . (the_right_argument_of q)) ) implies ( q is universal & not F2 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F2 . (the_scope_of q))))) ) ) or F1 = F2 )
then A1: for p, d1, d2 being Element of QC-WFF A holds
( ( p = VERUM A implies F1 . p = VERUM A ) & ( p is atomic implies F1 . p = H₃(p) ) & ( p is negative & d1 = F1 . (the_argument_of p) implies F1 . p = H₂(d1) ) & ( p is conjunctive & d1 = F1 . (the_left_argument_of p) & d2 = F1 . (the_right_argument_of p) implies F1 . p = H₁(d1,d2) ) & ( p is universal & d1 = F1 . (the_scope_of p) implies F1 . p = H₄(p,d1) ) ) ;
assume for q being Element of QC-WFF A holds
( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F2 . q = 'not' (F2 . (the_argument_of q)) ) & ( q is conjunctive implies F2 . q = (F2 . (the_left_argument_of q)) '&' (F2 . (the_right_argument_of q)) ) & ( q is universal implies F2 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F2 . (the_scope_of q))))) ) ) ; :: thesis: F1 = F2
then A2: for p, d1, d2 being Element of QC-WFF A holds
( ( p = VERUM A implies F2 . p = VERUM A ) & ( p is atomic implies F2 . p = H₃(p) ) & ( p is negative & d1 = F2 . (the_argument_of p) implies F2 . p = H₂(d1) ) & ( p is conjunctive & d1 = F2 . (the_left_argument_of p) & d2 = F2 . (the_right_argument_of p) implies F2 . p = H₁(d1,d2) ) & ( p is universal & d1 = F2 . (the_scope_of p) implies F2 . p = H₄(p,d1) ) ) ;
thus F1 = F2 from QC_LANG3:sch 1(A1, A2); :: thesis: verum