:: CALCUL_2 semantic presentation

definition

let m, n be natural number ;
func seq m,n -> set equals :: CALCUL_2:def 1
{ k where k is Nat : ( 1 + m <= k & k <= n + m ) } ;
coherence ;

end;

:: deftheorem defines seq CALCUL_2:def 1 :

definition

let m, n be natural number ;
:: original: seq
redefine func seq m,n -> Subset of NAT ;
coherence

proof end;

end;

theorem Th1: :: CALCUL_2:1

for c, a, b being natural number holds
( c in seq a,b iff ( 1 + a <= c & c <= b + a ) )

proof end;

theorem Th2: :: CALCUL_2:2

for a being natural number holds seq a,0 = {}

proof end;

theorem Th3: :: CALCUL_2:3

for b, a being natural number holds
( b = 0 or b + a in seq a,b )

proof end;

theorem Th4: :: CALCUL_2:4

for b1, b2, a being natural number holds
( b1 <= b2 iff seq a,b1 c= seq a,b2 )

proof end;

theorem Th5: :: CALCUL_2:5

for a, b being natural number holds (seq a,b) \/ {((a + b) + 1)} = seq a,(b + 1)

proof end;

theorem Th6: :: CALCUL_2:6

for m, n being Nat holds seq m,n,n are_equipotent

proof end;

registration

let m, n be Nat;
cluster seq m,n -> finite ;
coherence

proof end;

end;

registration

let f be FinSequence of CQC-WFF ;
cluster Card f -> finite ;
coherence by CARD_1:69;

end;

theorem Th7: :: CALCUL_2:7

for m, n being Nat holds seq m,n c= Seg (m + n)

proof end;

theorem :: CALCUL_2:8

for n, m being Nat holds Seg n misses seq n,m

proof end;

theorem :: CALCUL_2:9

for f, g being FinSequence holds Seg (len (f ^ g)) = (Seg (len f)) \/ (seq (len f),(len g))

proof end;

theorem Th10: :: CALCUL_2:10

for g, f being FinSequence of CQC-WFF holds len (Sgm (seq (len g),(len f))) = len f

proof end;

theorem Th11: :: CALCUL_2:11

for g, f being FinSequence of CQC-WFF holds dom (Sgm (seq (len g),(len f))) = dom f

proof end;

theorem Th12: :: CALCUL_2:12

for g, f being FinSequence of CQC-WFF holds rng (Sgm (seq (len g),(len f))) = seq (len g),(len f)

proof end;

theorem Th13: :: CALCUL_2:13

for i being Nat
for g, f being FinSequence of CQC-WFF st i in dom (Sgm (seq (len g),(len f))) holds
(Sgm (seq (len g),(len f))) . i = (len g) + i

proof end;

theorem Th14: :: CALCUL_2:14

for g, f being FinSequence of CQC-WFF holds seq (len g),(len f) c= dom (g ^ f)

proof end;

theorem Th15: :: CALCUL_2:15

for g, f being FinSequence of CQC-WFF holds dom ((g ^ f) | (seq (len g),(len f))) = seq (len g),(len f)

proof end;

theorem Th16: :: CALCUL_2:16

for g, f being FinSequence of CQC-WFF holds Seq ((g ^ f) | (seq (len g),(len f))) = (Sgm (seq (len g),(len f))) * (g ^ f)

proof end;

theorem Th17: :: CALCUL_2:17

for g, f being FinSequence of CQC-WFF holds dom (Seq ((g ^ f) | (seq (len g),(len f)))) = dom f

proof end;

theorem Th18: :: CALCUL_2:18

for f, g being FinSequence of CQC-WFF holds f is_Subsequence_of g ^ f

proof end;

definition

let D be non empty set ;
let f be FinSequence of D;
let P be Permutation of dom f;
func Per f,P -> FinSequence of D equals :: CALCUL_2:def 2
P * f;
coherence

proof end;

end;

:: deftheorem defines Per CALCUL_2:def 2 :

theorem Th19: :: CALCUL_2:19

for f being FinSequence of CQC-WFF
for P being Permutation of dom f holds dom (Per f,P) = dom f

proof end;

