begin
scheme
SeqLambda1C{
F1()
-> Nat,
F2()
-> non
empty set ,
P1[
set ],
F3(
set )
-> set ,
F4(
set )
-> set } :
ex
p being
FinSequence of
F2() st
(
len p = F1() & ( for
i being
Nat st
i in Seg F1() holds
( (
P1[
i] implies
p . i = F3(
i) ) & (
P1[
i] implies
p . i = F4(
i) ) ) ) )
provided
A1:
for
i being
Nat st
i in Seg F1() holds
( (
P1[
i] implies
F3(
i)
in F2() ) & (
P1[
i] implies
F4(
i)
in F2() ) )
theorem
canceled;
theorem Th2:
theorem
theorem Th4:
begin
definition
let X be
set ;
let p be
FinSequence of
bool X;
let q be
FinSequence of
BOOLEAN ;
func MergeSequence p,
q -> FinSequence of
bool X means :
Def1:
(
len it = len p & ( for
i being
Nat st
i in dom p holds
it . i = IFEQ (q . i),
TRUE ,
(p . i),
(X \ (p . i)) ) );
existence
ex b1 being FinSequence of bool X st
( len b1 = len p & ( for i being Nat st i in dom p holds
b1 . i = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) ) )
uniqueness
for b1, b2 being FinSequence of bool X st len b1 = len p & ( for i being Nat st i in dom p holds
b1 . i = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) ) & len b2 = len p & ( for i being Nat st i in dom p holds
b2 . i = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) ) holds
b1 = b2
end;
:: deftheorem Def1 defines MergeSequence YELLOW15:def 1 :
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem
theorem
theorem
theorem
theorem
theorem
for
X being
set for
x,
y,
z being
Subset of
X for
q being
FinSequence of
BOOLEAN holds
( (
q . 1
= TRUE implies
(MergeSequence <*x,y,z*>,q) . 1
= x ) & (
q . 1
= FALSE implies
(MergeSequence <*x,y,z*>,q) . 1
= X \ x ) & (
q . 2
= TRUE implies
(MergeSequence <*x,y,z*>,q) . 2
= y ) & (
q . 2
= FALSE implies
(MergeSequence <*x,y,z*>,q) . 2
= X \ y ) & (
q . 3
= TRUE implies
(MergeSequence <*x,y,z*>,q) . 3
= z ) & (
q . 3
= FALSE implies
(MergeSequence <*x,y,z*>,q) . 3
= X \ z ) )
theorem Th16:
:: deftheorem Def2 defines Components YELLOW15:def 2 :
theorem Th17:
theorem
theorem Th19:
theorem Th20:
:: deftheorem Def3 defines in_general_position YELLOW15:def 3 :
theorem
theorem
theorem
begin
theorem Th24:
theorem Th25:
theorem
theorem
theorem
theorem
theorem Th30:
theorem
theorem