namespace http://cds.omdoc.org/examples ❚

import lfx http://gl.mathhub.info/MMT/LFX/TypedHierarchy ❚
import finite http://gl.mathhub.info/MMT/LFX/Finite ❚
import rules scala://structuralfeatures.lf.mmt.kwarc.info❚

theory Hofstadter : ?InductivelyDefinedTypes =
	inductive hofstadter() ❘ =
		F: type ❙
		M: type ❙
		f: nat/n ⟶ F ❙
		m: nat/n ⟶ M ❙
		fToNat: F ⟶ nat/n ❙
		mToNat: M ⟶ nat/n ❙
  ❚

	minus: nat/n ⟶ nat/n ⟶ nat/n ❘ # 1 - 2 ❙
	/T A nice example demonstrating why this feature doesn't allow for mutually inductive definitions over a (non-mutually) inductively-defined type 
		 This shouldn't be (and isn't) accepted by the feature, as the definition f_h refers to hofstadter/f (self or forward-reverences) are not (and can't be) expanded ❙
  // inductive_definition hofstadter_mf_sequences() : hofstadter() ❘ =
	// 	F: type ❘ = nat/n  ❙
	// 	M: type ❘ = nat/n  ❙
	// 	fToNat: nat/n ⟶ nat/n ❘ = [u] u ❙
	// 	mToNat: nat/n ⟶ nat/n ❘ = [u] u ❙
	// 	f_h: nat/n ⟶ nat/n*nat/n ❘ = [u] (nat/induct/n (nat/n * nat/n) (pair_term nat/n nat/n (nat/s nat/z) (nat/s nat/z)) ([x] 
	// 		(pair_term nat/n nat/n (pair/a nat/n nat/n x) ((nat/s (pair/a nat/n nat/n x)) - (hofstadter/mToNat (hofstadter/m (pair/b nat/n nat/n x))))))) u ❙
	// 	f: nat/n ⟶ nat/n ❘ = [u] (nat/induct/n nat/n (nat/s nat/z) ([v] (pair/b nat/n nat/n (f_h v)))) u ❙
 	// 	m_h: nat/n ⟶ nat/n*nat/n ❘ = [u] (nat/induct/n (nat/n * nat/n) (pair_term nat/n nat/n nat/z nat/z) ([x] 
	// 		(pair_term nat/n nat/n (pair/a nat/n nat/n x) ((nat/s (pair/a nat/n nat/n x)) - (f (pair/b nat/n nat/n x)))))) u ❙
	// 	m: nat/n ⟶ nat/n ❘ = [u] (nat/induct/n nat/n nat/z ([v] (pair/b nat/n nat/n (m_h v)))) u ❙
  // ❚
❚