:: CALCUL_2 semantic presentation

definition

let c₁, c₂ be natural number ;
func seq c₁,c₂ -> set equals :: CALCUL_2:def 1
{ b₁ where B is Nat : ( 1 + a₁ <= b₁ & b₁ <= a₂ + a₁ ) } ;
coherence ;

end;

:: deftheorem Def1 defines seq CALCUL_2:def 1 :

definition

let c₁, c₂ be natural number ;
redefine func seq as seq c₁,c₂ -> Subset of NAT ;
coherence

proof end;

end;

theorem Th1: :: CALCUL_2:1

for b₁, b₂, b₃ being natural number holds
( b₁ in seq b₂,b₃ iff ( 1 + b₂ <= b₁ & b₁ <= b₃ + b₂ ) )

proof end;

theorem Th2: :: CALCUL_2:2

for b₁ being natural number holds seq b₁,0 = {}

proof end;

theorem Th3: :: CALCUL_2:3

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

proof end;

theorem Th4: :: CALCUL_2:4

for b₁, b₂, b₃ being natural number holds
( b₁ <= b₂ iff seq b₃,b₁ c= seq b₃,b₂ )

proof end;

theorem Th5: :: CALCUL_2:5

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

proof end;

theorem Th6: :: CALCUL_2:6

for b₁, b₂ being Nat holds seq b₁,b₂,b₂ are_equipotent

proof end;

registration

let c₁, c₂ be Nat;
cluster seq a₁,a₂ -> finite ;
coherence

proof end;

end;

registration

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

end;

theorem Th7: :: CALCUL_2:7

for b₁, b₂ being Nat holds seq b₁,b₂ c= Seg (b₁ + b₂)

proof end;

theorem Th8: :: CALCUL_2:8

for b₁, b₂ being Nat holds Seg b₁ misses seq b₁,b₂

proof end;

theorem Th9: :: CALCUL_2:9

for b₁, b₂ being FinSequence holds Seg (len (b₁ ^ b₂)) = (Seg (len b₁)) \/ (seq (len b₁),(len b₂))

proof end;

theorem Th10: :: CALCUL_2:10

for b₁, b₂ being FinSequence of CQC-WFF holds len (Sgm (seq (len b₁),(len b₂))) = len b₂

proof end;

theorem Th11: :: CALCUL_2:11

for b₁, b₂ being FinSequence of CQC-WFF holds dom (Sgm (seq (len b₁),(len b₂))) = dom b₂

proof end;

theorem Th12: :: CALCUL_2:12

for b₁, b₂ being FinSequence of CQC-WFF holds rng (Sgm (seq (len b₁),(len b₂))) = seq (len b₁),(len b₂)

proof end;

theorem Th13: :: CALCUL_2:13

for b₁ being Nat
for b₂, b₃ being FinSequence of CQC-WFF st b₁ in dom (Sgm (seq (len b₂),(len b₃))) holds
(Sgm (seq (len b₂),(len b₃))) . b₁ = (len b₂) + b₁

proof end;

theorem Th14: :: CALCUL_2:14

for b₁, b₂ being FinSequence of CQC-WFF holds seq (len b₁),(len b₂) c= dom (b₁ ^ b₂)

proof end;

theorem Th15: :: CALCUL_2:15

for b₁, b₂ being FinSequence of CQC-WFF holds dom ((b₁ ^ b₂) | (seq (len b₁),(len b₂))) = seq (len b₁),(len b₂)

proof end;

theorem Th16: :: CALCUL_2:16

for b₁, b₂ being FinSequence of CQC-WFF holds Seq ((b₁ ^ b₂) | (seq (len b₁),(len b₂))) = (Sgm (seq (len b₁),(len b₂))) * (b₁ ^ b₂)

proof end;

theorem Th17: :: CALCUL_2:17

for b₁, b₂ being FinSequence of CQC-WFF holds dom (Seq ((b₁ ^ b₂) | (seq (len b₁),(len b₂)))) = dom b₂

proof end;

theorem Th18: :: CALCUL_2:18

for b₁, b₂ being FinSequence of CQC-WFF holds b₁ is_Subsequence_of b₂ ^ b₁

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
let c₃ be Permutation of dom c₂;
func Per c₂,c₃ -> FinSequence of a₁ equals :: CALCUL_2:def 2
a₃ * a₂;
coherence

proof end;

end;

:: deftheorem Def2 defines Per CALCUL_2:def 2 :

theorem Th19: :: CALCUL_2:19

for b₁ being FinSequence of CQC-WFF
for b₂ being Permutation of dom b₁ holds dom (Per b₁,b₂) = dom b₁

proof end;

theorem Th20: :: CALCUL_2:20

