| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 910 B |
|
Quelle fsq.pvs Sprache: PVS |
|||||||||
|
fsq[T: TYPE]: THEORY
%------------------------------------------------------------------------ % % This theory is scaffolding for the "fseqs" finite sequences theory % %------------------------------------------------------------------------ BEGIN x,y : VAR T fsq: TYPE = [# length: nat, seq: [nat -> T] #] cnvfsq(fs: fsq): MACRO [nat -> T] = fs`seq; CONVERSION cnvfsq; CONVERSION- finseq_appl; %% turn off prelude finseq conversion l(f: fsq): MACRO nat = f`length seqn(f: fsq): MACRO [nat -> T]= f`seq %% not empty fseqs ne_fsq: TYPE = {s: fsq | length(s) > 0} in?(x: T, s: fsq): bool = (EXISTS (ii: below(length(s))): x = seq(s)(ii)) fsq1(t:T): fsq = (# length := 1, seq := (LAMBDA (n: nat): t) #) const_fsq(n: nat,c:T): fsq = (# length := n, seq := (LAMBDA (n: nat): c) #) END fsq ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