theorem Th20: :: CALCUL_2:20

for p being Element of CQC-WFF
for f, g being FinSequence of CQC-WFF st |- f ^ <*p*> holds
|- (g ^ f) ^ <*p*>

proof end;

definition

let f be FinSequence of CQC-WFF ;
func Begin f -> Element of CQC-WFF means :Def3: :: CALCUL_2:def 3
it = f . 1 if 1 <= len f
otherwise it = VERUM ;
existence

proof end;

uniqueness ;
consistency ;

end;

:: deftheorem Def3 defines Begin CALCUL_2:def 3 :

definition

let f be FinSequence of CQC-WFF ;
assume A1: 1 <= len f ;
func Impl f -> Element of CQC-WFF means :Def4: :: CALCUL_2:def 4
ex F being FinSequence of CQC-WFF st
( it = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds
ex p, q being Element of CQC-WFF st
( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Impl CALCUL_2:def 4 :

theorem Th21: :: CALCUL_2:21

for p being Element of CQC-WFF
for f being FinSequence of CQC-WFF holds |- (f ^ <*p*>) ^ <*p*>

proof end;

theorem Th22: :: CALCUL_2:22

for p, q being Element of CQC-WFF
for f being FinSequence of CQC-WFF st |- f ^ <*(p '&' q)*> holds
|- f ^ <*p*>

proof end;

theorem Th23: :: CALCUL_2:23

for p, q being Element of CQC-WFF
for f being FinSequence of CQC-WFF st |- f ^ <*(p '&' q)*> holds
|- f ^ <*q*>

proof end;

theorem Th24: :: CALCUL_2:24

for p, q being Element of CQC-WFF
for f being FinSequence of CQC-WFF st |- f ^ <*p*> & |- (f ^ <*p*>) ^ <*q*> holds
|- f ^ <*q*>

proof end;

theorem Th25: :: CALCUL_2:25

for p, q being Element of CQC-WFF
for f being FinSequence of CQC-WFF st |- f ^ <*p*> & |- f ^ <*('not' p)*> holds
|- f ^ <*q*>

proof end;

theorem Th26: :: CALCUL_2:26

for p, q being Element of CQC-WFF
for f being FinSequence of CQC-WFF st |- (f ^ <*p*>) ^ <*q*> & |- (f ^ <*('not' p)*>) ^ <*q*> holds
|- f ^ <*q*>

proof end;

theorem Th27: :: CALCUL_2:27

for p, q being Element of CQC-WFF
for f being FinSequence of CQC-WFF st |- (f ^ <*p*>) ^ <*q*> holds
|- f ^ <*(p => q)*>

proof end;

theorem Th28: :: CALCUL_2:28

for g, f being FinSequence of CQC-WFF st 1 <= len g & |- f ^ g holds
|- f ^ <*(Impl (Rev g))*>

proof end;

theorem Th29: :: CALCUL_2:29

for p being Element of CQC-WFF
for f being FinSequence of CQC-WFF
for P being Permutation of dom f st |- (Per f,P) ^ <*(Impl (Rev (f ^ <*p*>)))*> holds
|- (Per f,P) ^ <*p*>

proof end;

theorem :: CALCUL_2:30

for p being Element of CQC-WFF
for f being FinSequence of CQC-WFF
for P being Permutation of dom f st |- f ^ <*p*> holds
|- (Per f,P) ^ <*p*>

proof end;

notation

let n be Nat;
let c be set ;
synonym IdFinS c,n for n |-> c;

end;

theorem Th31: :: CALCUL_2:31

for n being Nat
for c being set st 1 <= n holds
rng (IdFinS c,n) = rng <*c*>

proof end;

definition

let D be non empty set ;
let n be Nat;
let p be Element of D;
:: original: IdFinS
redefine func IdFinS p,n -> FinSequence of D;
coherence

proof end;

end;

theorem :: CALCUL_2:32

for p, q being Element of CQC-WFF
for n being Nat
for f being FinSequence of CQC-WFF st 1 <= n & |- (f ^ (IdFinS p,n)) ^ <*q*> holds
|- (f ^ <*p*>) ^ <*q*>

proof end;