for b₁ being Element of CQC-WFF
for b₂, b₃ being FinSequence of CQC-WFF st |- b₂ ^ <*b₁*> holds
|- (b₃ ^ b₂) ^ <*b₁*>

proof end;

definition

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

proof end;

uniqueness ;
consistency ;

end;

:: deftheorem Def3 defines Begin CALCUL_2:def 3 :

definition

let c₁ be FinSequence of CQC-WFF ;
assume E20: 1 <= len c₁ ;
func Impl c₁ -> Element of CQC-WFF means :Def4: :: CALCUL_2:def 4
ex b₁ being FinSequence of CQC-WFF st
( a₂ = b₁ . (len a₁) & len b₁ = len a₁ & ( b₁ . 1 = Begin a₁ or len a₁ = 0 ) & ( for b₂ being Nat st 1 <= b₂ & b₂ < len a₁ holds
ex b₃, b₄ being Element of CQC-WFF st
( b₃ = a₁ . (b₂ + 1) & b₄ = b₁ . b₂ & b₁ . (b₂ + 1) = b₃ => b₄ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Impl CALCUL_2:def 4 :

theorem Th21: :: CALCUL_2:21

for b₁ being Element of CQC-WFF
for b₂ being FinSequence of CQC-WFF holds |- (b₂ ^ <*b₁*>) ^ <*b₁*>

proof end;

theorem Th22: :: CALCUL_2:22

for b₁, b₂ being Element of CQC-WFF
for b₃ being FinSequence of CQC-WFF st |- b₃ ^ <*(b₁ '&' b₂)*> holds
|- b₃ ^ <*b₁*>

proof end;

theorem Th23: :: CALCUL_2:23

for b₁, b₂ being Element of CQC-WFF
for b₃ being FinSequence of CQC-WFF st |- b₃ ^ <*(b₁ '&' b₂)*> holds
|- b₃ ^ <*b₂*>

proof end;

theorem Th24: :: CALCUL_2:24

for b₁, b₂ being Element of CQC-WFF
for b₃ being FinSequence of CQC-WFF st |- b₃ ^ <*b₁*> & |- (b₃ ^ <*b₁*>) ^ <*b₂*> holds
|- b₃ ^ <*b₂*>

proof end;

theorem Th25: :: CALCUL_2:25

for b₁, b₂ being Element of CQC-WFF
for b₃ being FinSequence of CQC-WFF st |- b₃ ^ <*b₁*> & |- b₃ ^ <*('not' b₁)*> holds
|- b₃ ^ <*b₂*>

proof end;

theorem Th26: :: CALCUL_2:26

for b₁, b₂ being Element of CQC-WFF
for b₃ being FinSequence of CQC-WFF st |- (b₃ ^ <*b₁*>) ^ <*b₂*> & |- (b₃ ^ <*('not' b₁)*>) ^ <*b₂*> holds
|- b₃ ^ <*b₂*>

proof end;

theorem Th27: :: CALCUL_2:27

for b₁, b₂ being Element of CQC-WFF
for b₃ being FinSequence of CQC-WFF st |- (b₃ ^ <*b₁*>) ^ <*b₂*> holds
|- b₃ ^ <*(b₁ => b₂)*>

proof end;

theorem Th28: :: CALCUL_2:28

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

proof end;

theorem Th29: :: CALCUL_2:29

for b₁ being Element of CQC-WFF
for b₂ being FinSequence of CQC-WFF
for b₃ being Permutation of dom b₂ st |- (Per b₂,b₃) ^ <*(Impl (Rev (b₂ ^ <*b₁*>)))*> holds
|- (Per b₂,b₃) ^ <*b₁*>

proof end;

theorem Th30: :: CALCUL_2:30

for b₁ being Element of CQC-WFF
for b₂ being FinSequence of CQC-WFF
for b₃ being Permutation of dom b₂ st |- b₂ ^ <*b₁*> holds
|- (Per b₂,b₃) ^ <*b₁*>

proof end;

notation

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

end;

theorem Th31: :: CALCUL_2:31

for b₁ being Nat
for b₂ being set st 1 <= b₁ holds
rng (IdFinS b₂,b₁) = rng <*b₂*>

proof end;

definition

let c₁ be non empty set ;
let c₂ be Nat;
let c₃ be Element of c₁;
redefine func IdFinS as IdFinS c₃,c₂ -> FinSequence of a₁;
coherence

proof end;

end;

theorem Th32: :: CALCUL_2:32

for b₁, b₂ being Element of CQC-WFF
for b₃ being Nat
for b₄ being FinSequence of CQC-WFF st 1 <= b₃ & |- (b₄ ^ (IdFinS b₁,b₃)) ^ <*b₂*> holds
|- (b₄ ^ <*b₁*>) ^ <*b₂*>

proof end;