let A be QC-alphabet ; :: thesis: for k being Nat
for l being QC-variable_list of k,A holds
( l is CQC-variable_list of k,A iff ( { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) )
let k be Nat; :: thesis: for l being QC-variable_list of k,A holds
( l is CQC-variable_list of k,A iff ( { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) )
let l be QC-variable_list of k,A; :: thesis: ( l is CQC-variable_list of k,A iff ( { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) )
set FR = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } ;
set FI = { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } ;
thus ( l is CQC-variable_list of k,A implies ( { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) ) :: thesis: ( { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} implies l is CQC-variable_list of k,A )
proof
assume l is CQC-variable_list of k,A ; :: thesis: ( { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} )
then reconsider l = l as CQC-variable_list of k,A ;
now :: thesis: not { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } <> {}
set x = the Element of { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } ;
assume { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } <> {} ; :: thesis: contradiction
then the Element of { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } ;
then consider i being Nat such that
the Element of { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = l . i and
A1: ( 1 <= i & i <= len l ) and
A2: l . i in free_QC-variables A ;
i in dom l by A1, FINSEQ_3:25;
then ( rng l c= bound_QC-variables A & l . i in rng l ) by FUNCT_1:def 3, RELAT_1:def 19;
hence contradiction by A2, QC_LANG3:34; :: thesis: verum
end;
hence { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} ; :: thesis: { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {}
now :: thesis: not { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } <> {}
set x = the Element of { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } ;
assume { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } <> {} ; :: thesis: contradiction
then the Element of { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } in { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } ;
then consider i being Nat such that
the Element of { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = l . i and
A3: ( 1 <= i & i <= len l ) and
A4: l . i in fixed_QC-variables A ;
i in dom l by A3, FINSEQ_3:25;
then ( rng l c= bound_QC-variables A & l . i in rng l ) by FUNCT_1:def 3, RELAT_1:def 19;
hence contradiction by A4, QC_LANG3:33; :: thesis: verum
end;
hence { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ; :: thesis: verum
end;
assume that
A5: { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} and
A6: { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ; :: thesis: l is CQC-variable_list of k,A
l is bound_QC-variables A -valued
proof
let x be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not x in rng l or x in bound_QC-variables A )
A7: rng l c= QC-variables A by FINSEQ_1:def 4;
assume x in rng l ; :: thesis: x in bound_QC-variables A
then consider i being object such that
A8: i in dom l and
A9: l . i = x by FUNCT_1:def 3;
reconsider i = i as Nat by A8;
A10: ( 1 <= i & i <= len l ) by A8, FINSEQ_3:25;
A11: now :: thesis: not x in fixed_QC-variables A
assume x in fixed_QC-variables A ; :: thesis: contradiction
then x in { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } by A9, A10;
hence contradiction by A6; :: thesis: verum
end;
A12: now :: thesis: not x in free_QC-variables A
assume x in free_QC-variables A ; :: thesis: contradiction
then x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } by A9, A10;
hence contradiction by A5; :: thesis: verum
end;
l . i in rng l by A8, FUNCT_1:def 3;
hence x in bound_QC-variables A by A9, A7, A11, A12, Th1; :: thesis: verum
end;
hence l is CQC-variable_list of k,A ; :: thesis: verum