gaxiiiiiiiiiiii

import Mathlib.tactic

abbrev Var := Nat

structure Lang where
  Const : Type
  Func : Nat → Type
  Rel : Nat → Type

/------

gaxiiiiiiiiiiii

import Mathlib
open scoped Pointwise
open Polynomial

#check Finset.sup_le
example [inst : SemilatticeSup α] [inst_1 : OrderBot α] [DecidableEq β] {s : Finset β} {f : β → α} {a : α} :
  (∀ b ∈ s, f b ≤ a) → s.sup f ≤ a
:= by
  induction s using Finset.induction_on with
  | empty => simp

gaxiiiiiiiiiiii

論理式

ϕ, ψ := A | ⊥ | R₁ t | R₂ (t₁, t₂) | ¬ϕ | ϕ ∧ ψ | ϕ ∨ ψ | ϕ → ψ | ∀x.ϕ | ∃x.ϕ

A は命題記号
x は変数記号
t,t₁,t₂ は項
R₁は1変数述語記号
R₂は2変数述語記号

gaxiiiiiiiiiiii

import Mathlib

lemma Subgroup.IsCyclic [Group G] [HG : IsCyclic G] (H : Subgroup G)  :
  IsCyclic H
:= by
  haveI := Classical.propDecidable
  obtain ⟨g, Hg : ∀ h, ∃ k, g ^ k = h⟩ := HG
  cases' subsingleton_or_nontrivial H with H0 H0
  · rcases H0 with ⟨H0⟩
    constructor; use 1; intro h; simp

gaxiiiiiiiiiiii

import Mathlib.tactic

example [Group G] [Fintype G] (g : G) :
  Fintype.card (Subgroup.zpowers g) = orderOf g
:= by
   have : orderOf g = Fintype.card (Fin (orderOf g)) := by simp
   rw [this]
   apply Fintype.card_congr
   refine {
    toFun := λ ⟨x, Hx⟩ => by

gaxiiiiiiiiiiii

import Mathlib.tactic
import Mathlib.GroupTheory.Complement

open Classical
open scoped Pointwise

lemma Subgroup.card_not_eq [Group G] [Fintype G] (H : Subgroup G) :
  Fintype.card ↑H ≠ 0
:= by
  intro F

gaxiiiiiiiiiiii

From mathcomp Require Import ssreflect.
Require Import Nat.

Definition name := nat.

Inductive proc :=
  | Nil
  | Tau (P : proc)
  | Para (P Q : proc)
  | Sum (P Q : proc)

gaxiiiiiiiiiiii

From mathcomp Require Import ssreflect.
From Autosubst Require Import Autosubst.
Require Import Nat.

Inductive proc_ :=
  | Var (x : var)
  | Nil
  | Para (P Q : proc_)
  | Repl (P : proc_)
  | Send (M : proc_) (N : proc_) (P : proc_)

gaxiiiiiiiiiiii

  function Pow(n:nat, k:nat) : (r:nat)
    ensures n > 0 ==> r > 0     
    {
        if k == 0 then 1
        else if k == 1 then n
        else
            var p := k / 2;
            var np := Pow(n,p);
            if p*2 == k then np * np
            else

gaxiiiiiiiiiiii

function Pow(n:nat, k:nat) : (r:nat)
  // Following needed for some proofs
  ensures n > 0 ==> r > 0     
  {
      if k == 0 then 1
      else if k == 1 then n
      else
          var p := k / 2;
          var np := Pow(n,p);
          if p*2 == k then np * np