public inbox for git-commits@fedoraproject.org
help / color / mirror / Atom feed
* [rpms/lfsc] rawhide: Orphaned for 6+ weeks
@ 2026-08-04 22:04 Orphaned Packages Process
0 siblings, 0 replies; only message in thread
From: Orphaned Packages Process @ 2026-08-04 22:04 UTC (permalink / raw)
To: git-commits
A new commit has been pushed.
Repo : rpms/lfsc
Branch : rawhide
Commit : e015494b71995a33cd04322f8424ad63ed2bb05c
Author : Orphaned Packages Process <packaging-reports@fedoraproject.org>
Date : 2026-08-04T17:04:33-05:00
Stats : +1/-2985 in 15 file(s)
URL : https://src.fedoraproject.org/rpms/lfsc/c/e015494b71995a33cd04322f8424ad63ed2bb05c?branch=rawhide
Log:
Orphaned for 6+ weeks
---
diff --git a/.gitignore b/.gitignore
deleted file mode 100644
index f27df56..0000000
--- a/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-/lfsc-*.tar.gz
diff --git a/README.md b/README.md
deleted file mode 100644
index 02ee280..0000000
--- a/README.md
+++ /dev/null
@@ -1,5 +0,0 @@
-# lfsc
-
-[LFSC](https://github.com/cvc5/LFSC) is an
-[SMT](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories) proof
-checker.
diff --git a/color_base.plf b/color_base.plf
deleted file mode 100644
index 5734cff..0000000
--- a/color_base.plf
+++ /dev/null
@@ -1,62 +0,0 @@
-(declare color type)
-(declare A color)
-(declare B color)
-
-; formula f is an interpolant for (A,B)
-(declare interpolant (! f formula type))
-
-; input formula f is from "c", where c is A|B
-(declare color_atom (! c color (! f formula type)))
-
-; simplify interpolant
-
-(program simplify_f ((f formula)) formula
- (match f
- ((and f1 f2)
- (let f1' (simplify_f f1)
- (match f1'
- (true (simplify_f f2))
- (false false)
- (default
- (let f2' (simplify_f f2)
- (match f2'
- (true f1')
- (false false)
- (default (and f1' f2'))))))))
- ((or f1 f2)
- (let f1' (simplify_f f1)
- (match f1'
- (true true)
- (false (simplify_f f2))
- (default
- (let f2' (simplify_f f2)
- (match f2'
- (true true)
- (false f1')
- (default (or f1' f2'))))))))
- ((impl f1 f2)
- (let f1' (simplify_f f1)
- (match f1'
- (true (simplify_f f2))
- (false true)
- (default
- (let f2' (simplify_f f2)
- (match f2'
- (true true)
- (false (match f1'
- ((not f1'') f1'')
- (default (not f1'))))
- (default (impl f1' f2'))))))))
- ((not f1)
- (let f1' (simplify_f f1)
- (match f1'
- ((not f1'') f1'')
- (default (not f1')))))
- (default f)))
-
-(declare simplify_interpolant
- (! f formula
- (! f' formula
- (! i (interpolant f)
- (! u (^ (simplify_f f) f')
- (interpolant f'))))))
diff --git a/color_euf.plf b/color_euf.plf
deleted file mode 100644
index 9b0cd10..0000000
--- a/color_euf.plf
+++ /dev/null
@@ -1,103 +0,0 @@
-; side conditions
-
-(program color_mark ((t term) (c color)) bool
- (match t
- ((apply s1 s2 t1 t2)
- (do (color_mark t1 c)
- (color_mark t2 c)))
- (default
- (do (match c
- (A (ifmarked5 t t (markvar5 t)))
- (B (ifmarked6 t t (markvar6 t)))) tt))))
-
-(program color_mark_formula ((f formula) (c color)) bool
- (match f
- ((= s t1 t2) (do (color_mark t1 c) (color_mark t2 c)))
- ((distinct s t1 t2) (do (color_mark t1 c) (color_mark t2 c)))))
-
-(program is_color_marked ((t term) (c color)) bool
- (match t
- ((apply s1 s2 t1 t2)
- (match (is_color_marked t1 c)
- (tt (is_color_marked t2 c))
- (ff ff)))
- (default
- (match c
- (A (ifmarked5 t tt ff))
- (B (ifmarked6 t tt ff))))))
-
-; introduce a color atom
-
-(declare catom_intro
- (! fi formula
- (! c color
- (! f formula
- (! r (^ (color_mark_formula f c) tt)
- (! u' (! a' (color_atom c f)
- (interpolant fi))
- (interpolant fi)))))))
-
-; rules for term colorability
-
-(declare colorable (! c color (! s sort (! t (term s) type))))
-
-; colorable let
-(declare colorable_intro
- (! c color
- (! s sort
- (! t (term s)
- (! f formula
- (! u (colorable c s t)
- (! u' (! v (colorable c s t) (interpolant f))
- (interpolant f))))))))
-
-; introduce a colorable
-
-(declare colorable_base
- (! s sort
- (! c color
- (! t (term s)
- (! r (^ (is_color_marked t c) tt)
- (colorable c s t))))))
-
-(declare colorable_apply
- (! s1 sort
- (! s2 sort
- (! t (term s1)
- (! f (term (arrow s1 s2))
- (! c color
- (! c1 (colorable c s1 t)
- (! c2 (colorable c (arrow s1 s2) f)
- (colorable c s2 (apply s1 s2 f t)))))))))))
-
-; rules for colorable atoms
-
-(declare catom_refl
- (! s sort
- (! t (term s)
- (! c color
- (! c1 (colorable c s t)
- (color_atom c (= s t t)))))))
-
-(declare catom_symm_eq
- (! c color
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! u (color_atom c (= s t1 t2))
- (color_atom c (= s t2 t1))))))))
-
-(declare catom_symm_distinct
- (! c color
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! u (color_atom c (distinct s t1 t2))
- (color_atom c (distinct s t2 t1))))))))
-
-; this is probably not necessary
-;(declare catom_uncolor
-; (! c color
-; (! f formula
-; (! u (color_atom c f)
-; (th_holds f)))))
\ No newline at end of file
diff --git a/dead.package b/dead.package
new file mode 100644
index 0000000..5204a84
--- /dev/null
+++ b/dead.package
@@ -0,0 +1 @@
+Orphaned for 6+ weeks
diff --git a/euf_interpolation.plf b/euf_interpolation.plf
deleted file mode 100644
index 106a447..0000000
--- a/euf_interpolation.plf
+++ /dev/null
@@ -1,287 +0,0 @@
-; f is the B-premise set for A-path t1...t2
-(declare bps_A
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! f formula
- (! fi formula
- type))))))
-
-(declare bps_A_derived
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! f formula
- (! fi formula
- type))))))
-
-; f is the B-premise set for c-ended chain t1...t2
-(declare bps
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! c color
- (! f formula
- (! fi formula
- type)))))))
-
-; f is the partial interpolant for B-chain t1...t2
-(declare pti_B
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! f formula
- type)))))
-
-(declare pti_B_derived
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! f formula
- type)))))
-
-; f is the partial interpolant for the c-ended chain t1...t2
-(declare pti
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! c color
- (! f formula
- type))))))
-
-; bps_A rules
-
-(declare baseA
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! c1 (color_atom A (= s t1 t2))
- (bps_A s t1 t2 true true))))))
-
-(declare simpA
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! t3 (term s)
- (! f formula
- (! fi formula
- (! b (bps_A s t1 t2 f fi)
- (! u (color_atom A (= s t2 t3))
- (bps_A s t1 t3 f fi))))))))))
-
-(declare drvA
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! t3 (term s)
- (! f formula
- (! fi formula
- (! fc formula
- (! fci formula
- (! b (bps_A s t1 t2 f fi)
- (! bc (bps_A_derived s t2 t3 fc fci)
- (! u (colorable A s t3)
- (bps_A s t1 t3 (and f fc) (and fi fci))))))))))))))
-
-(declare congA0
- (! s sort
- (! f (term s)
- (bps_A_derived s f f true true))))
-
-(declare congA
- (! s1 sort
- (! s2 sort
- (! t1 (term s1)
- (! t2 (term s1)
- (! f1 (term (arrow s1 s2))
- (! f2 (term (arrow s1 s2))
- (! c color
- (! f formula
- (! fi formula
- (! fc formula
- (! fci formula
- (! u1 (bps_A_derived (arrow s1 s2) f1 f2 fc fci)
- (! u2 (bps s1 t1 t2 c f fi)
- (bps_A_derived s2 (apply s1 s2 f1 t1) (apply s1 s2 f2 t2) (and fc f) (and fci fi))))))))))))))))
-
-; for optimization
-(declare congA_t
- (! s1 sort
- (! s2 sort
- (! f1 (term (arrow s1 s2))
- (! f2 (term (arrow s1 s2))
- (! fc formula
- (! fci formula
- (! b (bps_A_derived (arrow s1 s2) f1 f2 fc fci)
- (! t (term s1)
- (bps_A_derived s2 (apply s1 s2 f1 t) (apply s1 s2 f2 t) fc fci))))))))))
-
-; bps rules
-
-(declare bps_baseA
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! f formula
- (! fi formula
- (! b (bps_A s t1 t2 f fi)
- (bps s t1 t2 A f fi))))))))
-
-(declare bps_baseB
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! f formula
- (! b (pti_B s t1 t2 f)
- (bps s t1 t2 B (= s t1 t2) f)))))))
-
-(declare bps_appA
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! t3 (term s)
- (! f1 formula
- (! f1i formula
- (! f2 formula
- (! f2i formula
- (! b1 (bps s t1 t2 B f1 f1i)
- (! b2 (bps_A s t2 t3 f2 f2i)
- (bps s t1 t3 A (and f1 f2) (and f1i f2i)))))))))))))
-
-(declare bps_appB
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! t3 (term s)
- (! f1 formula
- (! f1i formula
- (! f2i formula
- (! b1 (bps s t1 t2 A f1 f1i)
- (! b2 (pti_B s t2 t3 f2i)
- (bps s t1 t3 B (and f1 (= s t2 t3)) (and f1i f2i))))))))))))
-
-; rules for B partial interpolants
-
-(declare baseB
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! u (color_atom B (= s t1 t2))
- (pti_B s t1 t2 true))))))
-
-(declare simpB
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! t3 (term s)
- (! f formula
- (! i (pti_B s t1 t2 f)
- (! u (color_atom B (= s t2 t3))
- (pti_B s t1 t3 f)))))))))
-
-(declare drvB
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! t3 (term s)
- (! f formula
- (! fc formula
- (! i (pti_B s t1 t2 f)
- (! u (pti_B_derived s t2 t3 fc)
- (! c (colorable B s t3)
- (pti_B s t1 t3 (and f fc))))))))))))
-
-(declare congB0
- (! s sort
- (! f (term s)
- (pti_B_derived s f f true))))
-
-(declare congB
- (! s1 sort
- (! s2 sort
- (! f1 (term (arrow s1 s2))
- (! f2 (term (arrow s1 s2))
- (! t1 (term s1)
- (! t2 (term s1)
- (! c color
- (! f formula
- (! fc formula
- (! u1 (pti_B_derived (arrow s1 s2) f1 f2 fc)
- (! u2 (pti s1 t1 t2 c f)
- (pti_B_derived s2 (apply s1 s2 f1 t1) (apply s1 s2 f2 t2) (and fc f))))))))))))))
-
-; for optimization
-(declare congB_t
- (! s1 sort
- (! s2 sort
- (! f1 (term (arrow s1 s2))
- (! f2 (term (arrow s1 s2))
- (! fc formula
- (! b (pti_B_derived (arrow s1 s2) f1 f2 fc)
- (! t (term s1)
- (pti_B_derived s2 (apply s1 s2 f1 t) (apply s1 s2 f2 t) fc)))))))))
-
-; rules for partial interpolants
-
-(declare pti_baseA
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! f formula
- (! fi formula
- (! i (bps_A s t1 t2 f fi)
- (pti s t1 t2 A (and (impl f (= s t1 t2)) fi)))))))))
-
-(declare pti_baseB
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! f formula
- (! i (pti_B s t1 t2 f)
- (pti s t1 t2 B f)))))))
-
-(declare pti_appA
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! t3 (term s)
- (! f1 formula
- (! f2 formula
- (! f2i formula
- (! i1 (pti s t1 t2 B f1)
- (! i2 (bps_A s t2 t3 f2 f2i)
- (pti s t1 t3 A (and f1 (and (impl f2 (= s t2 t3)) f2i)))))))))))))
-
-(declare pti_appB
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! t3 (term s)
- (! f1 formula
- (! f2 formula
- (! i1 (pti s t1 t2 A f1)
- (! i2 (pti_B s t2 t3 f2)
- (pti s t1 t3 B (and f1 f2)))))))))))
-
-; rules for interpolants
-
-(declare interpolant_introB
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! c color
- (! f formula
- (! i (pti s t1 t2 c f)
- (! u (color_atom B (distinct s t1 t2))
- (interpolant f)))))))))
-
-(declare interpolant_introA
- (! s sort
- (! t1 (term s)
- (! t2 (term s)
- (! c color
- (! f formula
- (! fi formula
- (! b (bps s t1 t2 c f fi)
- (! u (color_atom A (distinct s t1 t2))
- (interpolant (and fi (not f))))))))))))
\ No newline at end of file
diff --git a/lfsc-map.patch b/lfsc-map.patch
deleted file mode 100644
index 0d5ee75..0000000
--- a/lfsc-map.patch
+++ /dev/null
@@ -1,53 +0,0 @@
---- src/check.cpp.orig 2019-09-09 09:09:42.511584867 -0600
-+++ src/check.cpp 2019-09-09 09:10:28.396752570 -0600
-@@ -33,7 +33,7 @@ std::vector<Expr *> ascHoles;
-
- Trie<pair<Expr *, Expr *> > *symbols = new Trie<pair<Expr *, Expr *> >;
-
--hash_map<string, bool> imports;
-+std::unordered_map<string, bool> imports;
- std::map<SymExpr *, int> mark_map;
- std::vector<std::pair<std::string, std::pair<Expr *, Expr *> > >
- local_sym_names;
---- src/check.h.orig 2019-08-08 13:50:19.000000000 -0600
-+++ src/check.h 2019-09-09 09:09:42.511584867 -0600
-@@ -8,7 +8,7 @@
- #include <stdio.h>
- #include <hash_map>
- #else
--#include <ext/hash_map>
-+#include <unordered_map>
- #endif
-
- #include <cstddef>
-@@ -158,8 +158,8 @@ inline const char *prefix_id(bool skip_w
- typedef std::hash_map<std::string, Expr *> symmap;
- typedef std::hash_map<std::string, SymExpr *> symmap2;
- #else
--typedef __gnu_cxx::hash_map<std::string, Expr *> symmap;
--typedef __gnu_cxx::hash_map<std::string, SymExpr *> symmap2;
-+typedef std::unordered_map<std::string, Expr *> symmap;
-+typedef std::unordered_map<std::string, SymExpr *> symmap2;
- #endif
- extern symmap2 progs;
- extern std::vector<Expr *> ascHoles;
-@@ -171,19 +171,6 @@ extern std::map<SymExpr *, int> mark_map
- extern std::vector<std::pair<std::string, std::pair<Expr *, Expr *> > >
- local_sym_names;
-
--#ifndef _MSC_VER
--namespace __gnu_cxx {
--template <>
--struct hash<std::string>
--{
-- size_t operator()(const std::string &x) const
-- {
-- return hash<const char *>()(x.c_str());
-- }
--};
--} // namespace __gnu_cxx
--#endif
--
- extern Expr *statMpz;
- extern Expr *statMpq;
- extern Expr *statType;
diff --git a/lfsc.spec b/lfsc.spec
deleted file mode 100644
index 8ae1c6a..0000000
--- a/lfsc.spec
+++ /dev/null
@@ -1,221 +0,0 @@
-# NOTE: upstream does not make releases and has no version numbering scheme.
-# We check the code out of git and use the date of the last commit as the
-# version number.
-%global gittag 5a127dbbcf9a0f822768e783dbf892ee90c435d5
-%global shorttag %(cut -b -7 <<< %{gittag})
-
-Name: lfsc
-Version: 0.20230914
-Release: 6%{?dist}
-Summary: SMT proof checker
-
-License: BSD-3-Clause
-URL: https://github.com/cvc5/LFSC
-VCS: git:%{url}.git
-Source0: %{url}/archive/%{gittag}/%{name}-%{shorttag}.tar.gz
-# The next few sources contain commonly used proof definitions
-Source1: http://clc.cs.uiowa.edu/lfsc/euf_interpolation.plf
-Source2: http://clc.cs.uiowa.edu/lfsc/sat.plf
-Source3: http://clc.cs.uiowa.edu/lfsc/smt.plf
-Source4: http://clc.cs.uiowa.edu/lfsc/th_base.plf
-Source5: http://clc.cs.uiowa.edu/lfsc/th_real.plf
-Source6: http://clc.cs.uiowa.edu/lfsc/th_lra.plf
-Source7: http://clc.cs.uiowa.edu/lfsc/th_lra-cvc3.plf
-Source8: http://clc.cs.uiowa.edu/lfsc/color_base.plf
-Source9: http://clc.cs.uiowa.edu/lfsc/color_euf.plf
-# Use std::unordered_map instead of the deprecated __gnu_cxx::hash_map
-Patch: %{name}-map.patch
-
-# See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval
-ExcludeArch: %{ix86}
-
-BuildRequires: cmake
-BuildRequires: flex
-BuildRequires: gcc-c++
-BuildRequires: gmp-devel
-BuildRequires: help2man
-BuildRequires: make
-BuildRequires: python3-devel
-
-%description
-This package contains an SMT proof checker.
-
-%package devel
-Summary: Files needed to compile side conditions
-Requires: %{name}%{?_isa} = %{version}-%{release}
-
-%description devel
-This package contains the files needed to compile a version of %{name} that
-can execute a side condition.
-
-%prep
-%autosetup -p0 -n LFSC-%{gittag}
-
-%conf
-# We want to know about use of deprecated interfaces
-sed -i '/Wno-deprecated/d' CMakeLists.txt
-
-# Build a shared library instead of a static library, and give it an soname
-sed -e 's/STATIC/SHARED/' \
- -e '/^[[:blank:]]*OUTPUT_NAME lfscc/i\ VERSION 0.0.0\n SOVERSION 0' \
- -e 's/ARCHIVE DESTINATION/LIBRARY DESTINATION/' \
- -e '/^set_target_properties/iTARGET_LINK_LIBRARIES(liblfscc gmp)' \
- -i src/CMakeLists.txt
-
-# Fix the library install path
-if [ "%{_lib}" = "lib64" ]; then
- sed -i 's,/lib,/lib64,' src/CMakeLists.txt
-fi
-
-# Fix the test script
-%py3_shebang_fix tests/run_test.py
-
-%build
-%cmake
-%cmake_build
-
-%install
-%cmake_install
-
-# Install the proof files
-mkdir -p %{buildroot}%{_datadir}/%{name}
-cp -p %{SOURCE1} %{SOURCE2} %{SOURCE3} %{SOURCE4} %{SOURCE5} %{SOURCE6} \
- %{SOURCE7} %{SOURCE8} %{SOURCE9} %{buildroot}%{_datadir}/%{name}
-
-# Generate a man page
-cd %{_vpath_builddir}/src
-mkdir -p %{buildroot}%{_mandir}/man1
-export LD_LIBRARY_PATH=$PWD
-help2man -N --version-string=%{version} -n 'SMT proof checker' ./lfscc > \
- %{buildroot}%{_mandir}/man1/lfscc.1
-# Fix line breaks in the man page
-sed -i 's/\\fB/.TP\n&/;s/\\fR: /\\fR\n/' %{buildroot}%{_mandir}/man1/lfscc.1
-
-# Help the debuginfo generator
-cp -p ../../src/lexer.flex .
-cd -
-
-%check
-%ctest
-
-%files
-%license COPYING
-%doc AUTHORS README.md
-%{_bindir}/lfscc
-%{_datadir}/%{name}/
-%{_libdir}/liblfscc.so.0{,.*}
-%{_mandir}/man1/lfscc.1*
-
-%files devel
-%{_includedir}/lfscc.h
-%{_libdir}/liblfscc.so
-
-%changelog
-* Thu Jul 16 2026 Fedora Release Engineering <releng@fedoraproject.org> - 0.20230914-6
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild
-
-* Fri Jan 16 2026 Fedora Release Engineering <releng@fedoraproject.org> - 0.20230914-5
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild
-
-* Thu Jul 24 2025 Fedora Release Engineering <releng@fedoraproject.org> - 0.20230914-4
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild
-
-* Fri Jan 17 2025 Fedora Release Engineering <releng@fedoraproject.org> - 0.20230914-3
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild
-
-* Thu Jul 18 2024 Fedora Release Engineering <releng@fedoraproject.org> - 0.20230914-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild
-
-* Thu Mar 14 2024 Jerry James <loganjerry@gmail.com> - 0.20230914-1
-- Update to 20230914 git snapshot
-- Drop upstreamed stdint patch
-
-* Thu Jan 25 2024 Fedora Release Engineering <releng@fedoraproject.org> - 0.20230523-3
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
-
-* Sun Jan 21 2024 Fedora Release Engineering <releng@fedoraproject.org> - 0.20230523-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
-
-* Tue Jan 16 2024 Jerry James <loganjerry@gmail.com> - 0.20230523-1
-- Stop building for 32-bit x86
-
-* Fri Jul 28 2023 Jerry James <loganjerry@gmail.com> - 0.20230523-1
-- Update to 20230523 git snapshot
-
-* Thu Jul 20 2023 Fedora Release Engineering <releng@fedoraproject.org> - 0.20210305-6
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
-
-* Thu Jan 19 2023 Jerry James <loganjerry@gmail.com> - 0.20210305-5
-- Add -stdint patch to fix FTBFS
-
-* Thu Jan 19 2023 Fedora Release Engineering <releng@fedoraproject.org> - 0.20210305-5
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
-
-* Mon Nov 28 2022 Jerry James <loganjerry@gmail.com> - 0.20210305-4
-- New project URL
-- Convert License tag to SPDX
-
-* Thu Jul 21 2022 Fedora Release Engineering <releng@fedoraproject.org> - 0.20210305-4
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
-
-* Thu Jan 20 2022 Fedora Release Engineering <releng@fedoraproject.org> - 0.20210305-3
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
-
-* Thu Jul 22 2021 Fedora Release Engineering <releng@fedoraproject.org> - 0.20210305-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
-
-* Sat Jul 17 2021 Jerry James <loganjerry@gmail.com> - 0.20210305-1
-- Update to 20210305 git snapshot
-
-* Tue Jan 26 2021 Fedora Release Engineering <releng@fedoraproject.org> - 0.20201110-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
-
-* Tue Jan 19 2021 Jerry James <loganjerry@gmail.com> - 0.20201110-1
-- Update to 20201110 snapshot
-
-* Mon Aug 24 2020 Jerry James <loganjerry@gmail.com> - 0.20200815-1
-- Update to 20200815 git snapshot
-
-* Tue Jul 28 2020 Fedora Release Engineering <releng@fedoraproject.org> - 0.20200719-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
-
-* Sat Jul 25 2020 Jerry James <loganjerry@gmail.com> - 0.20200719-1
-- Update to 20200719 git snapshot
-- Adapt to cmake changes in Rawhide
-
-* Thu Mar 5 2020 Jerry James <loganjerry@gmail.com> - 0.20200115-1
-- Update to latest git snapshot
-- Link the library with gmp
-- Generate a man page for the binary with help2man
-
-* Wed Jan 29 2020 Fedora Release Engineering <releng@fedoraproject.org> - 0.20190808-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
-
-* Mon Sep 9 2019 Jerry James <loganjerry@gmail.com> - 0.20190808-1
-- Update to latest git snapshot
-
-* Thu Jul 25 2019 Fedora Release Engineering <releng@fedoraproject.org> - 0.20190226-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
-
-* Wed Jun 12 2019 Jerry James <loganjerry@gmail.com> - 0.20190226-1
-- Update to latest git snapshot
-
-* Thu Feb 7 2019 Jerry James <loganjerry@gmail.com> - 0.20190113-1
-- Update to latest git snapshot for identifier bug fix
-- Add -map patch to fix use of deprecated interface
-
-* Fri Feb 01 2019 Fedora Release Engineering <releng@fedoraproject.org> - 0.20181122-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
-
-* Mon Nov 26 2018 Jerry James <loganjerry@gmail.com> - 0.20181122-1
-- Update to latest git snapshot for 2 bug fixes
-- Use upstream's new test suite
-
-* Wed Nov 7 2018 Jerry James <loganjerry@gmail.com> - 0.20181029-1
-- Update to latest git snapshot
-
-* Fri Jul 13 2018 Fedora Release Engineering <releng@fedoraproject.org> - 0.20180322-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
-
-* Thu Jul 5 2018 Jerry James <loganjerry@gmail.com> - 0.20180322-1
-- Initial RPM (unretired)
diff --git a/sat.plf b/sat.plf
deleted file mode 100644
index f463424..0000000
--- a/sat.plf
+++ /dev/null
@@ -1,122 +0,0 @@
-(declare bool type)
-(declare tt bool)
-(declare ff bool)
-
-(declare var type)
-
-(declare lit type)
-(declare pos (! x var lit))
-(declare neg (! x var lit))
-
-(declare clause type)
-(declare cln clause)
-(declare clc (! x lit (! c clause clause)))
-
-; constructs for general clauses for R, Q, satlem
-
-(declare concat (! c1 clause (! c2 clause clause)))
-(declare clr (! l lit (! c clause clause)))
-
-; code to check resolutions
-
-(program append ((c1 clause) (c2 clause)) clause
- (match c1 (cln c2) ((clc l c1') (clc l (append c1' c2)))))
-
-; we use marks as follows:
-; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable.
-; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable.
-; -- mark 3 if we did indeed remove the variable positively
-; -- mark 4 if we did indeed remove the variable negatively
-(program simplify_clause ((c clause)) clause
- (match c
- (cln cln)
- ((clc l c1)
- (match l
- ; Set mark 1 on v if it is not set, to indicate we should remove it.
- ; After processing the rest of the clause, set mark 3 if we were already
- ; supposed to remove v (so if mark 1 was set when we began). Clear mark3
- ; if we were not supposed to be removing v when we began this call.
- ((pos v)
- (let m (ifmarked v tt (do (markvar v) ff))
- (let c' (simplify_clause c1)
- (match m
- (tt (do (ifmarked3 v v (markvar3 v)) c'))
- (ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c')))))))
- ; the same as the code for tt, but using different marks.
- ((neg v)
- (let m (ifmarked2 v tt (do (markvar2 v) ff))
- (let c' (simplify_clause c1)
- (match m
- (tt (do (ifmarked4 v v (markvar4 v)) c'))
- (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c')))))))))
- ((concat c1 c2) (append (simplify_clause c1) (simplify_clause c2)))
- ((clr l c1)
- (match l
- ; set mark 1 to indicate we should remove v, and fail if
- ; mark 3 is not set after processing the rest of the clause
- ; (we will set mark 3 if we remove a positive occurrence of v).
- ((pos v)
- (let m (ifmarked v tt (do (markvar v) ff))
- (let m3 (ifmarked3 v (do (markvar3 v) tt) ff)
- (let c' (simplify_clause c1)
- (ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v)))
- (match m (tt v) (ff (markvar v))) c')
- (fail clause))))))
- ; same as the tt case, but with different marks.
- ((neg v)
- (let m2 (ifmarked2 v tt (do (markvar2 v) ff))
- (let m4 (ifmarked4 v (do (markvar4 v) tt) ff)
- (let c' (simplify_clause c1)
- (ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v)))
- (match m2 (tt v) (ff (markvar2 v))) c')
- (fail clause))))))
- ))))
-
-
-; resolution proofs
-
-(declare holds (! c clause type))
-
-(define bottom (holds cln))
-
-(declare R (! c1 clause (! c2 clause
- (! u1 (holds c1)
- (! u2 (holds c2)
- (! n var
- (holds (concat (clr (pos n) c1)
- (clr (neg n) c2)))))))))
-
-(declare Q (! c1 clause (! c2 clause
- (! u1 (holds c1)
- (! u2 (holds c2)
- (! n var
- (holds (concat (clr (neg n) c1)
- (clr (pos n) c2)))))))))
-
-(declare satlem (! c1 clause
- (! c2 clause
- (! c3 clause
- (! u1 (holds c1)
- (! r (^ (simplify_clause c1) c2)
- (! u2 (! x (holds c2) (holds c3))
- (holds c3))))))))
-
-
-; A little example to demonstrate simplify_clause.
-; It can handle nested clr's of both polarities,
-; and correctly cleans up marks when it leaves a
-; clr or clc scope. Uncomment and run with
-; --show-runs to see it in action.
-;
-; (check
-; (% v1 var
-; (% u1 (holds (concat (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln))))))
-; (clc (pos v1) (clc (pos v1) cln))))
-; (satlem _ _ _ u1 (\ x x))))))
-
-
-;(check
-; (% v1 var
-; (% u1 (holds (clr (neg v1) (concat (clc (neg v1) cln)
-; (clr (neg v1) (clc (neg v1) cln)))))
-; (satlem _ _ _ u1 (\ x x))))))
\ No newline at end of file
diff --git a/smt.plf b/smt.plf
deleted file mode 100644
index 3ae6edd..0000000
--- a/smt.plf
+++ /dev/null
@@ -1,271 +0,0 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; SMT syntax and semantics (not theory-specific)
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(declare formula type)
-(declare th_holds (! f formula type))
-
-; constants
-(declare true formula)
-(declare false formula)
-
-; logical connectives
-(declare not (! f formula formula))
-(declare and (! f1 formula (! f2 formula formula)))
-(declare or (! f1 formula (! f2 formula formula)))
-(declare impl (! f1 formula (! f2 formula formula)))
-(declare iff (! f1 formula (! f2 formula formula)))
-(declare xor (! f1 formula (! f2 formula formula)))
-(declare ifte (! b formula (! f1 formula (! f2 formula formula))))
-
-; terms
-(declare sort type) ; sort in the theory
-(declare arrow (! s1 sort (! s2 sort sort))) ; function constructor
-
-(declare term (! t sort type)) ; declared terms in formula
-
-(declare apply (! s1 sort
- (! s2 sort
- (! t1 (term (arrow s1 s2))
- (! t2 (term s1)
- (term s2))))))
-
-(declare ite (! s sort
- (! f formula
- (! t1 (term s)
- (! t2 (term s)
- (term s))))))
-
-; let/flet
-(declare let (! s sort
- (! t (term s)
- (! f (! v (term s) formula)
- formula))))
-(declare flet (! f1 formula
- (! f2 (! v formula formula)
- formula)))
-
-; predicates
-(declare = (! s sort
- (! x (term s)
- (! y (term s)
- formula))))
-
-(declare distinct (! s sort
- (! x (term s)
- (! y (term s)
- formula))))
-
-; To avoid duplicating some of the rules (e.g., cong), we will view
-; applications of predicates as terms of sort "Bool".
-; Such terms can be injected as atomic formulas using "p_app".
-
-(declare Bool sort) ; the special sort for predicates
-(declare p_app (! x (term Bool) formula)) ; propositional application of term
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-; Examples
-
-; an example of "(p1 or p2(0)) and t1=t2(1)"
-;(! p1 (term Bool)
-;(! p2 (term (arrow Int Bool))
-;(! t1 (term Int)
-;(! t2 (term (arrow Int Int))
-;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0)))
-; (= _ t1 (apply _ _ t2 1))))
-; ...
-
-; another example of "p3(a,b)"
-;(! a (term Int)
-;(! b (term Int)
-;(! p3 (term (arrow Int (arrow Int Bool))) ; arrow is right assoc.
-;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc.
-; ...
-
-; natural deduction rules here
-
-(declare LEM
- (! f formula
- (th_holds (or (not f) f))))
-
-; bottom elim
-(declare bottom_elim
- (! f formula
- (! u bottom
- (th_holds f))))
-
-
-;; not not
-
-(declare not_not_intro
- (! f formula
- (! u (th_holds f)
- (th_holds (not (not f))))))
-
-(declare not_not_elim
- (! f formula
- (! u (th_holds (not (not f)))
- (th_holds f))))
-
-;; or elimination
-
-(declare or_elim_1
- (! f1 formula
- (! f2 formula
- (! u1 (th_holds (not f1))
- (! u2 (th_holds (or f1 f2))
- (th_holds f2))))))
-
-(declare or_elim_2
- (! f1 formula
- (! f2 formula
- (! u1 (th_holds (not f2))
- (! u2 (th_holds (or f1 f2))
- (th_holds f1))))))
-
-;; and elimination
-
-(declare and_intro
- (! f1 formula
- (! f2 formula
- (! u1 (th_holds f1)
- (! u2 (th_holds f2)
- (th_holds (and f1 f2)))))))
-
-(declare and_elim_1
- (! f1 formula
- (! f2 formula
- (! u (th_holds (and f1 f2))
- (th_holds f1)))))
-
-(declare and_elim_2
- (! f1 formula
- (! f2 formula
- (! u (th_holds (and f1 f2))
- (th_holds f2)))))
-
-;; not impl elimination
-
-(declare not_impl_elim_1
- (! f1 formula
- (! f2 formula
- (! u (th_holds (not (impl f1 f2)))
- (th_holds f1)))))
-
-(declare not_impl_elim_2
- (! f1 formula
- (! f2 formula
- (! u (th_holds (not (impl f1 f2)))
- (th_holds (not f2))))))
-
-;; impl elimination
-
-(declare impl_intro (! f1 formula
- (! f2 formula
- (! i1 (! u (th_holds f1)
- (th_holds f2))
- (th_holds (impl f1 f2))))))
-
-(declare impl_elim
- (! f1 formula
- (! f2 formula
- (! u1 (th_holds f1)
- (! u2 (th_holds (impl f1 f2))
- (th_holds f2))))))
-
-;; iff elimination
-
-(declare iff_elim_1
- (! f1 formula
- (! f2 formula
- (! u1 (th_holds (iff f1 f2))
- (th_holds (impl f1 f2))))))
-
-(declare iff_elim_2
- (! f1 formula
- (! f2 formula
- (! u1 (th_holds (iff f1 f2))
- (th_holds (impl f2 f1))))))
-
-(declare not_iff_elim_1
- (! f1 formula
- (! f2 formula
- (! u1 (th_holds (not f1))
- (! u2 (th_holds (not (iff f1 f2)))
- (th_holds f2))))))
-
-(declare not_iff_elim_2
- (! f1 formula
- (! f2 formula
- (! u1 (th_holds f1)
- (! u2 (th_holds (not (iff f1 f2)))
- (th_holds (not f2)))))))
-
-;; ite elimination
-
-(declare ite_elim_1
- (! a formula
- (! b formula
- (! c formula
- (! u1 (th_holds a)
- (! u2 (th_holds (ifte a b c))
- (th_holds b)))))))
-
-(declare ite_elim_2
- (! a formula
- (! b formula
- (! c formula
- (! u1 (th_holds (not a))
- (! u2 (th_holds (ifte a b c))
- (th_holds c)))))))
-
-(declare ite_elim_3
- (! a formula
- (! b formula
- (! c formula
- (! u1 (th_holds (not b))
- (! u2 (th_holds (ifte a b c))
- (th_holds c)))))))
-
-(declare ite_elim_2n
- (! a formula
- (! b formula
- (! c formula
- (! u1 (th_holds a)
- (! u2 (th_holds (ifte (not a) b c))
- (th_holds c)))))))
-
-(declare not_ite_elim_1
- (! a formula
- (! b formula
- (! c formula
- (! u1 (th_holds a)
- (! u2 (th_holds (not (ifte a b c)))
- (th_holds (not b))))))))
-
-(declare not_ite_elim_2
- (! a formula
- (! b formula
- (! c formula
- (! u1 (th_holds (not a))
- (! u2 (th_holds (not (ifte a b c)))
- (th_holds (not c))))))))
-
-(declare not_ite_elim_3
- (! a formula
- (! b formula
- (! c formula
- (! u1 (th_holds b)
- (! u2 (th_holds (not (ifte a b c)))
- (th_holds (not c))))))))
-
-(declare not_ite_elim_2n
- (! a formula
- (! b formula
- (! c formula
- (! u1 (th_holds a)
- (! u2 (th_holds (not (ifte (not a) b c)))
- (th_holds (not c))))))))
\ No newline at end of file
diff --git a/sources b/sources
deleted file mode 100644
index 03b0693..0000000
--- a/sources
+++ /dev/null
@@ -1 +0,0 @@
-SHA512 (lfsc-5a127db.tar.gz) = 54fe25dc54161e5e43c3ee3b0f5e890b81aaf4c9b58e41699ed8f64674c8741b41196d7b1fbf7f5d76eb3e6d4c7d923a36d6a66368ed1cea62157d060dd0d928
diff --git a/th_base.plf b/th_base.plf
deleted file mode 100644
index 903654c..0000000
--- a/th_base.plf
+++ /dev/null
@@ -1,135 +0,0 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Atomization
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-
-; binding between an LF var and an (atomic) formula
-(declare atom (! v var (! p formula type)))
-
-(declare decl_atom
- (! f formula
- (! u (! v var
- (! a (atom v f)
- bottom))
- bottom)))
-
-; direct clausify
-(declare clausify_form
- (! f formula
- (! v var
- (! a (atom v f)
- (! u (th_holds f)
- (holds (clc (pos v) cln)))))))
-
-(declare clausify_form_not
- (! f formula
- (! v var
- (! a (atom v f)
- (! u (th_holds (not f))
- (holds (clc (neg v) cln)))))))
-
-(declare clausify_false
- (! u (th_holds false)
- bottom))
-
-(declare let_pf
- (! c clause
- (! c' clause
- (! u (holds c)
- (! u2 (! v (holds c) bottom)
- bottom)))))
-
-(declare th_let_pf
- (! f formula
- (! u (th_holds f)
- (! u2 (! v (th_holds f) bottom)
- bottom))))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Theory reasoning
-; - make a series of assumptions and then derive a contradiction (or false)
-; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
-; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(declare ast
- (! v var
- (! f formula
- (! C clause
- (! r (atom v f) ;this is specified
- (! u (! o (th_holds f)
- (holds C))
- (holds (clc (neg v) C))))))))
-
-(declare asf
- (! v var
- (! f formula
- (! C clause
- (! r (atom v f)
- (! u (! o (th_holds (not f))
- (holds C))
- (holds (clc (pos v) C))))))))
-
-(declare contra
- (! f formula
- (! r1 (th_holds f)
- (! r2 (th_holds (not f))
- (holds cln)))))
-
-(declare th_ast
- (! f formula
- (! u (! o (th_holds f)
- (holds cln))
- (th_holds (not f)))))
-
-(declare th_asf
- (! f formula
- (! u (! o (th_holds (not f))
- (holds cln))
- (th_holds f))))
-
-(declare lem
- (! f formula
- (! v var
- (! a (atom v f)
- (holds (clc (pos v) (clc (neg v) cln)))))))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Theory of Equality and Congruence Closure
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(declare refl
- (! s sort
- (! t (term s)
- (th_holds (= s t t)))))
-
-(declare symm (! s sort
- (! x (term s)
- (! y (term s)
- (! u (th_holds (= _ x y))
- (th_holds (= _ y x)))))))
-
-(declare trans (! s sort
- (! x (term s)
- (! y (term s)
- (! z (term s)
- (! u (th_holds (= _ x y))
- (! u (th_holds (= _ y z))
- (th_holds (= _ x z)))))))))
-
-(declare cong (! s1 sort
- (! s2 sort
- (! a1 (term (arrow s1 s2))
- (! b1 (term (arrow s1 s2))
- (! a2 (term s1)
- (! b2 (term s1)
- (! u1 (th_holds (= _ a1 b1))
- (! u2 (th_holds (= _ a2 b2))
- (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))
-
diff --git a/th_lra-cvc3.plf b/th_lra-cvc3.plf
deleted file mode 100644
index 5cd2639..0000000
--- a/th_lra-cvc3.plf
+++ /dev/null
@@ -1,1089 +0,0 @@
-; polynomial normalization for unary minus
-
-(declare pn_mul_u-_c_L
- (! y (term Real)
- (! py poly
- (! pz poly
- (! x mpq
- (! pny (poly_norm y py)
- (! a (^ (poly_mul_c py (mp_neg x)) pz)
- (poly_norm (*_Real (u-_Real (a_real x)) y) pz))))))))
-
-(declare pn_mul_u-_c_R
- (! y (term Real)
- (! py poly
- (! pz poly
- (! x mpq
- (! pny (poly_norm y py)
- (! a (^ (poly_mul_c py (mp_neg x)) pz)
- (poly_norm (*_Real y (u-_Real (a_real x))) pz))))))))
-
-(declare pn_u-
- (! y (term Real)
- (! py poly
- (! pz poly
- (! pny (poly_norm y py)
- (! a (^ (poly_neg py) pz)
- (poly_norm (u-_Real y) pz)))))))
-
-
-; and normalization
-
-(program do_and_elim ((f formula) (c mpz) (isEnd bool)) formula
- (match f
- ((and f1 f2)
- (mp_ifzero c
- (match isEnd (tt f) (ff f1))
- (do_and_elim f2 (mp_add c (~ 1)) isEnd)))
- (default f)))
-
-(program do_and_rem ((f formula) (c mpz)) formula
- (match f
- ((and f1 f2) (mp_ifzero c f2 (and f1 (do_and_rem f2 (mp_add c (~ 1))))))
- (default f)))
-
-(declare and_elim
- (! f formula
- (! f' formula
- (! c mpz
- (! u1 (th_holds f)
- (! r (^ (do_and_elim f c ff) f')
- (th_holds f')))))))
-
-(declare and_elim_end
- (! f formula
- (! f' formula
- (! c mpz
- (! u1 (th_holds f)
- (! r (^ (do_and_elim f c tt) f')
- (th_holds f')))))))
-
-(declare and_rem
- (! f formula
- (! f' formula
- (! c mpz
- (! u1 (th_holds f)
- (! r (^ (do_and_rem f c) f')
- (th_holds f')))))))
-
-; and normalize
-(program do_and_normalize_h ((f formula) (fc formula)) formula
- (match f
- ; ((true) fc)
- ((and f1 f2) (do_and_normalize_h f1 (do_and_normalize_h f2 fc)))
- (default (and f fc))))
-
-(program do_and_normalize ((f formula)) formula
- (match f
- ((and f1 f2) (do_and_normalize_h f1 (do_and_normalize f2)))
- (default f)))
-
-(declare and_norm
- (! f formula
- (! f' formula
- (! u (th_holds f)
- (! r (^ (do_and_normalize f) f')
- (th_holds f'))))))
-
-(declare and_normalize
- (! f' formula
- (! f formula
- (! r (^ (do_and_normalize f) f')
- (th_holds (iff f f'))))))
-
-(declare and_nd
- (! f1 formula
- (! f2 formula
- (! f' formula
- (! u (th_holds (iff f1 f2))
- (! r (^ (do_and_normalize f1) f')
- (th_holds (iff f1 f2))))))))
-
-(declare and_redundant
- (! f formula
- (th_holds (iff (and f f) f))))
-
-(declare and_symm
- (! f1 formula
- (! f2 formula
- (th_holds (iff (and f1 f2) (and f2 f1))))))
-
-
-
-
-
-; or elimination
-
-(program do_or_elim ((f formula) (c mpz) (isEnd bool)) formula
- (match f
- ((or f1 f2)
- (mp_ifzero c
- (match isEnd (tt f) (ff f1))
- (do_or_elim f2 (mp_add c (~ 1)) isEnd)))
- (default f)))
-
-(declare or_elim
- (! f formula
- (! f' formula
- (! c mpz
- (! u1 (th_holds (not f))
- (! r (^ (do_or_elim f c ff) f')
- (th_holds (not f'))))))))
-
-(declare or_elim_end
- (! f formula
- (! f' formula
- (! c mpz
- (! u1 (th_holds (not f))
- (! r (^ (do_or_elim f c tt) f')
- (th_holds (not f'))))))))
-
-(program do_or_normalize_h ((f formula) (fc formula)) formula
- (match f
- ; ((false) fc)
- ((or f1 f2) (do_or_normalize_h f1 (do_or_normalize_h f2 fc)))
- (default (or f fc))))
-
-(program do_or_normalize ((f formula)) formula
- (match f
- ((or f1 f2) (do_or_normalize_h f1 (do_or_normalize f2)))
- (default f)))
-
-(declare or_norm
- (! f formula
- (! f' formula
- (! u (th_holds f)
- (! r (^ (do_or_normalize f) f')
- (th_holds f'))))))
-
-(declare or_normalize
- (! f' formula
- (! f formula
- (! r (^ (do_or_normalize f) f')
- (th_holds (iff f f'))))))
-
-(declare or_nd
- (! f1 formula
- (! f2 formula
- (! f' formula
- (! u (th_holds (iff f1 f2))
- (! r (^ (do_or_normalize f1) f')
- (th_holds (iff f1 f2))))))))
-
-(declare or_redundant
- (! f formula
- (th_holds (iff (or f f) f))))
-
-(declare or_symm
- (! f1 formula
- (! f2 formula
- (th_holds (iff (or f1 f2) (or f2 f1))))))
-
-(declare or_intro_1
- (! f1 formula
- (! f2 formula
- (! v var
- (! a (atom v f2)
- (! u (th_holds f1)
- (th_holds (or f1 f2))))))))
-
-(declare or_intro_2
- (! f1 formula
- (! f2 formula
- (! v var
- (! a (atom v f2)
- (! u (th_holds f1)
- (th_holds (or f2 f1))))))))
-
-
-
-
-
-
-
-; transitivity for iff
-(declare impl_trans (! f1 formula
- (! f2 formula
- (! f3 formula
- (! i1 (th_holds (impl f1 f2))
- (! i2 (th_holds (impl f2 f3))
- (th_holds (impl f1 f3))))))))
-
-(define impl_mp impl_elim)
-
-; reflexivity for impl
-(declare impl_refl (! f formula
- (th_holds (impl f f))))
-; reflexivity for impl
-(declare impl_refl_atom (! v var
- (! f formula
- (! a (atom v f)
- (th_holds (impl f f))))))
-(declare impl_refl_atom_not (! v var
- (! f formula
- (! a (atom v f)
- (th_holds (impl (not f) (not f)))))))
-
-
-(declare impl_refl_false (th_holds (impl false false)))
-(declare impl_refl_true (th_holds (impl true true)))
-
-; symmetry for iff
-(declare impl_symm (! f1 formula
- (! f2 formula
- (! i1 (th_holds (impl f1 f2))
- (th_holds (impl f2 f1))))))
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Rules for iff
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-; dual implication is iff
-(declare iff_intro (! f1 formula
- (! f2 formula
- (! i1 (th_holds (impl f1 f2))
- (! i2 (th_holds (impl f2 f1))
- (th_holds (iff f1 f2)))))))
-
-; reflexivity for iff
-(declare iff_refl_false (th_holds (iff false false)))
-(declare iff_refl_true (th_holds (iff true true)))
-(declare iff_refl
- (! f formula
- (th_holds (iff f f))))
-
-; symmetry for iff
-(declare iff_symm (! f1 formula
- (! f2 formula
- (! i1 (th_holds (iff f1 f2))
- (th_holds (iff f2 f1))))))
-
-; transitivity for iff
-(declare iff_trans (! f1 formula
- (! f2 formula
- (! f3 formula
- (! i1 (th_holds (iff f1 f2))
- (! i2 (th_holds (iff f2 f3))
- (th_holds (iff f1 f3))))))))
-
-; mp for iff
-(declare iff_mp (! f1 formula
- (! f2 formula
- (! i1 (th_holds f1)
- (! i2 (th_holds (iff f1 f2))
- (th_holds f2))))))
-
-;;
-
-(declare basic_subst_op_=
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (! i1 (th_holds (= Real t1 t2))
- (! i2 (th_holds (= Real t3 t4))
- (th_holds (iff (= Real t1 t3) (= Real t2 t4))))))))))
-
-(declare basic_subst_op_<
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (! i1 (th_holds (= Real t1 t2))
- (! i2 (th_holds (= Real t3 t4))
- (th_holds (iff (<_Real t1 t3) (<_Real t2 t4))))))))))
-
-(declare basic_subst_op_>
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (! i1 (th_holds (= Real t1 t2))
- (! i2 (th_holds (= Real t3 t4))
- (th_holds (iff (>_Real t1 t3) (>_Real t2 t4))))))))))
-
-(declare basic_subst_op_<=
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (! i1 (th_holds (= Real t1 t2))
- (! i2 (th_holds (= Real t3 t4))
- (th_holds (iff (<=_Real t1 t3) (<=_Real t2 t4))))))))))
-
-(declare basic_subst_op_>=
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (! i1 (th_holds (= Real t1 t2))
- (! i2 (th_holds (= Real t3 t4))
- (th_holds (iff (>=_Real t1 t3) (>=_Real t2 t4))))))))))
-
-(declare basic_subst_op_distinct
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (! i1 (th_holds (= Real t1 t2))
- (! i2 (th_holds (= Real t3 t4))
- (th_holds (iff (distinct Real t1 t3) (distinct Real t2 t4))))))))))
-
-
-;; subst op1
-
-(declare basic_subst_op1_+
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (! i1 (th_holds (= Real t1 t2))
- (! i2 (th_holds (= Real t3 t4))
- (th_holds (= Real (+_Real t1 t3) (+_Real t2 t4))))))))))
-
-(declare basic_subst_op1_-
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (! i1 (th_holds (= Real t1 t2))
- (! i2 (th_holds (= Real t3 t4))
- (th_holds (= Real (-_Real t1 t3) (-_Real t2 t4))))))))))
-
-(declare basic_subst_op1_*
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (! i1 (th_holds (= Real t1 t2))
- (! i2 (th_holds (= Real t3 t4))
- (th_holds (= Real (*_Real t1 t3) (*_Real t2 t4))))))))))
-
-(declare basic_subst_op1_or
- (! f1 formula
- (! f2 formula
- (! f3 formula
- (! f4 formula
- (! i1 (th_holds (iff f1 f2))
- (! i2 (th_holds (iff f3 f4))
- (th_holds (iff (or f1 f3) (or f2 f4))))))))))
-
-(declare basic_subst_op1_and
- (! f1 formula
- (! f2 formula
- (! f3 formula
- (! f4 formula
- (! i1 (th_holds (iff f1 f2))
- (! i2 (th_holds (iff f3 f4))
- (th_holds (iff (and f1 f3) (and f2 f4))))))))))
-
-(declare basic_subst_op1_iff
- (! f1 formula
- (! f2 formula
- (! f3 formula
- (! f4 formula
- (! i1 (th_holds (iff f1 f2))
- (! i2 (th_holds (iff f3 f4))
- (th_holds (iff (iff f1 f3) (iff f2 f4))))))))))
-
-(define basic_subst_op1_= basic_subst_op_=)
-(define basic_subst_op1_>= basic_subst_op_>=)
-(define basic_subst_op1_<= basic_subst_op_<=)
-(define basic_subst_op1_> basic_subst_op_>)
-(define basic_subst_op1_< basic_subst_op_<)
-(define basic_subst_op1_distinct basic_subst_op_distinct)
-
-(declare basic_subst_op1_impl_or
- (! f1 formula
- (! f2 formula
- (! f3 formula
- (! f4 formula
- (! i1 (th_holds (impl f1 f2))
- (! i2 (th_holds (impl f3 f4))
- (th_holds (impl (or f1 f3) (or f2 f4))))))))))
-
-(declare basic_subst_op1_impl_and
- (! f1 formula
- (! f2 formula
- (! f3 formula
- (! f4 formula
- (! i1 (th_holds (impl f1 f2))
- (! i2 (th_holds (impl f3 f4))
- (th_holds (impl (and f1 f3) (and f2 f4))))))))))
-
-
-
-(declare basic_subst_op0_not
- (! f1 formula
- (! f2 formula
- (! i1 (th_holds (iff f1 f2))
- (th_holds (iff (not f1) (not f2)))))))
-
-(declare basic_subst_op0_u-
- (! t1 (term Real)
- (! t2 (term Real)
- (! i1 (th_holds (= Real t1 t2))
- (th_holds (= Real (u-_Real t1) (u-_Real t2)))))))
-
-(declare optimized_subst_op_ite
- (! f formula
- (! f1 formula
- (! f2 formula
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (! u1 (th_holds (= Real (ite Real f t1 t2) (ite Real f t3 t4)))
- (! u2 (th_holds (iff f1 f2))
- (th_holds (= Real (ite Real f1 t1 t2) (ite Real f2 t3 t4)))))))))))))
-
-(declare optimized_subst_op_ite_t1
- (! f1 formula
- (! f2 formula
- (! t (term Real)
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (! u1 (th_holds (= Real (ite Real f1 t t2) (ite Real f2 t t4)))
- (! u (th_holds (= Real t1 t3))
- (th_holds (= Real (ite Real f1 t1 t2) (ite Real f2 t3 t4)))))))))))))
-
-(declare optimized_subst_op_ite_t2
- (! f1 formula
- (! f2 formula
- (! t (term Real)
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (! u1 (th_holds (= Real (ite Real f1 t1 t) (ite Real f2 t3 t)))
- (! u (th_holds (= Real t2 t4))
- (th_holds (= Real (ite Real f1 t1 t2) (ite Real f2 t3 t4)))))))))))))
-
-
-(declare optimized_subst_op_ifte
- (! f formula
- (! f1 formula
- (! f2 formula
- (! ft1 formula
- (! ft2 formula
- (! ft3 formula
- (! ft4 formula
- (! u1 (th_holds (iff (ifte f ft1 ft2) (ifte f ft3 ft4)))
- (! u2 (th_holds (iff f1 f2))
- (th_holds (iff (ifte f1 ft1 ft2) (ifte f2 ft3 ft4)))))))))))))
-
-(declare optimized_subst_op_ifte_t1
- (! f1 formula
- (! f2 formula
- (! ft formula
- (! ft1 formula
- (! ft2 formula
- (! ft3 formula
- (! ft4 formula
- (! u1 (th_holds (iff (ifte f1 ft ft2) (ifte f2 ft ft4)))
- (! u (th_holds (iff ft1 ft3))
- (th_holds (iff (ifte f1 ft1 ft2) (ifte f2 ft3 ft4)))))))))))))
-
-(declare optimized_subst_op_ifte_t2
- (! f1 formula
- (! f2 formula
- (! ft formula
- (! ft1 formula
- (! ft2 formula
- (! ft3 formula
- (! ft4 formula
- (! u1 (th_holds (iff (ifte f1 ft1 ft) (ifte f2 ft3 ft)))
- (! u (th_holds (iff ft2 ft4))
- (th_holds (iff (ifte f1 ft1 ft2) (ifte f2 ft3 ft4)))))))))))))
-
-(declare optimized_subst_op_impl_ite
- (! f1 formula
- (! f2 formula
- (! t1 (term Real)
- (! t2 (term Real)
- (! u (th_holds (impl f1 f2))
- (th_holds (= Real (ite Real f1 t1 t2) (ite Real f2 t1 t2)))))))))
-
-(declare optimized_subst_op_impl_and
- (! f1 formula
- (! f2 formula
- (! f3 formula
- (! u (th_holds (impl f1 f2))
- (th_holds (impl (and f1 f3) (and f1 f3))))))))
-
-(declare optimized_subst_op_impl_or
- (! f1 formula
- (! f2 formula
- (! f3 formula
- (! u (th_holds (impl f1 f2))
- (th_holds (impl (or f1 f3) (or f1 f3))))))))
-
-
-;; real shadow
-
-(declare real_shadow_<_<
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! f1 (th_holds (<_Real t1 t2))
- (! f2 (th_holds (<_Real t2 t3))
- (th_holds (<_Real t1 t3))))))))
-
-(declare real_shadow_<_<=
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! f1 (th_holds (<_Real t1 t2))
- (! f2 (th_holds (<=_Real t2 t3))
- (th_holds (<_Real t1 t3))))))))
-
-(declare real_shadow_<=_<
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! f1 (th_holds (<=_Real t1 t2))
- (! f2 (th_holds (<_Real t2 t3))
- (th_holds (<_Real t1 t3))))))))
-
-(declare real_shadow_<=_<=
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! f1 (th_holds (<=_Real t1 t2))
- (! f2 (th_holds (<=_Real t2 t3))
- (th_holds (<=_Real t1 t3))))))))
-
-;; real shadow eq
-
-(declare real_shadow_eq
- (! t1 (term Real)
- (! t2 (term Real)
- (! i1 (th_holds (<=_Real t1 t2))
- (! i2 (th_holds (<=_Real t2 t1))
- (th_holds (= Real t1 t2)))))))
-
-;; add inequalities
-
-(declare add_inequalities_<_<=
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (!f1 (th_holds ( <_Real t1 t2))
- (!f2 (th_holds ( <=_Real t3 t4))
- (th_holds (<_Real (+_Real t1 t3) (+_Real t2 t4))))))))))
-
-
-;; right minus left
-
-(declare right_minus_left_=
- (! x (term Real)
- (! y (term Real)
- (th_holds (iff (= Real x y) (= Real (a_real 0/1) (-_Real y x)))))))
-
-(declare right_minus_left_>
- (! x (term Real)
- (! y (term Real)
- (th_holds (iff (>_Real x y) (>_Real (a_real 0/1) (-_Real y x)))))))
-
-(declare right_minus_left_<
- (! x (term Real)
- (! y (term Real)
- (th_holds (iff (<_Real x y) (<_Real (a_real 0/1) (-_Real y x)))))))
-
-(declare right_minus_left_>=
- (! x (term Real)
- (! y (term Real)
- (th_holds (iff (>=_Real x y) (>=_Real (a_real 0/1) (-_Real y x)))))))
-
-(declare right_minus_left_<=
- (! x (term Real)
- (! y (term Real)
- (th_holds (iff (<=_Real x y) (<=_Real (a_real 0/1) (-_Real y x)))))))
-
-(declare right_minus_left_distinct
- (! x (term Real)
- (! y (term Real)
- (th_holds (iff (distinct Real x y) (distinct Real (a_real 0/1) (-_Real y x)))))))
-
-; minus to plus
-
-(declare minus_to_plus
- (! x (term Real)
- (! y (term Real)
- (th_holds (= Real (-_Real x y) (+_Real x (*_Real (a_real (~ 1/1)) y)))))))
-
-;; plus pred
-
-(declare plus_predicate_=
- (! x (term Real)
- (! y (term Real)
- (! z (term Real)
- (th_holds (iff (= Real x y) (= Real (+_Real x z) (+_Real y z))))))))
-
-(declare plus_predicate_>
- (! x (term Real)
- (! y (term Real)
- (! z (term Real)
- (th_holds (iff (>_Real x y) (>_Real (+_Real x z) (+_Real y z))))))))
-
-(declare plus_predicate_<
- (! x (term Real)
- (! y (term Real)
- (! z (term Real)
- (th_holds (iff (<_Real x y) (<_Real (+_Real x z) (+_Real y z))))))))
-
-(declare plus_predicate_>=
- (! x (term Real)
- (! y (term Real)
- (! z (term Real)
- (th_holds (iff (>=_Real x y) (>=_Real (+_Real x z) (+_Real y z))))))))
-
-(declare plus_predicate_<=
- (! x (term Real)
- (! y (term Real)
- (! z (term Real)
- (th_holds (iff (<=_Real x y) (<=_Real (+_Real x z) (+_Real y z))))))))
-
-(declare plus_predicate_distinct
- (! x (term Real)
- (! y (term Real)
- (! z (term Real)
- (th_holds (iff (distinct Real x y) (distinct Real (+_Real x z) (+_Real y z))))))))
-
-;; mult_ineqn
-
-(declare mult_eqn
- (! x (term Real)
- (! y (term Real)
- (! c mpq
- (th_holds (iff (= Real x y) (= Real (*_Real x (a_real c)) (*_Real y (a_real c))))))))))
-
-(declare mult_ineqn_>
- (! x (term Real)
- (! y (term Real)
- (! c mpq
- (! u (^ (mpq_ifpos c) tt)
- (th_holds (iff (>_Real x y) (>_Real (*_Real x (a_real c)) (*_Real y (a_real c))))))))))
-
-(declare mult_ineqn_<
- (! x (term Real)
- (! y (term Real)
- (! c mpq
- (! u (^ (mpq_ifpos c) tt)
- (th_holds (iff (<_Real x y) (<_Real (*_Real x (a_real c)) (*_Real y (a_real c))))))))))
-
-(declare mult_ineqn_>=
- (! x (term Real)
- (! y (term Real)
- (! c mpq
- (! u (^ (mpq_ifpos c) tt)
- (th_holds (iff (>=_Real x y) (>=_Real (*_Real x (a_real c)) (*_Real y (a_real c))))))))))
-
-(declare mult_ineqn_<=
- (! x (term Real)
- (! y (term Real)
- (! c mpq
- (! u (^ (mpq_ifpos c) tt)
- (th_holds (iff (<=_Real x y) (<=_Real (*_Real x (a_real c)) (*_Real y (a_real c))))))))))
-
-(declare mult_ineqn_neg_>
- (! x (term Real)
- (! y (term Real)
- (! c mpq
- (! u (^ (mp_ifneg c tt ff) tt)
- (th_holds (iff (>_Real x y) (>_Real (*_Real y (a_real c)) (*_Real x (a_real c))))))))))
-
-(declare mult_ineqn_neg_<
- (! x (term Real)
- (! y (term Real)
- (! c mpq
- (! u (^ (mp_ifneg c tt ff) tt)
- (th_holds (iff (<_Real x y) (<_Real (*_Real y (a_real c)) (*_Real x (a_real c))))))))))
-
-(declare mult_ineqn_neg_>=
- (! x (term Real)
- (! y (term Real)
- (! c mpq
- (! u (^ (mp_ifneg c tt ff) tt)
- (th_holds (iff (>=_Real x y) (>=_Real (*_Real y (a_real c)) (*_Real x (a_real c))))))))))
-
-(declare mult_ineqn_neg_<=
- (! x (term Real)
- (! y (term Real)
- (! c mpq
- (! u (^ (mp_ifneg c tt ff) tt)
- (th_holds (iff (<=_Real x y) (<=_Real (*_Real y (a_real c)) (*_Real x (a_real c))))))))))
-
-;; canon
-(declare canonize_=
- (! t1 (term Real)
- (! t2 (term Real)
- (! p poly
- (! pn (poly_norm (-_Real t1 t2) p)
- (! u (^ (mp_ifzero (is_poly_const p) tt ff) tt)
- (th_holds (= Real t1 t2))))))))
-
-(declare canonize_iff
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (! p1 poly
- (! p2 poly
- (! pn1 (poly_norm (-_Real t1 t2) p1)
- (! pn2 (poly_norm (-_Real t3 t4) p2)
- (! u (^ (mp_ifzero (is_poly_const (poly_add p1 p2)) tt ff) tt)
- (th_holds (iff (= Real t1 t2) (= Real t3 t4)))))))))))))
-
-(declare canonize_conv
- (! t1 (term Real)
- (! t2 (term Real)
- (! t1' (term Real)
- (! t2' (term Real)
- (! p poly
- (! p' poly
- (! pn (poly_norm (-_Real t1 t2) p)
- (! pn (poly_norm (-_Real t1' t2') p')
- (! u (th_holds (= Real t1 t2))
- (! r (^ (mp_ifzero (is_poly_const (poly_sub p p')) tt ff) tt)
- (th_holds (= Real t1' t2')))))))))))))
-
-;; flip_inequality
-
-(declare flip_inequality_>_<
- (! t1 (term Real)
- (! t2 (term Real)
- (th_holds (iff (>_Real t1 t2) (<_Real t2 t1))))))
-
-(declare flip_inequality_>=_<=
- (! t1 (term Real)
- (! t2 (term Real)
- (th_holds (iff (>=_Real t1 t2) (<=_Real t2 t1))))))
-
- (declare flip_inequality_<_>
- (! t1 (term Real)
- (! t2 (term Real)
- (th_holds (iff (<_Real t1 t2) (>_Real t2 t1))))))
-
-(declare flip_inequality_<=_>=
- (! t1 (term Real)
- (! t2 (term Real)
- (th_holds (iff (<=_Real t1 t2) (>=_Real t2 t1))))))
-
-;; negated inequality
-
-(declare negated_inequality_>_<=
- (! t1 (term Real)
- (! t2 (term Real)
- (th_holds (iff (not (>_Real t1 t2)) (<=_Real t1 t2))))))
-
-(declare negated_inequality_>=_<
- (! t1 (term Real)
- (! t2 (term Real)
- (th_holds (iff (not (>=_Real t1 t2)) (<_Real t1 t2))))))
-
-(declare negated_inequality_<_>=
- (! t1 (term Real)
- (! t2 (term Real)
- (th_holds (iff (not (<_Real t1 t2)) (>=_Real t1 t2))))))
-
-(declare negated_inequality_<=_>
- (! t1 (term Real)
- (! t2 (term Real)
- (th_holds (iff (not (<=_Real t1 t2)) (>_Real t1 t2))))))
-
-;; imply negated inequality
-
-(declare imply_negated_inequality_<_<
- (! t1 (term Real)
- (! t2 (term Real)
- (! p1 poly
- (! p2 poly
- (! pn1 (poly_norm t1 p1)
- (! pn2 (poly_norm t2 p2)
- (! u (^ (mp_ifneg (is_poly_const (poly_add p1 p2)) tt ff) tt)
- (th_holds
- (impl (<_Real (a_real 0/1) t1)
- (not (<_Real (a_real 0/1) t2))))))))))))
-
-(declare imply_negated_inequality_<=_<=
- (! t1 (term Real)
- (! t2 (term Real)
- (! p1 poly
- (! p2 poly
- (! pn1 (poly_norm t1 p1)
- (! pn2 (poly_norm t2 p2)
- (! u (^ (mp_ifneg (is_poly_const (poly_add p1 p2)) tt ff) tt)
- (th_holds
- (impl (<=_Real (a_real 0/1) t1)
- (not (<=_Real (a_real 0/1) t2))))))))))))
-
-(declare imply_negated_inequality_<=_<
- (! t1 (term Real)
- (! t2 (term Real)
- (! p1 poly
- (! p2 poly
- (! pn1 (poly_norm t1 p1)
- (! pn2 (poly_norm t2 p2)
- (! u (^ (mp_ifneg (is_poly_const (poly_add p1 p2)) tt ff) tt)
- (th_holds
- (impl (<=_Real (a_real 0/1) t1)
- (not (<_Real (a_real 0/1) t2))))))))))))
-
-(declare imply_negated_inequality_<_<=
- (! t1 (term Real)
- (! t2 (term Real)
- (! p1 poly
- (! p2 poly
- (! pn1 (poly_norm t1 p1)
- (! pn2 (poly_norm t2 p2)
- (! u (^ (mp_ifneg (is_poly_const (poly_add p1 p2)) tt ff) tt)
- (th_holds
- (impl (<_Real (a_real 0/1) t1)
- (not (<=_Real (a_real 0/1) t2))))))))))))
-
-;; imply weaker inequality
-
-(declare imply_weaker_inequality_<_<
- (! t (term Real)
- (! c1 mpq
- (! c2 mpq
- (! u (^ (mp_ifneg (mp_add c2 (mp_mul (~ 1/1 ) c1)) tt ff) ff)
- (th_holds
- (impl (<_Real (a_real 0/1) (+_Real (a_real c1) t))
- (<_Real (a_real 0/1) (+_Real (a_real c2) t)))))))))
-
-(declare imply_weaker_inequality_<=_<=
- (! t (term Real)
- (! c1 mpq
- (! c2 mpq
- (! u (^ (mp_ifneg (mp_add c2 (mp_mul (~ 1/1 ) c1)) tt ff) ff)
- (th_holds
- (impl (<=_Real (a_real 0/1) (+_Real (a_real c1) t))
- (<=_Real (a_real 0/1) (+_Real (a_real c2) t)))))))))
-
-(declare imply_weaker_inequality_<=_<
- (! t (term Real)
- (! c1 mpq
- (! c2 mpq
- (! u (^ (mpq_ifpos (mp_add c2 (mp_mul (~ 1/1 ) c1))) tt)
- (th_holds
- (impl (<=_Real (a_real 0/1) (+_Real (a_real c1) t))
- (<_Real (a_real 0/1) (+_Real (a_real c2) t)))))))))
-
-(declare imply_weaker_inequality_<_<=
- (! t (term Real)
- (! c1 mpq
- (! c2 mpq
- (! u (^ (mp_ifneg (mp_add c2 (mp_mul (~ 1/1 ) c1)) tt ff) ff)
- (th_holds
- (impl (<_Real (a_real 0/1) (+_Real (a_real c1) t))
- (<=_Real (a_real 0/1) (+_Real (a_real c2) t)))))))))
-
-
-(declare rewrite_iff_symm
- (! f1 formula
- (! f2 formula
- (th_holds (iff (iff f1 f2) (iff f2 f1))))))
-
-(declare rewrite_eq_symm
- (! t1 (term Real)
- (! t2 (term Real)
- (th_holds (iff (= Real t1 t2) (= Real t2 t1))))))
-
-
-;; rewrite implies
-
-(declare rewrite_implies
- (! f1 formula
- (! f2 formula
- (th_holds (iff (impl f1 f2) (or (not f1) f2))))))
-
-;; not to iff
-
-(declare not_to_iff
- (! f1 formula
- (! f2 (th_holds (not f1))
- (th_holds (iff f1 false)))))
-
-;; rewrite_not_not
-
-(declare rewrite_not_not
- (! f formula
- (th_holds (iff (not (not f)) f ))))
-
-(declare uminus_to_mult
- (! c mpq
- (th_holds (= Real (u-_Real (a_real c)) (*_Real (a_real (~ 1/1)) (a_real c))))))
-
-;; const_predicate
-(declare const_predicate_=
- (! c1 mpq
- (! c2 mpq
- (! r (^ (mp_ifzero (mp_add c2 (mp_mul (~ 1/1) c1)) tt ff) ff)
- (th_holds (iff (= Real (a_real c1) (a_real c2)) false))))))
-
-(declare const_predicate_<
- (! c1 mpq
- (! c2 mpq
- (! r (^ (mpq_ifpos (mp_add c2 (mp_mul (~ 1/1) c1))) ff)
- (th_holds (iff (<_Real (a_real c1) (a_real c2)) false))))))
-
-(declare const_predicate_<=
- (! c1 mpq
- (! c2 mpq
- (! r (^ (mp_ifneg (mp_add c2 (mp_mul (~ 1/1) c1)) tt ff) tt)
- (th_holds (iff (<=_Real (a_real c1) (a_real c2)) false))))))
-
-(declare const_predicate_=_t
- (! c1 mpq
- (! c2 mpq
- (! r (^ (mp_ifzero (mp_add c2 (mp_mul (~ 1/1) c1)) tt ff) tt)
- (th_holds (iff (= Real (a_real c1) (a_real c2)) true))))))
-
-(declare const_predicate_<_t
- (! c1 mpq
- (! c2 mpq
- (! r (^ (mpq_ifpos (mp_add c2 (mp_mul (~ 1/1) c1))) tt)
- (th_holds (iff (<_Real (a_real c1) (a_real c2)) true))))))
-
-(declare const_predicate_<=_t
- (! c1 mpq
- (! c2 mpq
- (! r (^ (mp_ifneg (mp_add c2 (mp_mul (~ 1/1) c1)) tt ff) ff)
- (th_holds (iff (<=_Real (a_real c1) (a_real c2)) true))))))
-
-
-(declare rewrite_not_true (th_holds (iff (not true) false)))
-
-(declare rewrite_not_false (th_holds (iff (not false) true)))
-
-(declare rewrite_eq_symm
- (! t1 (term Real)
- (! t2 (term Real)
- (th_holds (iff (= Real t1 t2) (= Real t2 t1))))))
-
-(declare rewrite_eq_refl
- (! t1 (term Real)
- (th_holds (iff (= Real t1 t1) true))))
-
-; class of ignored rules
-
-(declare iff_true
- (! f formula
- (! u (th_holds f)
- (th_holds (iff f true)))))
-
-
-(declare iff_not_false
- (! f formula
- (! u (th_holds f)
- (th_holds (iff (not f) false)))))
-
-(declare iff_true_elim
- (! f formula
- (! u (th_holds (iff f true))
- (th_holds f))))
-
-(declare iff_false_elim
- (! f formula
- (! u (th_holds (iff f false))
- (th_holds (not f)))))
-
-(declare not_to_iff
- (! f formula
- (! u (th_holds (not f))
- (th_holds (iff f false)))))
-
-
-(declare iff_true_impl
- (! f formula
- (! u (th_holds f)
- (th_holds (impl f true)))))
-
-(declare iff_not_false_impl
- (! f formula
- (! u (th_holds f)
- (th_holds (impl (not f) false)))))
-
-(declare iff_true_elim_impl
- (! f formula
- (! u (th_holds (impl f true))
- (th_holds f))))
-
-(declare iff_false_elim_impl
- (! f formula
- (! u (th_holds (impl f false))
- (th_holds (not f)))))
-
-(declare not_to_iff_impl
- (! f formula
- (! u (th_holds (not f))
- (th_holds (impl f false)))))
-
-
-; the different rewrite_iff cases
-
-(declare rewrite_iff_true_l
- (!f1 formula
- (th_holds (iff (iff true f1) f1))))
-
-(declare rewrite_iff_false_l
- (!f1 formula
- (th_holds (iff (iff false f1) (not f1)))))
-
-(declare rewrite_iff_not_l
- (!f1 formula
- (th_holds (iff (iff (not f1) f1) false))))
-
-(declare rewrite_iff_true_r
- (!f1 formula
- (th_holds (iff (iff f1 true) f1))))
-
-(declare rewrite_iff_false_r
- (!f1 formula
- (th_holds (iff (iff f1 false) (not f1)))))
-
-(declare rewrite_iff_not_r
- (!f1 formula
- (th_holds (iff (iff f1 (not f1)) false))))
-
-
-
-; ite axiom
-(declare ite_axiom
- (! f formula
- (! t1 (term Real)
- (! t2 (term Real)
- (th_holds (ifte f (= Real (ite Real f t1 t2) t1) (= Real (ite Real f t1 t2) t2)))))))
-
-; ite same
-(declare rewrite_ite_same
- (! f formula
- (! t (term Real)
- (th_holds (= Real (ite Real f t t) t)))))
-
-(declare imply_equalities
- (! t1 (term Real)
- (! t2 (term Real)
- (! t3 (term Real)
- (! t4 (term Real)
- (! p1 poly
- (! p2 poly
- (! pn1 (poly_norm (-_Real t2 t1) p1)
- (! pn2 (poly_norm (-_Real t4 t3) p2)
- (! u1 (th_holds (<=_Real t1 t2))
- (! u2 (th_holds (<=_Real t3 t4))
- (! u (^ (mp_ifzero (is_poly_const (poly_add p1 p2)) tt ff) tt)
- (th_holds (and (= Real t1 t2) (= Real t3 t4)))))))))))))))
-
-
-(declare contrapositive
- (! f1 formula
- (! f2 formula
- (! u (th_holds (impl f1 f2))
- (th_holds (impl (not f2) (not f1)))))))
\ No newline at end of file
diff --git a/th_lra.plf b/th_lra.plf
deleted file mode 100644
index fa95f68..0000000
--- a/th_lra.plf
+++ /dev/null
@@ -1,482 +0,0 @@
-; 59 loc in side conditions
-
-(program mpq_ifpos ((x mpq)) bool
- (mp_ifneg x ff (mp_ifzero x ff tt)))
-
-; a real variable
-(declare var_real type)
-; a real variable term
-(declare a_var_real (! v var_real (term Real)))
-
-;; linear polynomials in the form a_1*x_1 + a_2*x_2 .... + a_n*x_n
-
-(declare lmon type)
-(declare lmonn lmon)
-(declare lmonc (! c mpq (! v var_real (! l lmon lmon))))
-
-(program lmon_neg ((l lmon)) lmon
- (match l
- (lmonn l)
- ((lmonc c' v' l') (lmonc (mp_neg c') v' (lmon_neg l')))))
-
-(program lmon_add ((l1 lmon) (l2 lmon)) lmon
- (match l1
- (lmonn l2)
- ((lmonc c' v' l')
- (match l2
- (lmonn l1)
- ((lmonc c'' v'' l'')
- (compare v' v''
- (lmonc c' v' (lmon_add l' l2))
- (lmonc c'' v'' (lmon_add l1 l''))))))))
-
-(program lmon_mul_c ((l lmon) (c mpq)) lmon
- (match l
- (lmonn l)
- ((lmonc c' v' l') (lmonc (mp_mul c c') v' (lmon_mul_c l' c)))))
-
-;; linear polynomials in the form (a_1*x_1 + a_2*x_2 .... + a_n*x_n) + c
-
-(declare poly type)
-(declare polyc (! c mpq (! l lmon poly)))
-
-(program poly_neg ((p poly)) poly
- (match p
- ((polyc m' p') (polyc (mp_neg m') (lmon_neg p')))))
-
-(program poly_add ((p1 poly) (p2 poly)) poly
- (match p1
- ((polyc c1 l1)
- (match p2
- ((polyc c2 l2) (polyc (mp_add c1 c2) (lmon_add l1 l2)))))))
-
-(program poly_sub ((p1 poly) (p2 poly)) poly
- (poly_add p1 (poly_neg p2)))
-
-(program poly_mul_c ((p poly) (c mpq)) poly
- (match p
- ((polyc c' l') (polyc (mp_mul c' c) (lmon_mul_c l' c)))))
-
-;; code to isolate a variable from a term
-;; if (isolate v l) returns (c,l'), this means l = c*v + l', where v is not in FV(t').
-
-(declare isol type)
-(declare isolc (! r mpq (! l lmon isol)))
-
-(program isolate_h ((v var_real) (l lmon) (e bool)) isol
- (match l
- (lmonn (isolc 0/1 l))
- ((lmonc c' v' l')
- (ifmarked v'
- (match (isolate_h v l' tt)
- ((isolc ci li) (isolc (mp_add c' ci) li)))
- (match e
- (tt (isolc 0/1 l))
- (ff (match (isolate_h v l' ff)
- ((isolc ci li) (isolc ci (lmonc c' v' li))))))))))
-
-(program isolate ((v var_real) (l lmon)) isol
- (do (markvar v)
- (let i (isolate_h v l ff)
- (do (markvar v) i))))
-
-;; determine if a monomial list is constant
-
-(program is_lmon_zero ((l lmon)) bool
- (match l
- (lmonn tt)
- ((lmonc c v l')
- (match (isolate v l)
- ((isolc ci li)
- (mp_ifzero ci (is_lmon_zero li) ff))))))
-
-;; return the constant that p is equal to. If p is not constant, fail.
-
-(program is_poly_const ((p poly)) mpq
- (match p
- ((polyc c' l')
- (match (is_lmon_zero l')
- (tt c')
- (ff (fail mpq))))))
-
-;; conversion to use polynomials in term formulas
-
-(declare poly_term (! p poly (term Real)))
-
-;; create new equality out of inequality
-
-(declare lra_>=_>=_to_=
- (! p1 poly
- (! p2 poly
- (! f1 (th_holds (>=0_Real (poly_term p1)))
- (! f2 (th_holds (>=0_Real (poly_term p2)))
- (! i2 (^ (mp_ifzero (is_poly_const (poly_add p1 p2)) tt ff) tt)
- (th_holds (=0_Real (poly_term p2))))))))))
-
-;; axioms
-
-(declare lra_axiom_=
- (th_holds (=0_Real (poly_term (polyc 0/1 lmonn)))))
-
-(declare lra_axiom_>
- (! c mpq
- (! i (^ (mpq_ifpos c) tt)
- (th_holds (>0_Real (poly_term (polyc c lmonn)))))))
-
-(declare lra_axiom_>=
- (! c mpq
- (! i (^ (mp_ifneg c tt ff) ff)
- (th_holds (>=0_Real (poly_term (polyc c lmonn)))))))
-
-(declare lra_axiom_distinct
- (! c mpq
- (! i (^ (mp_ifzero c tt ff) ff)
- (th_holds (distinct0_Real (poly_term (polyc c lmonn)))))))
-
-;; contradiction rules
-
-(declare lra_contra_=
- (! p poly
- (! f (th_holds (=0_Real (poly_term p)))
- (! i (^ (mp_ifzero (is_poly_const p) tt ff) ff)
- bottom))))
-
-(declare lra_contra_>
- (! p poly
- (! f (th_holds (>0_Real (poly_term p)))
- (! i2 (^ (mpq_ifpos (is_poly_const p)) ff)
- bottom))))
-
-(declare lra_contra_>=
- (! p poly
- (! f (th_holds (>=0_Real (poly_term p)))
- (! i2 (^ (mp_ifneg (is_poly_const p) tt ff) tt)
- bottom))))
-
-(declare lra_contra_distinct
- (! p poly
- (! f (th_holds (distinct0_Real (poly_term p)))
- (! i2 (^ (mp_ifzero (is_poly_const p) tt ff) tt)
- bottom))))
-
-;; muliplication by a constant
-
-(declare lra_mul_c_=
- (! p poly
- (! p' poly
- (! c mpq
- (! f (th_holds (=0_Real (poly_term p)))
- (! i (^ (poly_mul_c p c) p')
- (th_holds (=0_Real (poly_term p')))))))))
-
-(declare lra_mul_c_>
- (! p poly
- (! p' poly
- (! c mpq
- (! f (th_holds (>0_Real (poly_term p)))
- (! i (^ (mp_ifneg c (fail poly) (mp_ifzero c (fail poly) (poly_mul_c p c))) p')
- (th_holds (>0_Real (poly_term p')))))))));)
-
-(declare lra_mul_c_>=
- (! p poly
- (! p' poly
- (! c mpq
- (! f (th_holds (>=0_Real (poly_term p)))
- (! i (^ (mp_ifneg c (fail poly) (poly_mul_c p c)) p')
- (th_holds (>=0_Real (poly_term p')))))))));)
-
-(declare lra_mul_c_distinct
- (! p poly
- (! p' poly
- (! c mpq
- (! f (th_holds (distinct0_Real (poly_term p)))
- (! i (^ (mp_ifzero c (fail poly) (poly_mul_c p c)) p')
- (th_holds (distinct0_Real (poly_term p')))))))));)
-
-;; adding equations
-
-(declare lra_add_=_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_Real (poly_term p1)))
- (! f2 (th_holds (=0_Real (poly_term p2)))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (=0_Real (poly_term p3)))))))))))
-
-(declare lra_add_>_>
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>0_Real (poly_term p1)))
- (! f2 (th_holds (>0_Real (poly_term p2)))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>0_Real (poly_term p3))))))))))
-
-(declare lra_add_>=_>=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>=0_Real (poly_term p1)))
- (! f2 (th_holds (>=0_Real (poly_term p2)))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>=0_Real (poly_term p3))))))))))
-
-(declare lra_add_=_>
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_Real (poly_term p1)))
- (! f2 (th_holds (>0_Real (poly_term p2)))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>0_Real (poly_term p3))))))))))
-
-(declare lra_add_=_>=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_Real (poly_term p1)))
- (! f2 (th_holds (>=0_Real (poly_term p2)))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>=0_Real (poly_term p3))))))))))
-
-(declare lra_add_>_>=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>0_Real (poly_term p1)))
- (! f2 (th_holds (>=0_Real (poly_term p2)))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>0_Real (poly_term p3))))))))))
-
-(declare lra_add_=_distinct
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_Real (poly_term p1)))
- (! f2 (th_holds (distinct0_Real (poly_term p2)))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (distinct0_Real (poly_term p3)))))))))))
-
-;; substracting equations
-
-(declare lra_sub_=_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_Real (poly_term p1)))
- (! f2 (th_holds (=0_Real (poly_term p2)))
- (! i (^ (poly_sub p1 p2) p3)
- (th_holds (=0_Real (poly_term p3)))))))))))
-
-(declare lra_sub_>_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>0_Real (poly_term p1)))
- (! f2 (th_holds (=0_Real (poly_term p2)))
- (! i (^ (poly_sub p1 p2) p3)
- (th_holds (>0_Real (poly_term p3))))))))))
-
-(declare lra_sub_>=_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>=0_Real (poly_term p1)))
- (! f2 (th_holds (=0_Real (poly_term p2)))
- (! i (^ (poly_sub p1 p2) p3)
- (th_holds (>=0_Real (poly_term p3))))))))))
-
-(declare lra_sub_distinct_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (distinct0_Real (poly_term p1)))
- (! f2 (th_holds (=0_Real (poly_term p2)))
- (! i (^ (poly_sub p1 p2) p3)
- (th_holds (distinct0_Real (poly_term p3)))))))))))
-
- ;; converting between terms and polynomials
-
-(declare poly_norm (! t (term Real) (! p poly type)))
-
-(declare pn_let
- (! t (term Real)
- (! p poly
- (! pn (poly_norm t p)
- (! u (! pnt (poly_norm t p)
- bottom)
- bottom)))))
-
-(declare pn_const
- (! x mpq
- (poly_norm (a_real x) (polyc x lmonn))))
-
-(declare pn_var
- (! v var_real
- (poly_norm (a_var_real v) (polyc 0/1 (lmonc 1/1 v lmonn)))))
-
-
-(declare pn_+
- (! x (term Real)
- (! px poly
- (! y (term Real)
- (! py poly
- (! pz poly
- (! pnx (poly_norm x px)
- (! pny (poly_norm y py)
- (! a (^ (poly_add px py) pz)
- (poly_norm (+_Real x y) pz))))))))))
-
-(declare pn_-
- (! x (term Real)
- (! px poly
- (! y (term Real)
- (! py poly
- (! pz poly
- (! pnx (poly_norm x px)
- (! pny (poly_norm y py)
- (! a (^ (poly_sub px py) pz)
- (poly_norm (-_Real x y) pz))))))))))
-
-(declare pn_mul_c_L
- (! y (term Real)
- (! py poly
- (! pz poly
- (! x mpq
- (! pny (poly_norm y py)
- (! a (^ (poly_mul_c py x) pz)
- (poly_norm (*_Real (a_real x) y) pz))))))))
-
-(declare pn_mul_c_R
- (! y (term Real)
- (! py poly
- (! pz poly
- (! x mpq
- (! pny (poly_norm y py)
- (! a (^ (poly_mul_c py x) pz)
- (poly_norm (*_Real y (a_real x)) pz))))))))
-
-;; for polynomializing other terms, in particular ite's
-
-(declare term_atom (! v var_real (! t (term Real) type)))
-
-(declare decl_term_atom
- (! t (term Real)
- (! u (! v var_real
- (! a (term_atom v t)
- bottom))
- bottom)))
-
-(declare pn_var_atom
- (! v var_real
- (! t (term Real)
- (! a (term_atom v t)
- (poly_norm t (polyc 0/1 (lmonc 1/1 v lmonn)))))))
-
-
-;; conversion between term formulas and polynomial formulas
-
-(declare poly_formula_norm (! ft formula (! fp formula type)))
-
-; convert between term formulas and polynomial formulas
-
-(declare poly_form
- (! ft formula
- (! fp formula
- (! p (poly_formula_norm ft fp)
- (! u (th_holds ft)
- (th_holds fp))))))
-
-(declare poly_form_not
- (! ft formula
- (! fp formula
- (! p (poly_formula_norm ft fp)
- (! u (th_holds (not ft))
- (th_holds (not fp)))))))
-
-; form equivalence between term formula and polynomial formula
-
-(declare poly_norm_=
- (! x (term Real)
- (! y (term Real)
- (! p poly
- (! n (poly_norm (-_Real x y) p)
- (! u (! pn (poly_formula_norm (= Real x y) (=0_Real (poly_term p)))
- bottom)
- bottom))))))
-
-(declare poly_norm_>
- (! x (term Real)
- (! y (term Real)
- (! p poly
- (! n (poly_norm (-_Real x y) p)
- (! u (! pn (poly_formula_norm (>_Real x y) (>0_Real (poly_term p)))
- bottom)
- bottom))))))
-
-(declare poly_norm_<
- (! x (term Real)
- (! y (term Real)
- (! p poly
- (! n (poly_norm (-_Real y x) p)
- (! u (! pn (poly_formula_norm (<_Real x y) (>0_Real (poly_term p)))
- bottom)
- bottom))))))
-
-(declare poly_norm_>=
- (! x (term Real)
- (! y (term Real)
- (! p poly
- (! n (poly_norm (-_Real x y) p)
- (! u (! pn (poly_formula_norm (>=_Real x y) (>=0_Real (poly_term p)))
- bottom)
- bottom))))))
-
-(declare poly_norm_<=
- (! x (term Real)
- (! y (term Real)
- (! p poly
- (! n (poly_norm (-_Real y x) p)
- (! u (! pn (poly_formula_norm (<=_Real x y) (>=0_Real (poly_term p)))
- bottom)
- bottom))))))
-
-(declare poly_norm_distinct
- (! x (term Real)
- (! y (term Real)
- (! p poly
- (! n (poly_norm (-_Real y x) p) ; note the sign change
- (! u (! pn (poly_formula_norm (distinct Real x y) (distinct0_Real (poly_term p)))
- bottom)
- bottom))))))
-
-;; negated polynomial formula conversion
-
-(declare lra_not_=_to_distinct
- (! p poly
- (! p' poly
- (! f (th_holds (not (=0_Real (poly_term p))))
- (! u (^ (poly_neg p) p')
- (th_holds (distinct0_Real (poly_term p'))))))))
-
-(declare lra_not_>_to_>=
- (! p poly
- (! p' poly
- (! f (th_holds (not (>0_Real (poly_term p))))
- (! u (^ (poly_neg p) p')
- (th_holds (>=0_Real (poly_term p'))))))))
-
-(declare lra_not_>=_to_>
- (! p poly
- (! p' poly
- (! f (th_holds (not (>=0_Real (poly_term p))))
- (! u (^ (poly_neg p) p')
- (th_holds (>0_Real (poly_term p'))))))))
-
-(declare lra_not_distinct_to_=
- (! p poly
- (! p' poly
- (! f (th_holds (not (distinct0_Real (poly_term p))))
- (! u (^ (poly_neg p) p')
- (th_holds (=0_Real (poly_term p'))))))))
diff --git a/th_real.plf b/th_real.plf
deleted file mode 100644
index ecb268d..0000000
--- a/th_real.plf
+++ /dev/null
@@ -1,153 +0,0 @@
-(declare Real sort)
-
-(define arithpred_Real (! x (term Real)
- (! y (term Real)
- formula)))
-
-(declare >_Real arithpred_Real)
-(declare >=_Real arithpred_Real)
-(declare <_Real arithpred_Real)
-(declare <=_Real arithpred_Real)
-
-(define arithterm_Real (! x (term Real)
- (! y (term Real)
- (term Real))))
-(declare +_Real arithterm_Real)
-(declare -_Real arithterm_Real)
-(declare *_Real arithterm_Real)
-(declare /_Real arithterm_Real)
-
-; a constant term
-(declare a_real (! x mpq (term Real)))
-
-; unary negation ?
-(declare u-_Real (! t (term Real) (term Real)))
-
-;; normalization to >=, >
-
-(declare <_to_>_Real
- (! x (term Real)
- (! y (term Real)
- (! u (th_holds (<_Real x y))
- (th_holds (>_Real y x))))))
-
-(declare <=_to_>=_Real
- (! x (term Real)
- (! y (term Real)
- (! u (th_holds (<=_Real x y))
- (th_holds (>=_Real y x))))))
-
-(declare not_<_to_>=_Real
- (! x (term Real)
- (! y (term Real)
- (! u (th_holds (not (<_Real x y)))
- (th_holds (>=_Real x y))))))
-
-(declare not_<=_to_>_Real
- (! x (term Real)
- (! y (term Real)
- (! u (th_holds (not (<=_Real x y)))
- (th_holds (>_Real x y))))))
-
-(declare not_>_to_>=_Real
- (! x (term Real)
- (! y (term Real)
- (! u (th_holds (not (>_Real x y)))
- (th_holds (>=_Real y x))))))
-
-(declare not_>=_to_>_Real
- (! x (term Real)
- (! y (term Real)
- (! u (th_holds (not (>=_Real x y)))
- (th_holds (>_Real y x))))))
-
-;; transitivity for >=, >
-
-(declare trans_>=_>=_Real
- (! x (term Real)
- (! y (term Real)
- (! z (term Real)
- (! u1 (th_holds (>=_Real x y))
- (! u2 (th_holds (>=_Real y z))
- (th_holds (>=_Real x z))))))))
-
-(declare trans_>=_>_Real
- (! x (term Real)
- (! y (term Real)
- (! z (term Real)
- (! u1 (th_holds (>=_Real x y))
- (! u2 (th_holds (>_Real y z))
- (th_holds (>_Real x z))))))))
-
-(declare trans_>_>=_Real
- (! x (term Real)
- (! y (term Real)
- (! z (term Real)
- (! u1 (th_holds (>_Real x y))
- (! u2 (th_holds (>=_Real y z))
- (th_holds (>_Real x z))))))))
-
-(declare trans_>_>_Real
- (! x (term Real)
- (! y (term Real)
- (! z (term Real)
- (! u1 (th_holds (>_Real x y))
- (! u2 (th_holds (>_Real y z))
- (th_holds (>_Real x z))))))))
-
-; predicate with 0 assumed for the RHS
-
-(define arithpred0_Real (! x (term Real)
- formula))
-
-(declare >0_Real arithpred0_Real)
-(declare >=0_Real arithpred0_Real)
-(declare <0_Real arithpred0_Real)
-(declare <=0_Real arithpred0_Real)
-(declare =0_Real arithpred0_Real)
-(declare distinct0_Real arithpred0_Real)
-
-;; conversion between arithpred0_Real and arithpred_Real
-
-(declare norm_>_Real
- (! x (term Real)
- (! y (term Real)
- (! t (th_holds (>_Real x y))
- (th_holds (>0_Real (-_Real x y)))))))
-
-(declare norm_>=_Real
- (! x (term Real)
- (! y (term Real)
- (! t (th_holds (>=_Real x y))
- (th_holds (>=0_Real (-_Real x y)))))))
-
-(declare norm_<_Real
- (! x (term Real)
- (! y (term Real)
- (! t (th_holds (<_Real x y))
- (th_holds (<0_Real (-_Real x y)))))))
-
-(declare norm_<=_Real
- (! x (term Real)
- (! y (term Real)
- (! t (th_holds (<=_Real x y))
- (th_holds (<=0_Real (-_Real x y)))))))
-
-(declare norm_=_Real
- (! x (term Real)
- (! y (term Real)
- (! t (th_holds (= Real x y))
- (th_holds (=0_Real (-_Real x y)))))))
-
-(declare norm_distinct_Real
- (! x (term Real)
- (! y (term Real)
- (! t (th_holds (distinct Real x y))
- (th_holds (distinct0_Real (-_Real x y)))))))
-
-;; weaken to non-strict inequality
-
-(declare >0_to_>=0_Real
- (! x (term Real)
- (! u (th_holds (>0_Real x))
- (th_holds (>=0_Real x)))))
\ No newline at end of file
^ permalink raw reply related [flat|nested] only message in thread
only message in thread, other threads:[~2026-08-04 22:04 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2026-08-04 22:04 [rpms/lfsc] rawhide: Orphaned for 6+ weeks Orphaned Packages Process
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox